Na miña opinión, no sector en lingua rusa de Internet, o tema da verificación formal non está suficientemente tratado, e hai especialmente unha falta de exemplos sinxelos e claros.
Poñerei un exemplo de fonte estranxeira, e engadirei a miña propia solución ao coñecido problema de cruzar un lobo, unha cabra e un repolo ao outro lado do río.
Pero primeiro, describirei brevemente que é a verificación formal e por que é necesaria.
A verificación formal normalmente significa comprobar un programa ou algoritmo usando outro.
Isto é necesario para garantir que o programa se comporta como se espera e tamén para garantir a súa seguridade.
A verificación formal é o medio máis poderoso para atopar e eliminar vulnerabilidades: permítelle atopar todos os buracos e erros existentes nun programa ou demostrar que non existen.
Cabe sinalar que nalgúns casos isto é imposible, como no problema de 8 damas cun ancho de taboleiro de 1000 cadrados: todo se reduce á complexidade algorítmica ou ao problema de parar.
Non obstante, en calquera caso, recibirase unha das tres respostas: o programa é correcto, incorrecto ou non foi posible calcular a resposta.
Se é imposible atopar unha resposta, moitas veces é posible reelaborar partes pouco claras do programa, reducindo a súa complexidade algorítmica, para obter unha resposta específica de si ou non.
E a verificación formal utilízase, por exemplo, no núcleo de Windows e nos sistemas operativos de drones Darpa, para garantir o máximo nivel de protección.
Usaremos Z3Prover, unha ferramenta moi poderosa para a demostración automatizada de teoremas e a resolución de ecuacións.
Ademais, Z3 resolve ecuacións e non selecciona os seus valores usando a forza bruta.
Isto significa que é capaz de atopar a resposta, mesmo nos casos nos que hai 10^100 combinacións de opcións de entrada.
Pero só se trata dunha ducia de argumentos de entrada de tipo Enteiro, e isto adoita atoparse na práctica.
Problema sobre 8 reinas (Tomado do 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)
Executando Z3, obtemos a 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]
O problema da raíña é comparable a un programa que toma como entrada as coordenadas de 8 raíñas e dá a resposta se as raíñas se vencen entre si.
Se resolvésemos un programa deste tipo mediante a verificación formal, entón en comparación co problema, simplemente necesitaríamos dar un paso máis en forma de converter o código do programa nunha ecuación: resultaría esencialmente idéntico ao noso ( claro, se o programa foi escrito correctamente).
Case o mesmo ocorrerá no caso da busca de vulnerabilidades: só establecemos as condicións de saída que necesitamos, por exemplo, o contrasinal do administrador, transformamos o código fonte ou descompilado en ecuacións compatibles coa verificación e despois obtemos unha resposta sobre o que Os datos deben proporcionarse como entrada para acadar o obxectivo.
Na miña opinión, o problema do lobo, a cabra e o repolo é aínda máis interesante, xa que resolvelo xa require moitos (7) pasos.
Se o problema da raíña é comparable ao caso no que se pode penetrar nun servidor mediante unha única solicitude GET ou POST, entón o lobo, a cabra e o repolo mostran un exemplo dunha categoría moito máis complexa e estendida, na que o obxectivo só se pode alcanzar. por varias solicitudes.
Isto é comparable, por exemplo, a un escenario no que necesitas atopar unha inxección SQL, escribir un ficheiro a través dela, elevar os teus dereitos e só despois obter un contrasinal.
Condicións do problema e a súa soluciónO granxeiro necesita transportar un lobo, unha cabra e un repolo polo río. O labrego ten un barco que só pode acomodar un obxecto, ademais do propio labrego. O lobo comerá a cabra e a cabra comerá o repolo se o labrego os deixa desatendidos.
A solución é que no paso 4 o gandeiro terá que levar a cabra de volta.
Agora imos comezar a resolvelo mediante programación.
Denotemos o labrego, o lobo, a cabra e o repolo como 4 variables que toman o valor só 0 ou 1. O cero significa que están na marxe esquerda, e unha significa que están na dereita.
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 é o número de pasos necesarios para resolver. Cada paso representa o estado do río, do barco e de todas as entidades.
De momento, escollémolo ao chou e cunha marxe, tome 10.
Cada entidade está representada en 10 copias: este é o seu valor en cada un dos 10 pasos.
Agora imos establecer as condicións para o comezo e o 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 ]
Despois establecemos as condicións nas que o lobo come a cabra ou a cabra come o repolo, como restricións na ecuación.
(En presenza dun agricultor, a agresión é 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) ]
E por último, definiremos todas as accións posibles do gandeiro ao cruzar alí ou voltar.
Pode levar consigo un lobo, unha cabra ou un repolo, ou non levar a ninguén, ou non navegar por ningún lado.
Por suposto, ninguén pode cruzar sen labrego.
Isto expresarase polo feito de que cada estado posterior do río, barco e entidades pode diferir do anterior só de forma estritamente limitada.
Non máis de 2 bits, e con moitos outros límites, xa que o gandeiro só pode transportar unha entidade á vez e non se poden deixar todas xuntas.
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) ]
Imos executar a solución.
solve(Side + Start + Finish + Safe + Travel)
E temos a resposta!
Z3 atopou un conxunto consistente de estados que satisface todas as condicións.
Unha especie de elenco cuatridimensional do espazo-tempo.
Imos descubrir o que pasou.
Vemos que ao final todos se cruzaron, só ao principio o noso labrego decidiu descansar, e nos 2 primeiros pasos non nada nada.
Human_2 = 0
Human_3 = 0
Isto suxire que o número de estados que eliximos é excesivo e que 8 serán suficientes.
No noso caso, o gandeiro facía isto: comezar, descansar, descansar, cruzar a cabra, cruzar cara atrás, cruzar a verza, volver coa cabra, cruzar o lobo, volver só, volver a entregar a cabra.
Pero ao final o problema quedou solucionado.
#Старт.
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
Agora intentemos cambiar as condicións e demostrar que non hai solucións.
Para iso, darémoslle herbívoro ao noso lobo, e quererá comer repolo.
Isto pódese comparar co caso no que o noso obxectivo é protexer a aplicación e temos que asegurarnos de que non hai lagoas.
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 deunos a seguinte resposta:
no solution
Significa que realmente non hai solucións.
Así, demostramos programáticamente a imposibilidade de cruzarnos cun lobo omnívoro sen perdas para o gandeiro.
Se o público considera interesante este tema, en artigos futuros contarei como converter un programa ou función común nunha ecuación compatible con métodos formais e resolvelo, revelando así todos os escenarios lexítimos e vulnerabilidades. Primeiro, sobre a mesma tarefa, pero presentado en forma de programa, para despois complicalo pouco a pouco e pasar a exemplos actuais do mundo do desenvolvemento de software.
O seguinte artigo xa está listo:
Nel paso da verificación formal de problemas a programas, e describo
como se poden converter en sistemas de regras formais automaticamente.
Fonte: www.habr.com