A mio avviso, nel settore della rete di lingua russa, il tema della verifica formale è insufficientemente trattato, e mancano in particolare esempi semplici e chiari.
Porterò un esempio da una fonte straniera e completerò con la mia soluzione a un problema noto sul trasporto di un lupo, una capra e del cavolo dall'altra parte del fiume.
Ma prima descriverò brevemente cosa sia la verifica formale e a cosa serva.
Con verifica formale si intende generalmente la verifica di un programma o di un algoritmo tramite un altro.
Questo è necessario per assicurarsi che il comportamento del programma corrisponda alle aspettative e per garantirne la sicurezza.
La verifica formale è il mezzo più potente per individuare e risolvere vulnerabilità: permette di trovare tutte le falle e i bug esistenti nel programma, oppure di dimostrare che non ce ne sono.
Va notato che in alcuni casi questo è impossibile, come nel problema delle 8 regine su una scacchiera larga 1000 celle: tutto dipende dalla complessità algoritmica o dal problema dell'arresto.
Tuttavia, in ogni caso, si otterrà una delle tre risposte: il programma è corretto, non è corretto, oppure non è stato possibile calcolare la risposta.
In caso di impossibilità di trovare una risposta, spesso è possibile rielaborare le parti poco chiare del programma, riducendo la loro complessità algoritmica, per ottenere una risposta specifica sì o no.
La verifica formale è utilizzata, ad esempio, nel kernel di Windows e nei sistemi operativi dei droni Darpa, per garantire il massimo livello di sicurezza.
Utilizzeremo Z3Prover, uno strumento molto potente per la dimostrazione automatizzata di teoremi e la risoluzione di equazioni.
E Z3 risolve effettivamente le equazioni, anziché cercare i loro valori tramite brute force.
Ciò significa che è in grado di trovare la risposta, anche in casi in cui le combinazioni delle opzioni di input siano 10^100.
E questo è solo circa una dozzina di argomenti di input di tipo Integer, e situazioni simili si incontrano spesso nella pratica.
Il problema degli 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)
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 accetta le coordinate di 8 regine e restitusce una risposta se le regine si colpiscono a vicenda.
Se risolvessimo un tale programma usando la verifica formale, rispetto al problema, avremmo solo bisogno di fare un ulteriore passo per trasformare il codice del programma in un'equazione: essa sarebbe essenzialmente identica alla nostra (ovviamente, se il programma è scritto senza errori).
Praticamente lo stesso avverrebbe nel caso della ricerca di vulnerabilità: noi poniamo semplicemente le condizioni di uscita necessarie, ad esempio la password dell'amministratore, trasformiamo il codice sorgente o decompilato in equazioni compatibili con la verifica e poi otteniamo una 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é per risolverlo sono necessari molti passi (7).
Se il problema delle regine è paragonabile a uno scenario in cui si può accedere al server con una sola richiesta GET o POST, allora il problema del lupo, della capra e del cavolo rappresenta un esempio di una categoria molto più complessa e comune, in cui gli obiettivi possono essere raggiunti solo attraverso più richieste.
Questo è paragonabile, ad esempio, a uno scenario in cui è necessario trovare un'iniezione SQL, scrivere un file tramite essa, poi elevare i propri privilegi e solo allora ottenere la password.
Le condizioni del problema e la sua soluzioneIl contadino deve trasportare attraverso il fiume un lupo, una capra e un cavolo. Il contadino ha una barca che può contenere, oltre a lui stesso, solo un oggetto. Il lupo mangerà la capra, e la capra mangerà il cavolo se il contadino li lascia incustoditi.
La soluzione è che al quarto passaggio il contadino dovrà riportare indietro la capra.
Ora cominciamo a risolverlo in modo programmatico.
Denotiamo il contadino, il lupo, la capra e il cavolo come 4 variabili, che possono assumere solo i valori 0 o 1. Zero indica che si trovano sulla riva sinistra, mentre uno indica 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ò essere 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 scegliamolo a caso e con un margine, prendiamo 10.
Ogni entità è rappresentata in 10 esemplari — questo è il suo valore in ciascuno dei 10 passi.
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 definiamo le condizioni in cui il lupo mangia la capra, o la capra la verza, 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 nel trasporto avanti e indietro.
Può infatti portare con sé il lupo, la capra o la verza, oppure non portare nessuno, o non andare affatto.
È ovvio che senza il contadino nessuno può attraversare.
Questo sarà espresso dal fatto che ogni stato successivo del fiume, della barca e degli oggetti può differire dal precedente solo in modo rigorosamente limitato.
Non più di 2 bit, e con molte altre limitazioni, dato che il contadino può trasportare solo un oggetto 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])) per i in range(Num-1) ]
Avviamo la soluzione.
solve(Side + Start + Finish + Safe + Travel)
E abbiamo la risposta!
Z3 ha trovato una coerenza e un insieme di stati che soddisfano tutte le condizioni.
Una sorta di impronta quadridimensionale dello spazio-tempo.
Scopriamo cosa è successo.
Abbiamo osservato che tutti hanno attraversato, ma inizialmente il nostro contadino ha deciso di riposare e non è andato da nessuna parte nei primi 2 passi.
Human_2 = 0
Human_3 = 0
Ciò indica che il numero di stati che abbiamo scelto è eccessivo, e 8 sono più che sufficienti.
Nel nostro caso, il contadino ha proceduto così: partenza, riposo, riposo, attraversamento della capra, ritorno, attraversamento del cavolo, ritorno con la capra, attraversamento del lupo, ritorno da solo, consegna della 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 dimostrare che non ci sono soluzioni.
Per questo dotiamo il nostro lupo di erbivorismo, e lui vorrà mangiare il cavolo.
Questo può essere paragonato al 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
Significa che davvero non ci sono soluzioni.
Così, abbiamo dimostrato programmaticamente l'impossibilità dell'attraversamento con un lupo onnivoro, senza perdite per il contadino.
Se il pubblico trova questo argomento interessante, nei prossimi articoli spiegherò come trasformare un normale programma o funzione in un'equazione conforme ai metodi formali e risolverla, scoprendo così sia scenari legittimi che vulnerabilità. Inizierò con lo stesso compito, ma presentato come programma, per poi gradualmente rendere le cose più complesse e passare a esempi pertinenti dal mondo dello sviluppo software.
Il prossimo articolo è già pronto:
In esso passo dalla verifica formale dei compiti ai programmi e descrivo
come è possibile convertirli automaticamente in sistemi di regole formali.
Fonte: habr.com
