Meiner Meinung nach wird im russischsprachigen Bereich des Internets das Thema der formalen Verifizierung nicht ausreichend behandelt und es mangelt vor allem an einfachen und anschaulichen Beispielen.
Ich werde ein Beispiel aus einer ausländischen Quelle geben und meine eigene Lösung für das bekannte Problem hinzufügen, einen Wolf, eine Ziege und einen Kohl auf die andere Seite des Flusses zu bringen.
Zunächst möchte ich jedoch kurz beschreiben, was eine formelle Verifizierung ist und warum sie erforderlich ist.
Formale Verifizierung bedeutet normalerweise, dass ein Programm oder ein Algorithmus mithilfe eines anderen Programms oder Algorithmus überprüft wird.
Dies ist notwendig, um sicherzustellen, dass sich das Programm wie erwartet verhält und um seine Sicherheit zu gewährleisten.
Die formale Verifizierung ist das wirksamste Mittel zum Auffinden und Beseitigen von Schwachstellen: Sie ermöglicht es Ihnen, alle vorhandenen Lücken und Fehler in einem Programm zu finden oder zu beweisen, dass sie nicht vorhanden sind.
Es ist erwähnenswert, dass dies in manchen Fällen unmöglich ist, wie zum Beispiel beim Problem von 8 Damen mit einer Spielbrettbreite von 1000 Feldern: Alles hängt von der Komplexität des Algorithmus oder dem Stoppproblem ab.
In jedem Fall erhält man jedoch eine von drei Antworten: Das Programm ist richtig, falsch oder die Antwort konnte nicht berechnet werden.
Wenn keine Antwort gefunden werden kann, ist es oft möglich, unklare Programmteile zu überarbeiten und ihre algorithmische Komplexität zu reduzieren, um eine konkrete Ja- oder Nein-Antwort zu erhalten.
Und formale Verifizierung wird beispielsweise im Windows-Kernel und in den Drohnen-Betriebssystemen Darpa eingesetzt, um ein Höchstmaß an Schutz zu gewährleisten.
Wir werden Z3Prover verwenden, ein sehr leistungsfähiges Tool zum automatisierten Beweisen von Theoremen und zum Lösen von Gleichungen.
Darüber hinaus löst Z3 Gleichungen und wählt ihre Werte nicht mit roher Gewalt aus.
Dies bedeutet, dass die Antwort auch dann gefunden werden kann, wenn es 10^100 Kombinationen von Eingabemöglichkeiten gibt.
Dabei handelt es sich jedoch nur um etwa ein Dutzend Eingabeargumente vom Typ Integer, was in der Praxis häufig vorkommt.
Aufgabe über 8 Königinnen (aus dem Englischen übernommen ).
# 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)
Wenn wir Z3 ausführen, 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 verwendet und die Antwort ausgibt, ob die Damen sich gegenseitig schlagen.
Wenn wir ein solches Programm durch formale Verifizierung lösen würden, müssten wir im Vergleich zum Problem lediglich einen weiteren Schritt in Form der Umwandlung des Programmcodes in eine Gleichung unternehmen: Es würde sich herausstellen, dass dieser im Wesentlichen mit unserem identisch ist ( natürlich, wenn das Programm korrekt geschrieben wurde).
Bei der Suche nach Schwachstellen passiert fast das Gleiche: Wir legen lediglich die Ausgabebedingungen fest, die wir benötigen, beispielsweise das Administratorkennwort, wandeln den Quell- oder dekompilierten Code in mit der Überprüfung kompatible Gleichungen um und erhalten dann eine Antwort, was Um das Ziel zu erreichen, müssen Daten als Eingabe bereitgestellt werden.
Meiner Meinung nach ist das Problem mit dem Wolf, der Ziege und dem Kohl sogar noch interessanter, da zu seiner Lösung bereits viele (7) Schritte erforderlich sind.
Wenn das Queen-Problem mit dem Fall vergleichbar ist, in dem man mit einer einzigen GET- oder POST-Anfrage in einen Server eindringen kann, dann ist „Wolf, Ziege und Kohl“ ein Beispiel aus einer viel komplexeren und weiter verbreiteten Kategorie, in der das Ziel nur erreicht werden kann auf mehrere Anfragen hin.
Dies ist beispielsweise vergleichbar mit einem Szenario, in dem Sie eine SQL-Injection finden, eine Datei darüber schreiben, dann Ihre Rechte erhöhen und erst dann ein Passwort erhalten müssen.
Bedingungen des Problems und seiner LösungDer Bauer muss einen Wolf, eine Ziege und Kohl über den Fluss transportieren. Der Bauer verfügt über ein Boot, das außer ihm selbst nur einen Gegenstand aufnehmen kann. Der Wolf frisst die Ziege und die Ziege frisst den Kohl, 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 mit der programmgesteuerten Lösung.
Bezeichnen wir den Bauer, 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 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) ]
# 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 zur Lösung erforderlichen Schritte. Jeder Schritt repräsentiert den Zustand des Flusses, des Bootes und aller Einheiten.
Wählen wir es zunächst zufällig aus und nehmen wir mit einem Spielraum 10.
Jede Entität wird in 10 Kopien dargestellt – dies ist ihr Wert bei jedem der 10 Schritte.
Legen wir nun 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 fest, unter denen der Wolf die Ziege frisst oder die Ziege den Kohl frisst, als Einschränkungen in der Gleichung.
(In Anwesenheit eines Landwirts 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 Landwirts bei der Hin- und Rücküberquerung.
Er kann entweder einen Wolf, eine Ziege oder einen Kohl mitnehmen oder niemanden mitnehmen oder überhaupt nicht segeln.
Natürlich kann niemand ohne einen Bauern überqueren.
Dies kommt dadurch zum Ausdruck, dass sich jeder nachfolgende Zustand des Flusses, Bootes und der Entitäten nur in streng begrenzter Weise vom 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 belassen 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) ]
Lassen Sie uns die Lösung ausführen.
solve(Side + Start + Finish + Safe + Travel)
Und wir bekommen die Antwort!
Z3 hat eine konsistente Menge von Zuständen gefunden, die alle Bedingungen erfüllen.
Eine Art vierdimensionaler Abdruck der Raumzeit.
Lassen Sie uns herausfinden, was passiert ist.
Wir sehen, dass am Ende alle überquert haben, nur unser Bauer hat sich zunächst entschieden, sich auszuruhen, und auf den ersten beiden Schritten schwimmt er nirgendwo hin.
Human_2 = 0
Human_3 = 0
Dies deutet darauf hin, dass die Anzahl der von uns ausgewählten Staaten zu hoch ist und 8 völlig ausreichen werden.
In unserem Fall hat der Bauer Folgendes getan: Anlaufen, ausruhen, ausruhen, die Ziege überqueren, zurück überqueren, den Kohl überqueren, mit der Ziege zurückkehren, den Wolf überqueren, allein zurückkommen, die Ziege erneut abgeben.
Aber am Ende war 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 geben wir unserem Wolf Pflanzenfresser, und er wird Kohl essen wollen.
Dies kann mit dem Fall verglichen werden, in dem unser Ziel die Sicherung der Anwendung ist und wir sicherstellen müssen, 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
Das bedeutet, dass es wirklich keine Lösungen gibt.
Damit haben wir programmatisch die Unmöglichkeit einer Kreuzung mit einem Allesfresserwolf ohne Verluste für den Landwirt bewiesen.
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, wodurch sowohl alle legitimen Szenarien als auch Schwachstellen aufgedeckt werden. Zuerst die gleiche Aufgabe, aber in Form eines Programms präsentiert, dann nach und nach verkomplizieren und zu aktuellen Beispielen aus der Welt der Softwareentwicklung übergehen.
Der nächste Artikel ist bereits fertig:
Darin gehe ich von der formalen Überprüfung von Problemen zu Programmen über und beschreibe sie
wie können sie automatisch in formale Regelsysteme umgewandelt werden?
Source: habr.com