Meiner Meinung nach ist das Thema der formalen Verifikation im russischsprachigen Internet nicht ausreichend behandelt, und es fehlen insbesondere einfache und anschauliche Beispiele.
Ich werde ein solches Beispiel aus einer ausländischen Quelle anführen und es mit einer eigenen Lösung des bekannten Problems der Überfahrt von Wolf, Ziege und Kohl auf die andere Seite des Flusses ergänzen.
Aber zunächst werde ich kurz skizzieren, was die formale Verifikation ist und wozu sie benötigt wird.
Unter formaler Verifikation versteht man in der Regel die Überprüfung eines Programms oder Algorithmus mit Hilfe eines anderen.
Dies ist notwendig, um sicherzustellen, dass das Verhalten des Programms dem Erwarteten entspricht und um dessen Sicherheit zu gewährleisten.
Die formale Verifikation ist das leistungsstärkste Mittel zur Entdeckung und Beseitigung von Schwachstellen: Sie ermöglicht es, alle vorhandenen Sicherheitslücken und Fehler im Programm zu finden oder zu beweisen, dass es diese nicht gibt.
Es sei darauf hingewiesen, dass dies in einigen Fällen unmöglich sein kann, wie zum Beispiel bei dem Problem der 8 Damen auf einem 1000-Felder-Brett: hier stößt man auf algorithmische Komplexität oder das Halteproblem.
In jedem Fall wird jedoch eine der drei Antworten erzielt: Das Programm ist korrekt, inkorrekt oder es war nicht möglich, eine Antwort zu berechnen.
Im Falle der Unmöglichkeit, eine Antwort zu finden, kann man oft die unklaren Teile des Programms überarbeiten, um ihre algorithmische Komplexität zu verringern, um eine konkrete Antwort ja oder nein zu erhalten.
Formale Verifikation wird beispielsweise im Windows-Kernel und in den Betriebssystemen von Darpa-Drohnen eingesetzt, um das höchstmögliche Schutzniveau zu gewährleisten.
Wir werden Z3Prover verwenden, ein sehr leistungsfähiges Tool für automatisierte Beweisführung von Theoremen und zur Lösung von Gleichungen.
Z3 löst tatsächlich Gleichungen und sucht nicht deren Werte mittels brutaler Bruteforce.
Das bedeutet, dass er auch in Fällen, in denen es 10^100 Kombinationen von Eingabevarianten gibt, eine Antwort finden kann.
Und das sind nur etwa ein Dutzend Eingabeargumente vom Typ Integer, was in der Praxis häufig vorkommt.
Das Problem der 8 Damen (entnommen aus dem englischsprachigen ).
# 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)
Nachdem wir Z3 gestartet haben, erhalten wir die Lösung:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Das Damenproblem ist vergleichbar mit einem Programm, das die Koordinaten von 8 Damen als Eingabe akzeptiert und die Antwort ausgibt, ob sich die Damen gegenseitig angreifen.
Wenn wir ein solches Programm mit formaler Verifikation lösen würden, müssten wir im Vergleich zu der Aufgabe einfach noch einen Schritt durch die Umwandlung des Programmcodes in eine Gleichung machen: diese wäre im Wesentlichen identisch mit unserer (natürlich vorausgesetzt, dass das Programm fehlerfrei geschrieben ist).
Praktisch wird dasselbe bei der Suche nach Schwachstellen geschehen: Wir definieren einfach die gewünschten Ausgabebedingungen, beispielsweise das Admin-Passwort, wandeln den ursprünglichen oder dekompilierten Code in mit der Verifikation kompatible Gleichungen um und erhalten dann die Antwort, welche Daten als Eingabe benötigt werden, um das Ziel zu erreichen.
Meiner Meinung nach ist die Aufgabe von Wolf, Ziege und Kohl noch interessanter, da für ihre Lösung bereits viele (7) Schritte notwendig sind.
Wenn die Aufgabe der Damen vergleichbar ist mit dem Szenario, in dem man durch eine einzige GET- oder POST-Anfrage auf den Server eindringen kann, demonstriert Wolf, Ziege und Kohl ein Beispiel aus einer weitaus komplexeren und verbreiteteren Kategorie, in der die Ziele nur durch mehrere Anfragen erreicht werden können.
Das ist beispielsweise vergleichbar mit einem Szenario, in dem man eine SQL-Injection finden, eine Datei darüber schreiben, dann seine Rechte erhöhen und erst dann das Passwort erhalten muss.
Aufgabenstellung und LösungDer Landwirt muss einen Wolf, eine Ziege und einen Kohl über den Fluss transportieren. Der Landwirt hat ein Boot, in dem neben dem Bauern nur ein Objekt Platz findet. Der Wolf frisst die Ziege, und die Ziege frisst den Kohl, wenn der Landwirt sie unbeaufsichtigt lässt.
Die Lösung besteht darin, dass der Landwirt die Ziege im 4. Schritt zurückbringen muss.
Nun beginnen wir mit der programmatischen Lösung.
Wir bezeichnen den Landwirt, den Wolf, die Ziege und den Kohl als 4 Variablen, die nur den Wert 0 oder 1 annehmen können. Null bedeutet, dass sie sich am linken Ufer befinden, und Eins bedeutet, dass sie sich am rechten Ufer befinden.
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) ]
# Jede Kreatur kann in jedem Zustand nur links (0) oder rechts (1) sein
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 – das ist die Anzahl der Schritte, die zur Lösung erforderlich sind. Jeder Schritt stellt einen Zustand des Flusses, des Boots und aller Wesen dar.
Wählen wir vorläufig zufällig und mit einem Puffer, nehmen wir 10.
Jede Entität ist in 10 Exemplaren vorhanden – das ist ihr Wert in jedem der 10 Schritte.
Nun legen wir die Bedingungen für den Start und das Ziel fest.
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 ]
Dann legen wir die Bedingungen fest, unter denen der Wolf die Ziege frisst oder die Ziege den Kohl, als Einschränkungen in der Gleichung.
(In Anwesenheit des Bauern ist Aggression unmöglich.)
# 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) ]
Und schließlich definieren wir alle möglichen Aktionen des Bauern beim Überqueren hin oder zurück.
Er kann den Wolf, die Ziege oder den Kohl mitnehmen, oder niemanden mitnehmen, oder überhaupt nicht fahren.
Natürlich kann ohne den Bauern niemand überqueren.
Dies wird dadurch ausgedrückt, dass sich jeder nachfolgende Zustand des Flusses, des Bootes und der Entitäten nur auf strikt begrenzte Weise vom vorherigen unterscheiden kann.
Nicht mehr als um 2 Einheiten und mit vielen anderen Einschränkungen, da der Bauer nur eine Entität auf einmal transportieren kann und nicht alle zusammen gelassen werden können.
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) ]
Lass uns die Lösung starten.
solve(Side + Start + Finish + Safe + Travel)
Und wir erhalten die Antwort!
Z3 hat eine konsistente und alle Bedingungen erfüllende Menge an Zuständen gefunden.
Eine Art vierdimensionaler Schnappschuss der Raum-Zeit.
Lasst uns herausfinden, was passiert ist.
Wir sehen, dass letztendlich alle überquert haben, nur dass unser Bauer zu Beginn beschlossen hat, sich auszuruhen, und in den ersten 2 Schritten nicht fährt.
Human_2 = 0
Human_3 = 0
Das sagt uns, dass die Anzahl der Zustände, die wir gewählt haben, überflüssig ist, und 8 vollkommen ausreichend sein wird.
In unserem Fall hat der Bauer so gehandelt: Start, Ruhe, Ruhe, Überfahrt der Ziege, Rückfahrt, Überfahrt des Kohls, Rückkehr mit der Ziege, Überfahrt des Wolfes, Rückfahrt allein, erneute Lieferung der Ziege.
Aber letztendlich ist das Problem gelöst.
#Старт.
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
Nun versuchen wir, die Bedingungen zu ändern und zu beweisen, dass es keine Lösungen gibt.
Dazu verleihen wir unserem Wolf Pflanzenfresserschaft, und er will den Kohl fressen.
Dies kann mit einem Fall verglichen werden, bei dem unser Ziel der Schutz der Anwendung ist, und wir müssen sicherstellen, dass es keine Schlupflöcher gibt.
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 gab uns die folgende Antwort:
keine Lösung
Das bedeutet, dass es tatsächlich keine Lösungen gibt.
So haben wir programmgesteuert die Unmöglichkeit der Überfahrt mit einem alles fressenden Wolf bewiesen, ohne Verluste für den Bauern.
Wenn das Publikum dieses Thema interessant findet, werde ich in zukünftigen Artikeln erklären, wie man ein gewöhnliches Programm oder eine Funktion in eine mit formalen Methoden kompatible Gleichung umwandelt und diese löst, wodurch sowohl legitime Szenarien als auch Schwachstellen entdeckt werden. Zuerst an dieser Aufgabe, aber bereits in Form eines Programms, und danach langsam komplizierter werden und aktuelle Beispiele aus der Softwareentwicklung behandeln.
Der nächste Artikel ist bereits fertig:
Darüber hinaus gehe ich von der formalen Verifizierung von Aufgaben zu Programmen über und beschreibe,
wie man diese automatisch in Systeme formaler Regeln umwandeln kann.
Quelle: habr.com
