Meiner Meinung nach wird im russischsprachigen Bereich des Internets das Thema der formalen Überprüfung nicht ausreichend behandelt, und es fehlen besonders einfache und klare Beispiele.
Ich werde ein solches Beispiel aus einer fremden Quelle geben und meine eigene Lösung für das bekannte Problem des Transports eines Wolfes, einer Ziege und eines Kohls auf die andere Seite des Flusses ergänzen.
Aber zuerst werde ich kurz beschreiben, was formale Überprüfung ist und warum sie benötigt wird.
Formale Überprüfung bedeutet normalerweise, ein Programm oder einen Algorithmus mit einem anderen zu überprüfen.
Dies ist notwendig, um sicherzustellen, dass das Verhalten des Programms wie erwartet ist, und um seine Sicherheit zu gewährleisten.
Die formale Überprüfung ist das leistungsstärkste Tool zum Auffinden und Beseitigen von Schwachstellen: Sie können alle vorhandenen Lücken und Fehler im Programm finden oder nachweisen, dass sie nicht vorhanden sind.
Es ist erwähnenswert, dass dies in einigen Fällen unmöglich ist, beispielsweise beim Problem von 8 Königinnen mit einer Brettbreite von 1000 Zellen: Alles hängt von der algorithmischen Komplexität oder dem Problem des Stoppens ab.
In jedem Fall wird jedoch eine der drei Antworten empfangen: Das Programm ist korrekt, falsch oder die Antwort konnte nicht berechnet werden.
Wenn es unmöglich ist, eine Antwort zu finden, ist es oft möglich, dunkle Stellen im Programm zu verarbeiten und deren algorithmische Komplexität zu verringern, um eine bestimmte Antwort zu erhalten, ja oder nein.
Die formale Überprüfung wird beispielsweise in den Betriebssystemen Windows-Kernel und Darpa-Drohnen verwendet, um ein Höchstmaß an Schutz zu gewährleisten.
Wir werden Z3Prover verwenden, ein sehr leistungsfähiges Werkzeug zum automatisierten Beweis von Theoremen und zum Lösen von Gleichungen.
Darüber hinaus löst Z3 die Gleichungen genau und wählt ihre Werte nicht mit roher Gewalt aus.
Dies bedeutet, dass er die Antwort auch in Fällen finden kann, in denen Kombinationen von Eingabeoptionen und 10 ^ 100 vorliegen.
Dies sind jedoch nur etwa ein Dutzend Eingabeargumente vom Typ Integer, die in der Praxis häufig vorkommen.
Das Problem von 8 Königinnen (entnommen aus dem englischen
Handbuch ).
# 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)
Mit Z3 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 Königinproblem ist vergleichbar mit einem Programm, das die Koordinaten von 8 Königinnen aufnimmt und die Antwort anzeigt, wenn sich die Königinnen gegenseitig schlagen.
Wenn wir ein solches Programm mithilfe einer formalen Überprüfung lösen würden, müssten wir im Vergleich zur Aufgabe nur einen weiteren Schritt in Form der Konvertierung des Programmcodes in eine Gleichung unternehmen: Es würde sich als im Wesentlichen identisch mit unserem herausstellen (natürlich, wenn das Programm korrekt geschrieben wurde).
Fast das Gleiche passiert bei der Suche nach Schwachstellen: Wir legen nur die Ausgabebedingungen fest, die wir benötigen, z. B. das Administratorkennwort, konvertieren den Quellcode oder den dekompilierten Code in mit der Überprüfung kompatible Gleichungen und erhalten dann die Antwort, welche Daten eingegeben werden müssen, um das Ziel zu erreichen.
Meiner Meinung nach ist das Problem von Wolf, Ziege und Kohl noch interessanter, da bereits viele (7) Schritte erforderlich sind, um es zu lösen.
Wenn die Aufgabe der Königinnen mit der Option vergleichbar ist, dass Sie mit einer GET- oder POST-Anfrage in den Server eindringen können, zeigen Wolf, Ziege und Kohl ein Beispiel aus einer viel komplexeren und weit verbreiteten Kategorie, in der nur wenige Anfragen erreicht werden können.
Dies ist beispielsweise mit dem Szenario vergleichbar, in dem Sie die SQL-Injection suchen, eine Datei durch sie schreiben, dann Ihre Rechte erhöhen und erst dann das Kennwort erhalten müssen.
Problembedingungen und deren LösungDer Bauer muss den Wolf, die Ziege und den Kohl über den Fluss transportieren. Der Bauer hat ein Boot, in das nur ein Gegenstand passen kann, außer der Bauer selbst. Der Wolf wird die Ziege essen, und die Ziege wird Kohl essen, wenn der Bauer sie unbeaufsichtigt lässt.
Die Lösung besteht darin, dass der Landwirt in Schritt 4 die Ziege zurücknehmen muss.
Beginnen wir nun programmgesteuert mit der Lösung.
Wir bezeichnen den Bauern, den Wolf, die Ziege und den Kohl als 4 Variablen, die nur den Wert 0 oder 1 annehmen. Null bedeutet, dass sie sich am linken Ufer befinden, und einer 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) ] # 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 ist die Anzahl der Schritte, die zur Lösung benötigt werden. Jeder Schritt ist ein Zustand eines Flusses, eines Bootes und aller Einheiten.
Wählen Sie es zunächst nach dem Zufallsprinzip aus und nehmen Sie mit einem Rand 10.
Jede Entität wird in 10 Kopien dargestellt - dies ist ihr Wert in jedem der 10 Schritte.
Jetzt legen wir die Bedingungen für Start und 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, unter denen der Wolf die Ziege oder den Ziegenkohl frisst, als Einschränkungen in der Gleichung fest.
(In Anwesenheit des Landwirts ist eine Aggression nicht mö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 fragen wir den Landwirt nach allen möglichen Handlungen, wenn er dorthin oder zurück zieht.
Er kann entweder einen Wolf, eine Ziege oder einen Kohl mitnehmen oder niemanden mitnehmen oder gar nirgendwo hingehen.
Natürlich kann niemand ohne einen Bauern überqueren.
Dies wird durch die Tatsache zum Ausdruck gebracht, dass sich jeder nachfolgende Zustand des Flusses, des Bootes und der Einheiten nur in streng begrenzter Weise von dem vorherigen unterscheiden kann.
Nicht mehr als 2 Bits und mit vielen anderen Einschränkungen, da der Landwirt jeweils nur eine Entität 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) ]
Führen Sie die Lösung aus.
solve(Side + Start + Finish + Safe + Travel)
Und wir bekommen die Antwort!
Z3 fand einen konsistenten und zufriedenstellenden Satz von Bedingungen.
Eine Art vierdimensionale Besetzung von Raum-Zeit.
Mal sehen, was passiert ist.
Wir sehen, dass am Ende alle überquerten, nur am Anfang entschied sich unser Bauer, sich zu entspannen und schwimmt in den ersten beiden Schritten nirgendwo.
Human_2 = 0 Human_3 = 0
Dies deutet darauf hin, dass die Anzahl der von uns gewählten Staaten zu hoch ist und 8 völlig ausreichen wird.
In unserem Fall hat der Bauer Folgendes getan: Starten, Ausruhen, Ausruhen, Überqueren der Ziege, Zurückkreuzen, Überqueren von Kohl, Zurückkehren mit der Ziege, Überqueren des Wolfs, Zurückkehren allein, erneutes Ausliefern der Ziege.
Aber am Ende 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
Versuchen wir nun, die Bedingungen zu ändern und zu beweisen, dass es keine Lösungen gibt.
Dazu werden wir unseren Wolf mit Pflanzenfressern ausstatten, und er wird Kohl essen wollen.
Dies kann mit dem Fall verglichen werden, in dem unser Ziel darin besteht, die Anwendung zu schützen, und wir müssen sicherstellen, dass es keine Lücken 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 folgende Antwort:
no solution
Es bedeutet, dass es wirklich keine Lösungen gibt.
So haben wir programmatisch bewiesen, dass es unmöglich ist, mit einem alles fressenden Wolf ohne Verluste für den Landwirt zu kreuzen.
Wenn das Publikum dieses Thema interessant findet, werde ich Ihnen in zukünftigen Artikeln erklären, wie Sie ein gewöhnliches Programm oder eine gewöhnliche Funktion in eine mit formalen Methoden kompatible Gleichung umwandeln und lösen können, um sowohl alle legitimen Szenarien als auch Schwachstellen aufzudecken. Zunächst zur gleichen Aufgabe, aber bereits in Form eines Programms vorgestellt, dann schrittweise erschwerend und relevant zu relevanten Beispielen aus der Welt der Softwareentwicklung.
Der folgende Artikel ist fertig:
Erstellen eines formalen Verifizierungssystems von Grund auf neu: Wir schreiben eine Zeichen-VM in PHP und PythonDarin gehe ich von der formalen Überprüfung von Aufgaben zu Programmen und beschreibe
wie man sie automatisch in formale Regelsysteme umwandelt.