Al meu entendre, al sector d'Internet en llengua russa, el tema de la verificació formal no està prou cobert, i hi ha especialment una manca d'exemples senzills i clars.
Posaré un exemple de font estrangera, i afegiré la meva pròpia solució al conegut problema de travessar un llop, una cabra i una col a l'altra banda del riu.
Però primer, descriuré breument què és la verificació formal i per què és necessària.
La verificació formal normalment significa comprovar un programa o algorisme amb un altre.
Això és necessari per garantir que el programa es comporta com s'espera i també per garantir la seva seguretat.
La verificació formal és el mitjà més potent per trobar i eliminar vulnerabilitats: permet trobar tots els forats i errors existents en un programa, o demostrar que no existeixen.
Val la pena assenyalar que en alguns casos això és impossible, com en el problema de 8 reines amb una amplada de tauler de 1000 quadrats: tot es redueix a la complexitat algorítmica o al problema de l'aturada.
Tanmateix, en qualsevol cas, es rebrà una de les tres respostes: el programa és correcte, incorrecte o no s'ha pogut calcular la resposta.
Si és impossible trobar una resposta, sovint és possible reelaborar parts poc clares del programa, reduint la seva complexitat algorítmica, per tal d'obtenir una resposta específica sí o no.
I la verificació formal s'utilitza, per exemple, al nucli de Windows i als sistemes operatius de drons Darpa, per garantir el màxim nivell de protecció.
Utilitzarem Z3Prover, una eina molt potent per a la demostració automatitzada de teoremes i la resolució d'equacions.
A més, Z3 resol equacions i no selecciona els seus valors amb força bruta.
Això vol dir que és capaç de trobar la resposta, fins i tot en els casos en què hi ha 10^100 combinacions d'opcions d'entrada.
Però només es tracta d'una dotzena d'arguments d'entrada de tipus Integer, i això es troba sovint a la pràctica.
Problema sobre 8 reines (pres de l'anglè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)
Executant Z3, obtenim la solució:
[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 és comparable a un programa que pren com a entrada les coordenades de 8 reines i dóna la resposta si les reines es guanyen entre elles.
Si haguéssim de resoldre aquest programa mitjançant la verificació formal, en comparació amb el problema, simplement hauríem de fer un pas més en forma de convertir el codi del programa en una equació: resultaria essencialment idèntic al nostre ( és clar, si el programa està escrit correctament).
Gairebé el mateix passarà en el cas de la recerca de vulnerabilitats: només establim les condicions de sortida que necessitem, per exemple, la contrasenya de l'administrador, transformem el codi font o descompilat en equacions compatibles amb la verificació, i després obtenim una resposta sobre què Les dades s'han de subministrar com a entrada per assolir l'objectiu.
Al meu entendre, el problema del llop, la cabra i la col és encara més interessant, ja que resoldre'l ja requereix molts (7) passos.
Si el problema de la reina és comparable al cas en què podeu penetrar en un servidor mitjançant una única sol·licitud GET o POST, aleshores el llop, la cabra i la col mostra un exemple d'una categoria molt més complexa i estesa, en la qual només es pot aconseguir l'objectiu. per diverses peticions.
Això és comparable, per exemple, a un escenari en què necessiteu trobar una injecció SQL, escriure-hi un fitxer, elevar els vostres drets i només després obtenir una contrasenya.
Condicions del problema i la seva solucióEl pagès necessita transportar un llop, una cabra i una col a través del riu. El pagès té una barca que només pot acollir un objecte, a més del propi pagès. El llop es menjarà la cabra i la cabra es menjarà la col si el pagès les deixa sense vigilància.
La solució és que al pas 4 l'agricultor haurà de recuperar la cabra.
Ara comencem a resoldre-ho amb programació.
Denotem el pagès, el llop, la cabra i la col com a 4 variables que prenen el valor només 0 o 1. Zero vol dir que estan a la riba esquerra, i una que estan a la dreta.
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 és el nombre de passos necessaris per resoldre. Cada pas representa l'estat del riu, el vaixell i totes les entitats.
De moment, triem-lo a l'atzar i amb un marge, agafem 10.
Cada entitat està representada en 10 còpies: aquest és el seu valor en cadascun dels 10 passos.
Ara posem les condicions per a l'inici i l'acabament.
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 ]
A continuació, establim les condicions en què el llop es menja la cabra, o la cabra menja la col, com a restriccions de l'equació.
(En presència d'un pagès, l'agressió és impossible)
# 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) ]
I finalment, definirem totes les accions possibles del pagès a l'hora de creuar cap allà o tornar.
Pot endur-se un llop, una cabra o una col, o no endur-se ningú, o no navegar enlloc.
Per descomptat, ningú pot creuar sense un pagès.
Això s'expressarà pel fet que cada estat posterior del riu, vaixell i entitats només pot diferir de l'anterior d'una manera estrictament limitada.
No més de 2 bits, i amb molts altres límits, ja que el pagès només pot transportar una entitat alhora i no es poden deixar totes juntes.
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) ]
Executem la solució.
solve(Side + Start + Finish + Safe + Travel)
I tenim la resposta!
Z3 va trobar un conjunt consistent d'estats que satisfà totes les condicions.
Una mena de repartiment de quatre dimensions de l'espai-temps.
Anem a esbrinar què va passar.
Veiem que al final tothom es va creuar, només al principi el nostre pagès va decidir descansar, i als 2 primers passos no neda enlloc.
Human_2 = 0
Human_3 = 0
Això suggereix que el nombre d'estats que hem escollit és excessiu i que 8 serà suficient.
En el nostre cas, el pagès va fer això: començar, descansar, descansar, creuar la cabra, creuar enrere, creuar la col, tornar amb la cabra, creuar el llop, tornar sol, tornar a lliurar la cabra.
Però al final el problema es va solucionar.
#Старт.
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
Ara intentem canviar les condicions i demostrar que no hi ha solucions.
Per fer-ho, donarem herbívor al nostre llop, i ell voldrà menjar col.
Això es pot comparar amb el cas en què el nostre objectiu és assegurar l'aplicació i hem d'assegurar-nos que no hi hagi llacunes.
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 ens va donar la següent resposta:
no solution
Vol dir que realment no hi ha solucions.
Així, vam demostrar programàticament la impossibilitat d'encreuar-se amb un llop omnívor sense pèrdues per al pagès.
Si l'audiència troba aquest tema interessant, en articles futurs us explicaré com convertir un programa o funció normal en una equació compatible amb mètodes formals i resoldre'l, revelant així tots els escenaris i vulnerabilitats legítims. Primer, sobre la mateixa tasca, però presentada en forma de programa, per després anar complicant-la progressivament i passant a exemples actuals del món del desenvolupament de programari.
El següent article ja està llest:
En ell passo de la verificació formal de problemes als programes, i descric
com es poden convertir automàticament en sistemes de regles formals.
Font: www.habr.com