Menger Meenung no, am russeschsproochege Secteur vum Internet, ass d'Thema vun der formeller Verifizéierung net genuch ofgedeckt, an et feelt besonnesch einfach a kloer Beispiller.
Ech ginn e Beispill vun enger auslännescher Quell, a füügt meng eegen Léisung fir de bekannte Problem fir e Wollef, eng Geess an e Kabes op déi aner Säit vum Floss ze kräizen.
Awer als éischt wäert ech kuerz beschreiwen wat eng formell Verifikatioun ass a firwat et néideg ass.
Formell Verifikatioun heescht normalerweis ee Programm oder Algorithmus mat engem aneren ze kontrolléieren.
Dëst ass néideg fir sécherzestellen datt de Programm sech wéi erwaart behält an och fir seng Sécherheet ze garantéieren.
Formell Verifizéierung ass dat mächtegst Mëttel fir Schwachstelle ze fannen an ze eliminéieren: et erlaabt Iech all existent Lächer a Bugs an engem Programm ze fannen oder ze beweisen datt se net existéieren.
Et ass derwäert ze bemierken datt an e puer Fäll dëst onméiglech ass, sou wéi am Problem vun 8 Kinniginendag mat enger Brietbreet vun 1000 Quadraten: et geet alles op d'algorithmesch Komplexitéit oder d'Stoppproblem erof.
Wéi och ëmmer, eng vun dräi Äntwerte gëtt kritt: de Programm ass richteg, falsch oder et war net méiglech d'Äntwert ze berechnen.
Wann et onméiglech ass eng Äntwert ze fannen, ass et dacks méiglech onkloer Deeler vum Programm ëmzeschaffen, hir algorithmesch Komplexitéit ze reduzéieren, fir eng spezifesch Jo oder Nee Äntwert ze kréien.
A formell Verifikatioun gëtt benotzt, zum Beispill, am Windows Kernel an Darpa Drone Betribssystemer, fir de maximalen Schutzniveau ze garantéieren.
Mir wäerten Z3Prover benotzen, e ganz mächtegt Tool fir automatiséiert Theorem Beweis an Equatiounsléisung.
Ausserdeem léist Z3 Equatiounen, a wielt hir Wäerter net mat brute Kraaft.
Dëst bedeit datt et fäeg ass d'Äntwert ze fannen, och a Fäll wou et 10^100 Kombinatioune vun Inputoptiounen sinn.
Awer dëst ass nëmmen ongeféier eng Dosen Input Argumenter vum Typ Integer, an dëst gëtt dacks an der Praxis begéint.
Problem iwwer 8 Kinniginendag (aus Englesch geholl ).
# 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)
Lafen Z3, mir kréien d'Léisung:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
De Kinnigineproblem ass vergläichbar mat engem Programm deen d'Koordinate vun 8 Kinniginen als Input hëlt an d'Äntwert erausgëtt ob d'Kinniginnen sech géigesäiteg schloen.
Wa mir sou e Programm mat formeller Verifizéierung géife léisen, da misste mir am Verglach mam Problem einfach e Schrëtt méi maachen a Form vum Ëmwandlung vum Programmcode an eng Equatioun: et géif sech wesentlech identesch mat eisem erausstellen ( natierlech, wann de Programm richteg geschriwwe gouf).
Bal datselwecht geschitt am Fall vun der Sich no Schwachstelle: mir setzen just d'Ausgangsbedéngungen déi mir brauchen, zum Beispill d'Admin Passwuert, transforméieren d'Quell oder dekompiléierte Code an Equatioune kompatibel mat der Verifizéierung, a kréien dann eng Äntwert op wat Daten mussen als Input geliwwert ginn fir dat Zil z'erreechen.
Menger Meenung no ass de Problem iwwer de Wollef, de Geess an de Kabes nach méi interessant, well d'Léisung et scho vill (7) Schrëtt erfuerdert.
Wann d'Kinnigin Problem mam Fall vergläichbar ass wou Dir e Server mat enger eenzeger GET oder POST Ufro penetréiere kënnt, da weist de Wollef, Geess a Kabes e Beispill aus enger vill méi komplexer a verbreeter Kategorie, an där d'Zil nëmmen erreecht ka ginn duerch verschidde Ufroen.
Dëst ass vergläichbar, zum Beispill, mat engem Szenario wou Dir eng SQL-Injektioun muss fannen, e Fichier driwwer schreiwen, dann Är Rechter erhéijen an nëmmen dann e Passwuert kréien.
Konditioune vum Problem a seng LéisungDe Bauer muss e Wollef, eng Geess a Kabes iwwer de Floss transportéieren. De Bauer huet e Boot, deen nieft dem Bauer selwer nëmmen een Objet ophält. De Wollef ësst d'Geess an d'Geess ësst de Kabes, wann de Bauer se ouni Iwwerwaachung léisst.
D'Léisung ass datt am Schrëtt 4 de Bauer muss d'Geess zréck huelen.
Loosst eis et elo programmatesch léisen.
Loosst eis de Bauer, de Wollef, de Geess a de Kabes als 4 Variabelen bezeechnen, déi de Wäert nëmmen 0 oder 1 huelen. Null heescht datt se op der lénker Bank sinn, an een heescht datt se op der rietser sinn.
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 ass d'Zuel vun de Schrëtt déi néideg ass fir ze léisen. All Schrëtt representéiert den Zoustand vum Floss, d'Boot an all Entitéiten.
Fir elo, loosst eis et zoufälleg wielen a mat enger Marge, huelt 10.
All Entitéit ass an 10 Exemplare vertruede - dat ass säi Wäert op jiddereng vun den 10 Schrëtt.
Loosst eis elo d'Konditioune fir den Start an de Schluss setzen.
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 ]
Duerno setze mir d'Konditioune fest, wou de Wollef d' Geess ësst, oder d' Geess de Kabes ësst, als Contrainten an der Equatioun.
(A Präsenz vun engem Bauer ass Agressioun onméiglech)
# 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) ]
A schlussendlech wäerte mir all méiglech Handlunge vum Bauer definéieren beim Kräizgang do oder zréck.
Hien kann entweder e Wollef, eng Geess oder e Kabes mat sech huelen, oder kee Mënsch huelen, oder iwwerhaapt néierens segelen.
Natierlech kann keen ouni Bauer iwwerfueren.
Dëst gëtt duerch d'Tatsaach ausgedréckt datt all spéider Staat vum Floss, Boot an Entitéite vun der viregter nëmmen op eng strikt limitéiert Manéier ënnerscheede kënnen.
Net méi wéi 2 Bits, a mat villen anere Grenzen, well de Bauer kann nëmmen eng Entitéit gläichzäiteg transportéieren an net all zesummen gelooss ginn.
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) ]
Loosst d'Léisung lafen.
solve(Side + Start + Finish + Safe + Travel)
A mir kréien d'Äntwert!
Z3 fonnt eng konsequent Formatioun vun Staaten déi all Konditiounen zefridden.
Eng Aart vu véierdimensionalen Besetzung vu Raumzäit.
Loosst eis erausfannen wat geschitt ass.
Mir gesinn, datt um Enn jidderee gekräizt ass, nëmmen am Ufank huet eise Bauer decidéiert fir ze raschten, an an den éischten 2 Schrëtt schwëmmt hien néierens.
Human_2 = 0
Human_3 = 0
Dëst hindeit datt d'Zuel vun de Staaten déi mir gewielt hunn exzessiv ass, an 8 wäerte ganz genuch sinn.
An eisem Fall huet de Bauer dat gemaach: ufänken, raschten, raschten, d'Geess iwwerschreiden, d'Kräiz zréck, de Kabes, de Kabes zréck, de Wollef iwwer de Wollef, eleng zréck, d'Geess erëm ze liwweren.
Mä um Enn war de Problem geléist.
#Старт.
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
Loosst eis elo probéieren d'Konditiounen z'änneren an ze beweisen datt et keng Léisunge gëtt.
Fir dëst ze maachen, gi mir eise Wollef Kraiderbestëmmung, an hie wëll Kabes iessen.
Dëst kann mam Fall vergläicht ginn an deem eist Zil ass d'Applikatioun ze sécheren a mir musse sécherstellen datt et keng Schleifen gëtt.
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 huet eis déi folgend Äntwert ginn:
no solution
Et heescht datt et wierklech keng Léisunge gëtt.
Domat hu mir programmatesch d'Onméiglechkeet bewisen, mat engem omnivoresche Wollef ouni Verloschter fir de Bauer ze kräizen.
Wann d'Publikum dëst Thema interessant fënnt, da wäert ech Iech an zukünfteg Artikelen soen wéi Dir e gewéinleche Programm oder Funktioun an eng Equatioun verwandelt, déi mat formelle Methoden kompatibel ass, an et léisen, an doduerch all legitim Szenarie a Schwachstelle opzeweisen. Éischtens, op der selwechter Aufgab, awer a Form vun engem Programm presentéiert, an dann lues a lues komplizéiert a weidergespillt op aktuell Beispiller aus der Welt vun Software Entwécklung.
Den nächsten Artikel ass scho fäerdeg:
An et plënneren ech aus formell Verifizéierung vu Probleemer op Programmer, a beschreiwen
wéi kënne se automatesch an formell Regelsystemer ëmgewandelt ginn.
Source: will.com