Meiner Meinung nach wird das Thema der formalen Verifikation im russischsprachigen Internetbereich nicht ausreichend behandelt, und es fehlen insbesondere einfache und anschauliche Beispiele.
Ich werde ein Beispiel aus einer ausländischen Quelle anführen und mit meiner eigenen Lösung des bekannten Problems der Überquerung von Wolf, Ziege und Kohl auf die andere Seite des Flusses ergänzen.
Doch zunächst werde ich kurz umreißen, was formale Verifikation ist und wozu sie dient.
Unter formaler Verifikation versteht man in der Regel die Überprüfung eines Programms oder Algorithmus mithilfe eines anderen.
Dies ist notwendig, um sicherzustellen, dass das Verhalten des Programms den Erwartungen entspricht und um dessen Sicherheit zu gewährleisten.
Formale Verifikation ist das wirkungsvollste Mittel zur Aufspürung und Beseitigung von Schwachstellen: Sie ermöglicht das Finden aller bestehenden Löcher und Bugs im Programm oder den Nachweis, dass es keine gibt.
Es ist zu beachten, dass dies in einigen Fällen unmöglich ist, wie zum Beispiel bei dem Problem der 8 Damen auf einem 1000 Felder breiten Schachbrett: Alles hängt von der algorithmischen Komplexität oder dem Halteproblem ab.
In jedem Fall wird eine der drei Antworten erhalten: Das Programm ist korrekt, inkorrekt oder es war nicht möglich, eine Antwort zu berechnen.
Wenn es nicht möglich ist, eine Antwort zu finden, kann häufig an den unklaren Stellen des Programms gearbeitet werden, indem deren algorithmische Komplexität reduziert wird, um eine konkrete Antwort von ja oder nein zu erhalten.
Formale Verifikation wird beispielsweise im Windows-Kernel und bei den Betriebssystemen der Darpa-Drohnen angewendet, um den höchsten Schutzgrad zu gewährleisten.
Wir werden Z3Prover verwenden, ein sehr leistungsstarkes Werkzeug zur automatisierten Beweissicherung und zur Lösung von Gleichungen.
Z3 löst tatsächlich Gleichungen und sucht ihre Werte nicht bruteforce-artig.
Das bedeutet, dass es in der Lage ist, Antworten zu finden, selbst wenn die Kombinationen der Eingangsvarianten 10^100 betragen.
Das sind nur etwa ein Dutzend Eingabeargumente vom Typ Integer, und solche Situationen treten in der Praxis häufig auf.
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 ähnelt einem Programm, das die Koordinaten von 8 Damen entgegennimmt und überprüft, ob sie einander bedrohen.
Wenn wir ein solches Programm mithilfe formaler Verifikation lösen würden, müssten wir im Vergleich zur Aufgabe nur noch einen zusätzlichen Schritt machen, indem wir den Programmcode in eine Gleichung umwandeln: Diese wäre im Grunde identisch mit unserer (vorausgesetzt, das Programm ist fehlerfrei geschrieben).
Fast das Gleiche geschieht beim Auffinden von Schwachstellen: Wir geben lediglich die benötigten Ausgabebedingungen an, zum Beispiel das Admin-Passwort, wandeln den Original- oder dekompilierten Code in verifikationskompatible Gleichungen um und erhalten dann die Antwort, welche Daten wir eingeben müssen, um das Ziel zu erreichen.
Meiner Meinung nach ist das Problem mit dem Wolf, der Ziege und dem Kohl noch interessanter, da für dessen Lösung bereits viele (7) Schritte notwendig sind.
Wenn das Problem der Damen vergleichbar ist mit einem Szenario, in dem man sich mit einer einzigen GET- oder POST-Anfrage auf einen Server zugreifen kann, dann zeigt die Geschichte von Wolf, Ziege und Kohl ein Beispiel aus einer weitaus komplexeren und verbreiteten Kategorie, in der die Ziele nur durch mehrere Anfragen erreicht werden können.
Das ist vergleichbar mit einem Szenario, in dem man eine SQL-Injection finden, über sie eine Datei hochladen, dann seine Rechte erhöhen und erst danach das Passwort erhalten muss.
Die Bedingungen der Aufgabe und ihre LösungDer Landwirt muss den Wolf, die Ziege und den Kohl über den Fluss bringen. Der Landwirt hat ein Boot, in dem neben ihm selbst nur ein Objekt Platz finden kann. 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 in Schritt 4 die Ziege zurückbringen muss.
Jetzt gehen wir zur programmatischen Lösung über.
Lassen Sie uns den Landwirt, den Wolf, die Ziege und den Kohl als 4 Variablen deklarieren, die nur die Werte 0 oder 1 annehmen können. Null bedeutet, dass sie sich am linken Ufer befinden, und Eins, dass sie am rechten Ufer sind.
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 entweder auf der linken (0) oder rechten Seite (1) in jedem Zustand 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 – ist die Anzahl der Schritte, die für die Lösung erforderlich sind. Jeder Schritt repräsentiert einen Zustand des Flusses, des Bootes und aller Entitäten.
Wählen wir ihn vorerst zufällig und großzügig, nehmen wir 10.
Jede Entität ist in 10 Exemplaren vertreten – dies ist ihr Wert in jedem der 10 Schritte.
Jetzt setzen 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 definieren wir die Bedingungen, unter denen der Wolf die Ziege frisst oder die Ziege das Gemüse angreift, 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 legen wir alle möglichen Aktionen des Bauern fest, wenn er hinüber oder zurück fährt.
Er kann den Wolf, die Ziege oder das Gemüse mitnehmen, oder auch niemanden, oder überhaupt nicht fahren.
Natürlich kann niemand ohne den Bauern überqueren.
Dies wird sich darin zeigen, dass jeder folgende Zustand des Flusses, des Bootes und der Entitäten nur auf streng begrenzte Weise vom vorherigen abweichen kann.
Nicht mehr als um 2 Bit und mit vielen anderen Grenzen, denn der Bauer kann jeweils nur eine Entität transportieren und nicht alle können zusammen gelassen werden.
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, alle Bedingungen erfüllende Menge von Zuständen gefunden.
Eine Art vierdimensionaler Abdruck von Raum-Zeit.
Lass uns herausfinden, was passiert ist.
Wir sehen, dass schließlich alle übergesetzt sind, aber zunächst wollte unser Bauer eine Pause machen und ist in den ersten zwei Schritten nicht weiter gefahren.
Human_2 = 0
Human_3 = 0
Das zeigt, dass wir eine überflüssige Anzahl an Zuständen gewählt haben, und 8 ist durchaus ausreichend.
In unserem Fall hat der Bauer so gehandelt: starten, Pause, Pause, Ziege übersetzen, zurückfahren, Kohl übersetzen, Rückkehr mit der Ziege, Wolf übersetzen, allein zurückkehren, Ziege erneut transportieren.
Am Ende ist die Aufgabe jedoch 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
Jetzt versuchen wir die Bedingungen zu ändern und zu beweisen, dass es keine Lösungen gibt.
Dazu statten wir unseren Wolf mit Pflanzenfresser-Eigenschaften aus, und er wird versuchen, den Kohl zu fressen.
Dies lässt sich mit dem Fall vergleichen, in dem unser Ziel der Schutz der Anwendung ist und wir sicherstellen müssen, 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 hat uns die folgende Antwort gegeben:
keine Lösung
Das bedeutet, dass es tatsächlich keine Lösungen gibt.
So haben wir programmatisch bewiesen, dass eine Überfahrt mit einem Allesfresser-Wolf ohne Verlust für den Bauern unmöglich ist.
Wenn das Publikum dieses Thema als interessant erachtet, werde ich in zukünftigen Artikeln erläutern, wie man ein gewöhnliches Programm oder eine Funktion in eine mit formalen Methoden kompatible Gleichung umwandelt und sie löst, um sowohl legitime Szenarien als auch Schwachstellen zu entdecken. Zuerst an derselben Aufgabe, jedoch bereits in Form eines Programms, und dann schrittweise komplexer werdend, bis wir relevante Beispiele aus der Softwareentwicklung erreichen.
Der nächste Artikel steht bereits bereit:
In diesem Artikel wechsle ich von der formalen Verifikation von Aufgaben zu Programmen und beschreibe,
wie man sie automatisch in Systeme formaler Regeln konvertieren kann.
Quelle: habr.com
