En mi opinión, el tema de la verificación formal no está suficientemente cubierto en el sector de habla rusahablante de Internet, y especialmente faltan ejemplos simples y claros.
Citaré un ejemplo de una fuente extranjera y complementaré con mi propia solución del conocido problema de transportar al lobo, la cabra y la col al otro lado del río.
Pero primero describiré brevemente qué es la verificación formal y por qué es necesaria.
Por lo general, la verificación formal se entiende como la comprobación de un programa o algoritmo mediante otro.
Esto es necesario para asegurarse de que el comportamiento del programa coincide con lo esperado, así como para garantizar su seguridad.
La verificación formal es el medio más poderoso para identificar y eliminar vulnerabilidades: permite encontrar todos los agujeros y errores en el programa, o demostrar que no existen.
Cabe señalar que en algunos casos esto puede ser imposible, como en el problema de las 8 reinas con un tablero de 1000 casillas: todo depende de la complejidad algorítmica o del problema de detención.
Sin embargo, en cualquier caso se obtendrá una de tres respuestas: el programa es correcto, incorrecto, o no se pudo calcular la respuesta.
En caso de no poder encontrar una respuesta, a menudo se pueden reformular las partes confusas del programa, reduciendo su complejidad algorítmica, para poder obtener una respuesta concreta de sí o no.
La verificación formal se aplica, por ejemplo, en el núcleo de Windows y en los sistemas operativos de drones de Darpa, para garantizar el máximo nivel de protección.
Utilizaremos Z3Prover, una herramienta muy potente para la prueba automatizada de teoremas y la solución de ecuaciones.
De hecho, Z3 resuelve ecuaciones, en lugar de simplemente probar sus valores mediante fuerza bruta.
Esto significa que es capaz de encontrar una respuesta, incluso en casos donde las combinaciones de entradas son 10^100.
Y eso son solo alrededor de una docena de argumentos de entrada tipo Integer, algo que a menudo se encuentra en la práctica.
El problema de las 8 reinas (tomado de un manual en 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 las reinas es comparable a un programa que toma como entrada las coordenadas de 8 reinas y devuelve una respuesta sobre si se atacan entre ellas.
Si tuviéramos que resolver este programa mediante verificación formal, en comparación con la tarea, solo tendríamos que realizar un paso más en convertir el código del programa en una ecuación: esta sería esencialmente idéntica a la nuestra (por supuesto, siempre que el programa esté libre de errores).
Prácticamente lo mismo sucederá en el caso de búsqueda de vulnerabilidades: simplemente definimos las condiciones de salida que necesitamos, por ejemplo, la contraseña de administrador, convertimos el código fuente o descompilado en ecuaciones compatibles con la verificación y luego obtenemos la respuesta sobre qué datos deben ser introducidos para alcanzar el objetivo.
En mi opinión, el problema del lobo, la cabra y la col es aún más interesante, ya que su solución requiere muchos (7) pasos.
Si el problema de las reinas es comparable a un caso en el que se puede acceder al servidor mediante una única solicitud GET o POST, el lobo, la cabra y la col muestra un ejemplo de una categoría mucho más compleja y común, donde los objetivos solo se pueden alcanzar con varias solicitudes.
Esto es comparable, por ejemplo, a un escenario donde es necesario encontrar una inyección SQL, escribir un archivo a través de ella, luego elevar privilegios y solo después obtener la contraseña.
Condiciones del problema y su soluciónEl agricultor necesita transportar un lobo, una cabra y una col a través del río. El agricultor tiene un bote que solo puede llevar, además de él mismo, un objeto. El lobo se comerá a la cabra y la cabra se comerá la col si el agricultor las deja desatendidas.
La solución es que en el cuarto paso, el agricultor tendrá que llevar la cabra de vuelta.
Ahora procedamos a resolverlo de forma programática.
Designaremos al agricultor, al lobo, a la cabra y a la col como 4 variables que solo pueden tomar el valor de 0 o 1. Cero significa que están en la orilla 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) ]
# Cada criatura solo puede estar en la izquierda (0) o en la derecha (1) en cada estado
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 solucionar el problema. Cada paso representa un estado del río, el bote y todas las entidades.
Por ahora, elijámoslo al azar y con un margen, tomemos 10.
Cada entidad se presenta 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 estableceremos las condiciones donde el lobo se come a la cabra, o la cabra se come la col, como restricciones en la ecuación.
(En la presencia del 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 finalmente, plantearemos todas las posibles acciones del granjero al cruzar hacia allá o de vuelta.
Él puede llevar consigo al lobo, la cabra o la col, o no llevar a nadie, o siquiera no navegar en absoluto.
Por supuesto, sin el granjero, nadie puede cruzar.
Esto se expresará en que cada estado siguiente del río, la balsa y las entidades pueden diferir del anterior solo de una manera estrictamente limitada.
No más de 2 bits, y con muchos otros límites, ya que el granjero solo puede transportar una entidad a la vez y no todos pueden ser dejados juntos.
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) ]
Iniciemos la solución.
solve(Side + Start + Finish + Safe + Travel)
¡Y obtenemos la respuesta!
Z3 encontró un conjunto de estados que es consistente y satisface todas las condiciones.
Una especie de molde cuatridimensional del espacio-tiempo.
Vamos a entender qué ocurrió.
Vemos que al final todos cruzaron, solo que al principio nuestro granjero decidió descansar y no navegó en los primeros 2 pasos.
Human_2 = 0
Human_3 = 0
Esto indica que el número de estados que elegimos es excesivo, y 8 será más que suficiente.
En nuestro caso, el granjero actuó así: inicio, descanso, descanso, cruce de la cabra, retorno, cruce de la col, regreso con la cabra, cruce del lobo, vuelta solo, entrega de la cabra nuevamente.
Pero al final, el problema se resolvió.
#Старт.
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 esto, haremos que nuestro lobo sea herbívoro, y querrá comerse la col.
Esto se puede comparar con un caso en el que nuestro objetivo es proteger la aplicación y debemos asegurarnos de que no haya vulnerabilidades.
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:
sin solución
Esto significa que realmente no hay soluciones.
De este modo, hemos demostrado programáticamente la imposibilidad de cruzar con un lobo omnívoro, sin pérdidas para el agricultor.
Si la audiencia considera este tema interesante, en futuros artículos explicaré cómo transformar un programa o función convencional en una ecuación compatible con métodos formales, y resolverla, descubriendo así tanto todos los escenarios legítimos como las vulnerabilidades. Primero con este mismo problema, pero presentado ya en forma de programa, y luego aumentando gradualmente la complejidad y pasando a ejemplos relevantes del mundo del desarrollo de software.
El siguiente artículo ya está listo:
En él, paso de la verificación formal de problemas a programas, y describo,
cómo se pueden convertir automáticamente en sistemas de reglas formales.
Fuente: habr.com
