En mi opinión, en el sector de Internet de habla rusa el tema de la verificación formal no está suficientemente tratado y, sobre todo, faltan ejemplos simples y claros.
Daré un ejemplo de una fuente extranjera y agregaré mi propia solución al conocido problema de cruzar un lobo, una cabra y un repollo al otro lado del río.
Pero primero describiré brevemente qué es la verificación formal y por qué es necesaria.
La verificación formal generalmente significa verificar un programa o algoritmo utilizando otro.
Esto es necesario para garantizar que el programa se comporte como se espera y también para garantizar su seguridad.
La verificación formal es el medio más poderoso para encontrar y eliminar vulnerabilidades: le permite encontrar todos los agujeros y errores existentes en un programa, o demostrar que no existen.
Vale la pena señalar que en algunos casos esto es imposible, como en el problema de las 8 reinas con un tablero de 1000 casillas de ancho: todo se reduce a la complejidad algorítmica o al problema de detenerse.
Sin embargo, en cualquier caso se recibirá una de tres respuestas: el programa es correcto, incorrecto o no fue posible calcular la respuesta.
Si es imposible encontrar una respuesta, a menudo es posible reelaborar partes poco claras del programa, reduciendo su complejidad algorítmica, para obtener una respuesta específica de sí o no.
Y la verificación formal se utiliza, por ejemplo, en el kernel de Windows y en los sistemas operativos del dron Darpa, para garantizar el máximo nivel de protección.
Usaremos Z3Prover, una herramienta muy poderosa para la demostración automatizada de teoremas y la resolución de ecuaciones.
Además, Z3 resuelve ecuaciones y no selecciona sus valores mediante la fuerza bruta.
Esto significa que es capaz de encontrar la respuesta, incluso en los casos en los que hay 10^100 combinaciones de opciones de entrada.
Pero esto es sólo alrededor de una docena de argumentos de entrada de tipo Integer, y esto se encuentra a menudo en la práctica.
Problema de 8 reinas (Tomado del inglés ).
# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]
# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]
# At most one queen per column
col_c = [ Distinct(Q) ]
# Diagonal constraint
diag_c = [ If(i == j,
True,
And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
for i in range(8) for j in range(i) ]
solve(val_c + col_c + diag_c)
Al ejecutar Z3, obtenemos la solución:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
El problema de la reina es comparable a un programa que toma como entrada las coordenadas de 8 reinas y genera la respuesta si las reinas se vencieron entre sí.
Si tuviéramos que resolver un programa de este tipo mediante verificación formal, entonces, en comparación con el problema, simplemente necesitaríamos dar un paso más para convertir el código del programa en una ecuación: resultaría ser esencialmente idéntico al nuestro ( por supuesto, si el programa fue escrito correctamente).
Casi lo mismo sucederá en el caso de buscar vulnerabilidades: simplemente establecemos las condiciones de salida que necesitamos, por ejemplo, la contraseña de administrador, transformamos el código fuente o descompilado en ecuaciones compatibles con la verificación, y luego obtenemos una respuesta de qué Es necesario proporcionar datos como entrada para lograr el objetivo.
En mi opinión, el problema del lobo, la cabra y la col es aún más interesante, pues solucionarlo ya requiere de muchos (7) pasos.
Si el problema de la reina es comparable al caso en el que se puede acceder a un servidor mediante una sola solicitud GET o POST, entonces el lobo, la cabra y el repollo son un ejemplo de una categoría mucho más compleja y extendida, en la que el objetivo sólo se puede lograr por varias solicitudes.
Esto es comparable, por ejemplo, a un escenario en el que necesita encontrar una inyección SQL, escribir un archivo a través de ella, luego elevar sus derechos y solo entonces obtener una contraseña.
Condiciones del problema y su solución.El granjero necesita transportar un lobo, una cabra y repollo a través del río. El granjero tiene un barco en el que sólo cabe un objeto, además del propio granjero. El lobo se comerá la cabra y la cabra se comerá la col si el granjero las deja desatendidas.
La solución es que en el paso 4 el granjero deberá recuperar la cabra.
Ahora comencemos a resolverlo programáticamente.
Designemos al granjero, el lobo, la cabra y el repollo como 4 variables que toman el valor solo 0 o 1. Cero significa que están en la margen izquierda y uno significa que están en la derecha.
import json
from z3 import *
s = Solver()
Num= 8
Human = [ Int('Human_%i' % (i + 1)) for i in range(Num) ]
Wolf = [ Int('Wolf_%i' % (i + 1)) for i in range(Num) ]
Goat = [ Int('Goat_%i' % (i + 1)) for i in range(Num) ]
Cabbage = [ Int('Cabbage_%i' % (i + 1)) for i in range(Num) ]
# Each creature can be only on left (0) or right side (1) on every state
HumanSide = [ Or(Human[i] == 0, Human[i] == 1) for i in range(Num) ]
WolfSide = [ Or(Wolf[i] == 0, Wolf[i] == 1) for i in range(Num) ]
GoatSide = [ Or(Goat[i] == 0, Goat[i] == 1) for i in range(Num) ]
CabbageSide = [ Or(Cabbage[i] == 0, Cabbage[i] == 1) for i in range(Num) ]
Side = HumanSide+WolfSide+GoatSide+CabbageSide
Num es el número de pasos necesarios para resolver. Cada paso representa el estado del río, del barco y de todas las entidades.
Por ahora elegimoslo al azar y con margen tomamos 10.
Cada entidad está representada en 10 copias; este es su valor en cada uno de los 10 pasos.
Ahora establezcamos las condiciones para el inicio y el final.
Start = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ]
Finish = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]
Luego establecemos las condiciones en las que el lobo se come a la cabra o la cabra se come el repollo, como restricciones en la ecuación.
(En presencia de un granjero la agresión es imposible)
# Wolf cant stand with goat, and goat with cabbage without human. Not 2, not 0 which means that they are one the same side
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
Y por último definiremos todas las posibles acciones del agricultor al cruzar de ida o de vuelta.
Puede llevarse un lobo, una cabra o un repollo, o no llevarse a nadie, o no navegar a ningún lado.
Por supuesto, nadie puede cruzar sin un granjero.
Esto se expresará en el hecho de que cada estado posterior del río, del barco y de las entidades puede diferir del anterior sólo de forma estrictamente limitada.
No más de 2 bits, y con otros muchos límites, ya que el agricultor sólo puede transportar una entidad a la vez y no pueden quedar todas juntas.
Travel = [ Or(
And(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) for i in range(Num-1) ]
Ejecutemos la solución.
solve(Side + Start + Finish + Safe + Travel)
¡Y obtenemos la respuesta!
Z3 encontró un conjunto consistente de estados que satisface todas las condiciones.
Una especie de reparto cuatridimensional del espacio-tiempo.
Averigüemos qué pasó.
Vemos que al final todos cruzaron, solo que al principio nuestro granjero decidió descansar, y en los primeros 2 pasos no nada a ningún lado.
Human_2 = 0
Human_3 = 0
Esto sugiere que el número de estados que elegimos es excesivo y 8 serán suficientes.
En nuestro caso, el granjero hizo esto: empezar, descansar, descansar, cruzar la cabra, cruzar de regreso, cruzar el repollo, regresar con la cabra, cruzar el lobo, regresar solo, volver a entregar la cabra.
Pero al final el problema se solucionó.
#Старт.
Human_1 = 0
Wolf_1 = 0
Goat_1 = 0
Cabbage_1 = 0
#Фермер отдыхает.
Human_2 = 0
Wolf_2 = 0
Goat_2 = 0
Cabbage_2 = 0
#Фермер отдыхает.
Human_3 = 0
Wolf_3 = 0
Goat_3 = 0
Cabbage_3 = 0
#Фермер отвозит козу на нужный берег.
Human_4 = 1
Wolf_4 = 0
Goat_4 = 1
Cabbage_4 = 0
#Фермер возвращается.
Human_5 = 0
Wolf_5 = 0
Goat_5 = 1
Cabbage_5 = 0
#Фермер отвозит капусту на нужный берег.
Human_6 = 1
Wolf_6 = 0
Cabbage_6 = 1
Goat_6 = 1
#Ключевая часть операции: фермер возвращает козу обратно.
Human_7 = 0
Wolf_7 = 0
Goat_7 = 0
Cabbage_7 = 1
#Фермер отвозит волка на другой берег, где он теперь находится вместе с капустой.
Human_8 = 1
Wolf_8 = 1
Goat_8 = 0
Cabbage_8 = 1
#Фермер возвращается за козой.
Human_9 = 0
Wolf_9 = 1
Goat_9 = 0
Cabbage_9 = 1
#Фермер повторно доставляет козу на нужный берег и завершают переправу.
Human_10 = 1
Wolf_10 = 1
Goat_10 = 1
Cabbage_10 = 1
Ahora intentemos cambiar las condiciones y demostrar que no hay soluciones.
Para ello, le daremos herbivoría a nuestro lobo, y él querrá comer repollo.
Esto se puede comparar con el caso en el que nuestro objetivo es proteger la aplicación y debemos asegurarnos de que no haya lagunas.
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i]), Or(Wolf[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
Z3 nos dio la siguiente respuesta:
no solution
Significa que realmente no hay soluciones.
Así, demostramos programáticamente la imposibilidad de cruzar con un lobo omnívoro sin pérdidas para el granjero.
Si la audiencia encuentra interesante este tema, en futuros artículos les diré cómo convertir un programa o función común en una ecuación compatible con métodos formales y resolverla, revelando así todos los escenarios legítimos y vulnerabilidades. Primero, en la misma tarea, pero presentada en forma de programa, para luego complicarla gradualmente y pasar a ejemplos actuales del mundo del desarrollo de software.
El siguiente artículo ya está listo:
En él paso de la verificación formal de problemas a los programas y describo
¿Cómo pueden convertirse automáticamente en sistemas de reglas formales?
Fuente: habr.com