A mio avviso, nel settore di internet di lingua russa, il tema della verifica formale è trattato in modo insufficiente, e manca in particolare esempi semplici e chiari.
Farò un esempio da una fonte straniera e lo integrerò con la mia soluzione a un noto problema del trasporto del lupo, della capra e del cavolo dall'altra parte del fiume.
Ma prima descriverò brevemente cosa sia la verifica formale e a cosa serva.
Per verifica formale si intende generalmente la verifica di un programma o di un algoritmo mediante un altro.
Questo è necessario per assicurarsi che il comportamento del programma corrisponda a quello previsto e per garantire la sua sicurezza.
La verifica formale è il mezzo più potente per cercare e correggere vulnerabilità: permette di trovare tutte le falle e i bug esistenti nel programma, oppure dimostrare che non ce ne sono.
Va notato che in alcuni casi questo è impossibile, come nel problema delle 8 regine con una scacchiera larga 1000 celle: tutto dipende dalla complessità algoritmica o dal problema dell'arresto.
Tuttavia, in ogni caso si avrà una delle tre risposte: il programma è corretto, non è corretto, oppure — non è stato possibile calcolare la risposta.
Nel caso in cui non sia possibile trovare una risposta, spesso è possibile rielaborare i punti non chiari del programma, riducendo la loro complessità algoritmica, per ottenere una risposta concreta sì o no.
La verifica formale è applicata, ad esempio, nel kernel di Windows e nei sistemi operativi dei droni Darpa, per garantire il massimo livello di protezione.
Utilizzeremo Z3Prover, uno strumento molto potente per la dimostrazione automatizzata di teoremi e la soluzione di equazioni.
Infatti, Z3 risolve effettivamente le equazioni, invece di cercarne i valori tramite brute force.
Questo significa che è in grado di trovare una risposta, anche in casi in cui le combinazioni delle variabili di input siano 10^100.
E ciò è solo una dozzina di argomenti in tipo Integer, e situazioni simili si incontrano spesso in pratica.
Il problema delle 8 regine (tratto da un manuale in lingua inglese) ).
# 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)
Avviando Z3, otteniamo la soluzione:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Il problema delle regine è paragonabile a un programma che riceve in input le coordinate di 8 regine e restituisce la risposta se le regine si attaccano a vicenda.
Se stessimo affrontando un programma del genere attraverso la verifica formale, avremmo semplicemente bisogno di compiere un ulteriore passo nella trasformazione del codice del programma in un'equazione: essa risulterebbe sostanzialmente identica alla nostra (ovviamente, se il programma è stato scritto senza errori).
Praticamente lo stesso accadrà nel caso di ricerca di vulnerabilità: dobbiamo solo specificare le condizioni di uscita desiderate, ad esempio la password dell'amministratore, trasformiamo il codice sorgente o decompilato in equazioni compatibili con la verifica e poi otteniamo la risposta su quali dati devono essere forniti come input per raggiungere l'obiettivo.
A mio avviso, il problema del lupo, della capra e del cavolo è ancora più interessante, poiché la sua soluzione richiede già molti (7) passi.
Se il problema delle regine è paragonabile a un caso in cui è possibile accedere al server mediante una semplice richiesta GET o POST, il lupo, la capra e il cavolo rappresentano un esempio di una categoria molto più complessa e diffusa, in cui gli obiettivi possono essere raggiunti solo con diverse richieste.
Questo è paragonabile, ad esempio, a uno scenario in cui è necessario trovare una SQL injection, scrivere un file attraverso di essa, poi elevare i propri diritti e solo dopo ottenere la password.
Condizioni del problema e sua risoluzioneIl contadino deve trasportare attraverso il fiume un lupo, una capra e un cavolo. Il contadino ha una barca che può ospitare, oltre a lui stesso, solo un oggetto. Il lupo mangerebbe la capra, e la capra mangerebbe il cavolo, se il contadino li lasciasse incustoditi.
La soluzione è che al quarto passo il contadino dovrà riportare indietro la capra.
Ora procediamo alla soluzione in modo programmatico.
Indichiamo il contadino, il lupo, la capra e il cavolo come quattro variabili che possono assumere solo i valori 0 o 1. Zero significa che si trovano sulla riva sinistra, e uno significa che si trovano sulla riva destra.
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) ]
# Ogni creatura può trovarsi solo a sinistra (0) o a destra (1) in ogni stato
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 — è il numero di passi necessari per risolvere. Ogni passo rappresenta uno stato del fiume, della barca e di tutte le entità.
Per ora lo sceglieremo a caso e con margine, prendendo 10.
Ogni entità è rappresentata in 10 esemplari: questo è il suo valore in ciascuno dei 10 passaggi.
Ora definiamo le condizioni per l'inizio e la fine.
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 ]
Poi definiremo le condizioni in cui il lupo mangia la capra, o la capra mangia il cavolo, come vincoli nell'equazione.
(In presenza del contadino l'aggressività è impossibile)
# 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 infine, definiamo tutte le possibili azioni del contadino durante il viaggio di andata o ritorno.
Può portare con sé il lupo, la capra o il cavolo, oppure non portare nessuno, o non andare affatto.
Naturalmente, senza il contadino nessuno può attraversare.
Questo sarà espresso dal fatto che ogni stato successivo del fiume, della barca e delle entità può differire da quello precedente solo in modo rigorosamente limitato.
Non più di 2 bit, e con molte altre limitazioni, dato che il contadino può trasportare solo una entità alla volta e non tutti possono essere lasciati insieme.
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) ]
Avviamo la soluzione.
solve(Side + Start + Finish + Safe + Travel)
E otteniamo la risposta!
Z3 ha trovato una combinazione di stati coerente e che soddisfa tutte le condizioni.
Una sorta di impronta spaziotemporale quadridimensionale.
Vediamo cosa è successo.
Vediamo che alla fine tutti sono stati trasferiti, solo che all'inizio il nostro contadino ha deciso di riposare e nei primi 2 passaggi non ha navigato.
Human_2 = 0
Human_3 = 0
Questo indica che il numero di stati scelto è eccessivo, e 8 è più che sufficiente.
Nel nostro caso, il contadino ha agito in questo modo: avvio, riposo, riposo, trasferimento della capra, ritorno, trasferimento del cavolo, ritorno con la capra, trasferimento del lupo, ritorno da solo, trasferimento ripetuto della capra.
Ma alla fine il problema è risolto.
#Старт.
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
Ora proviamo a cambiare le condizioni e dimostrare che non ci sono soluzioni.
Per fare ciò, daremo al nostro lupo la capacità di mangiare, e vorrà mangiare il cavolo.
Questo può essere paragonato a un caso in cui il nostro obiettivo è la protezione dell'applicazione e dobbiamo assicurarci che non ci siano falle.
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 ci ha fornito la seguente risposta:
nessuna soluzione
Ciò significa che non ci sono effettivamente soluzioni.
Pertanto, abbiamo dimostrato in modo programmatico l'impossibilità di attraversare con il lupo onnivoro, senza perdite per il contadino.
Se il pubblico riterrà interessante questo argomento, nei prossimi articoli racconterò come trasformare un programma o una funzione ordinaria in un'equazione compatibile con i metodi formali e risolverla, scoprendo così sia tutti gli scenari legittimi che le vulnerabilità. Inizialmente affrontando questo stesso problema, ma presentato già come programma, e successivamente complicando gradualmente passando ad esempi concreti nel mondo dello sviluppo software.
Il prossimo articolo è già pronto:
In esso passo dalla verifica formale di problemi, ai programmi, e descrivo,
come è possibile convertirli in sistemi di regole formali in modo automatico.
Fonte: habr.com
