A mio avviso, nel settore di lingua russa di Internet, il tema della verifica formale non è sufficientemente trattato e soprattutto mancano esempi semplici e chiari.
Darò un esempio tratto da una fonte straniera e aggiungerò la mia soluzione al noto problema di attraversare un lupo, una capra e un cavolo dall'altra parte del fiume.
Ma prima descriverò brevemente cos’è la verifica formale e perché è necessaria.
La verifica formale di solito significa controllare un programma o un algoritmo utilizzandone un altro.
Ciò è necessario per garantire che il programma si comporti come previsto e anche per garantirne la sicurezza.
La verifica formale è il mezzo più potente per trovare ed eliminare le vulnerabilità: consente di trovare tutti i buchi e i bug esistenti in un programma, o dimostrare che non esistono.
Vale la pena notare che in alcuni casi ciò è impossibile, come nel problema delle 8 regine con una larghezza della scacchiera di 1000 caselle: tutto si riduce alla complessità algoritmica o al problema dell'arresto.
In ogni caso si riceverà comunque una delle tre risposte: il programma è corretto, non è corretto oppure non è stato possibile calcolare la risposta.
Se è impossibile trovare una risposta, spesso è possibile rielaborare parti poco chiare del programma, riducendone la complessità algoritmica, al fine di ottenere una specifica risposta sì o no.
E la verifica formale viene utilizzata, ad esempio, nel kernel 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 risoluzione di equazioni.
Inoltre, Z3 risolve le equazioni e non seleziona i loro valori usando la forza bruta.
Ciò significa che è in grado di trovare la risposta, anche nei casi in cui sono presenti 10^100 combinazioni di opzioni di input.
Ma si tratta solo di una dozzina di argomenti di input di tipo Integer, e nella pratica si riscontra spesso.
Problema sulle 8 regine (tratto dall'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)
Eseguendo 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 della regina è paragonabile a un programma che prende come input le coordinate di 8 regine e restituisce la risposta se le regine si battono a vicenda.
Se dovessimo risolvere un programma del genere utilizzando la verifica formale, rispetto al problema, dovremmo semplicemente fare un passo in più sotto forma di conversione del codice del programma in un'equazione: risulterebbe essere essenzialmente identico al nostro ( ovviamente se il programma è stato scritto correttamente).
Quasi lo stesso accadrà nel caso della ricerca di vulnerabilità: impostiamo semplicemente le condizioni di output di cui abbiamo bisogno, ad esempio la password dell'amministratore, trasformiamo il codice sorgente o decompilato in equazioni compatibili con la verifica e quindi otteniamo una risposta su quali dati deve essere fornito come input per raggiungere l’obiettivo.
Secondo me il problema del lupo, della capra e del cavolo è ancora più interessante, poiché risolverlo richiede già molti (7) passaggi.
Se il problema della regina è paragonabile al caso in cui è possibile penetrare in un server utilizzando una singola richiesta GET o POST, allora il lupo, la capra e il cavolo rappresentano un esempio di una categoria molto più complessa e diffusa, in cui l'obiettivo può essere raggiunto solo da diverse richieste.
Ciò è paragonabile, ad esempio, a uno scenario in cui è necessario trovare un'iniezione SQL, scrivere un file al suo interno, quindi elevare i propri diritti e solo successivamente ottenere una password.
Condizioni del problema e sua soluzioneIl contadino deve trasportare un lupo, una capra e un cavolo attraverso il fiume. L'agricoltore ha una barca che può ospitare un solo oggetto, oltre all'agricoltore stesso. Il lupo mangerà la capra e la capra mangerà il cavolo se il contadino li lascia incustoditi.
La soluzione è che nella fase 4 l’agricoltore dovrà riprendersi la capra.
Ora iniziamo a risolverlo a livello di codice.
Indichiamo il contadino, il lupo, la capra e il cavolo come 4 variabili che assumono solo il valore 0 o 1. Zero significa che sono sulla riva sinistra e uno significa che sono 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) ]
# 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 è il numero di passaggi necessari per risolvere. Ogni passo rappresenta lo stato del fiume, della barca e di tutte le entità.
Per ora scegliamolo a caso e con un margine prendiamo 10.
Ogni entità è rappresentata in 10 copie: questo è il suo valore in ciascuno dei 10 passaggi.
Ora impostiamo le condizioni per la partenza e l'arrivo.
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 ]
Quindi impostiamo le condizioni in cui il lupo mangia la capra, o la capra mangia il cavolo, come vincoli nell'equazione.
(In presenza di un agricoltore l’aggressione è 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, definiremo tutte le possibili azioni dell'agricoltore durante la traversata di andata e ritorno.
Può portare con sé un lupo, una capra o un cavolo, oppure non portare nessuno, o non navigare affatto.
Naturalmente nessuno può attraversare senza un agricoltore.
Ciò sarà espresso dal fatto che ogni stato successivo del fiume, della barca e delle entità potrà differire dal precedente solo in modo strettamente limitato.
Non più di 2 bit, e con tanti altri limiti, visto che il farmer può trasportare solo una entità alla volta e non può essere lasciata tutta 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) ]
Eseguiamo la soluzione.
solve(Side + Start + Finish + Safe + Travel)
E otteniamo la risposta!
Z3 ha trovato un insieme coerente di stati che soddisfa tutte le condizioni.
Una sorta di calco quadridimensionale dello spazio-tempo.
Scopriamo cosa è successo.
Vediamo che alla fine tutti hanno attraversato, solo che all'inizio il nostro contadino ha deciso di riposarsi, e nei primi 2 passi non nuota da nessuna parte.
Human_2 = 0
Human_3 = 0
Ciò suggerisce che il numero di stati che abbiamo scelto è eccessivo e 8 saranno più che sufficienti.
Nel nostro caso il contadino ha fatto così: partenza, riposo, riposo, attraversare la capra, attraversare indietro, attraversare il cavolo, tornare con la capra, attraversare il lupo, tornare indietro da solo, riconsegnare la capra.
Ma alla fine il problema è stato 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 dimostriamo che non ci sono soluzioni.
Per fare questo, daremo al nostro lupo erbivoro e lui vorrà mangiare cavoli.
Questo può essere paragonato al caso in cui il nostro obiettivo è proteggere l'applicazione e dobbiamo assicurarci che non ci siano scappatoie.
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 dato la seguente risposta:
no solution
Vuol dire che davvero non ci sono soluzioni.
Pertanto, abbiamo dimostrato programmaticamente l'impossibilità di incrociare un lupo onnivoro senza perdite per l'agricoltore.
Se il pubblico trova questo argomento interessante, nei prossimi articoli ti dirò come trasformare un programma o una funzione ordinaria in un'equazione compatibile con metodi formali e risolverla, rivelando così sia tutti gli scenari legittimi che le vulnerabilità. Innanzitutto, sullo stesso compito, ma presentato sotto forma di programma, per poi complicarlo gradualmente e passare ad esempi attuali dal mondo dello sviluppo software.
Il prossimo articolo è già pronto:
In esso passo dalla verifica formale dei problemi ai programmi, e li descrivo
come possono essere convertiti automaticamente in sistemi di regole formali.
Fonte: habr.com