🥇Formele verifikasie oor die voorbeeld van die wolf-, bok- en koolprobleem

Na my mening, in die Russiessprekende sektor van die internet, word die onderwerp van formele verifikasie nie genoeg gedek nie, en veral is daar nie genoeg eenvoudige en illustratiewe voorbeelde nie.

Ek sal so 'n voorbeeld uit 'n vreemde bron gee, en my eie oplossing byvoeg vir die bekende probleem om 'n wolf, bok en kool na die ander kant van die rivier oor te steek.

Maar eers sal ek kortliks beskryf wat formele verifikasie is en hoekom dit nodig is.

Formele verifikasie word gewoonlik verstaan as die verifikasie van een program of algoritme met behulp van 'n ander.

Dit is nodig om seker te maak dat die gedrag van die program soos verwag is, asook om die veiligheid daarvan te verseker.

Formele verifikasie is die kragtigste hulpmiddel om kwesbaarhede te vind en uit te skakel: dit laat jou toe om alle bestaande gate en foute in die program te vind, of om te bewys dat hulle nie bestaan nie.
Dit is opmerklik dat dit in sommige gevalle onmoontlik is, soos byvoorbeeld in die probleem van 8 koninginne met 'n bordwydte van 1000 selle: alles berus op die algoritmiese kompleksiteit of die stopprobleem.

In elk geval sal een van drie antwoorde egter ontvang word: die program is korrek, verkeerd, of dit was nie moontlik om die antwoord te bereken nie.

As dit onmoontlik is om 'n antwoord te vind, is dit dikwels moontlik om die obskure dele van die program te herwerk deur hul algoritmiese kompleksiteit te verminder om 'n spesifieke ja of nee antwoord te kry.

En formele verifikasie word byvoorbeeld gebruik in die Windows-kern en bedryfstelsels van Darpa drones, om die maksimum vlak van beskerming te verseker.

Ons sal Z3Prover gebruik, 'n baie kragtige hulpmiddel vir outomatiese stellingbewys en vergelykingsoplossing.

Boonop los Z3 net die vergelykings op en kies nie hul waardes met brute krag nie.
Dit beteken dat dit die antwoord kan vind, selfs in gevalle waar die kombinasies van invoeropsies en 10^100.

Maar dit gaan net oor 'n dosyn invoerargumente van tipe Heelgetal, en dit kom dikwels in die praktyk voor.

Die probleem van 8 koninginne (Geneem uit die Engelse handleiding).

# 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)

Met Z3, kry ons die oplossing:

[Q_5 = 1,
 Q_8 = 7,
 Q_3 = 8,
 Q_2 = 2,
 Q_6 = 3,
 Q_4 = 6,
 Q_7 = 5,
 Q_1 = 4]

Die probleem oor queens is vergelykbaar met 'n program wat die koördinate van 8 queens as invoer neem en die antwoord gee of die queens mekaar klop.

As ons so 'n program sou oplos deur formele verifikasie te gebruik, sou ons in vergelyking met die probleem eenvoudig nog 'n stap moet neem in die vorm van die omskakeling van die programkode in 'n vergelyking: dit sou blykbaar in wese identies aan ons s'n wees ( natuurlik, as die program sonder foute geskryf is).

Amper dieselfde ding sal gebeur in die geval van soek na kwesbaarhede: ons stel net die uitvoervoorwaardes wat ons benodig, byvoorbeeld die administrateur wagwoord, transformeer die bron of gedekompileerde kode in vergelykings wat versoenbaar is met verifikasie, en kry dan 'n antwoord oor watter data insette moet word om die doel te bereik.

Na my mening is die wolf-, bok- en koolprobleem selfs interessanter, aangesien dit baie (7) stappe verg om dit op te los.

As die probleem van koninginne vergelykbaar is met die geval waar jy die bediener kan binnedring met 'n enkele GET- of POST-versoek, dan wys die wolf, bok en kool 'n voorbeeld uit 'n baie meer komplekse en algemene kategorie, waarin die doel bereik kan word met slegs 'n paar versoeke.

Dit is byvoorbeeld vergelykbaar met 'n scenario waar jy 'n SQL-inspuiting moet vind, 'n lêer daardeur moet skryf, dan jou regte verhoog, en dan eers 'n wagwoord moet kry.

Toestande van die probleem en die oplossing daarvanDie boer moet 'n wolf, 'n bok en 'n kool oor die rivier vervoer. Die boer het 'n boot wat net een voorwerp kan pas buiten die boer self. Die wolf sal die bok eet en die bok sal die kool eet as die boer hulle sonder toesig los.

Die antwoord is dat die boer in stap 4 die bok moet terugneem.
Kom ons begin nou om programmaties op te los.

Kom ons wys 'n boer, 'n wolf, 'n bok en 'n kool aan as 4 veranderlikes wat slegs 'n waarde van 0 of 1 neem. Nul beteken dat hulle op die linkeroewer is, en een beteken dat hulle aan die regterkant is.

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

Getal is die aantal stappe wat nodig is om op te los. Elke stap verteenwoordig die toestand van die rivier, die boot en alle entiteite.

Kom ons kies dit vir eers lukraak en met 'n marge, neem 10.

Elke entiteit word in 10 gevalle verteenwoordig - dit is sy waarde by elk van die 10 stappe.

Kom ons stel nou die voorwaardes vir die begin en einde.

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 ]

Dan stel ons voorwaardes waar die wolf die bok eet, of die bokkool, as beperkings in die vergelyking.
(In die teenwoordigheid van 'n boer is aggressie onmoontlik)

# 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) ]

En laastens, kom ons definieer al die moontlike optrede van die boer wanneer hy daarheen of terug gaan.
Hy kan óf 'n wolf, 'n bok of 'n kool saamneem, óf niemand vat nie, óf nêrens heen gaan nie.

Natuurlik kan niemand oorsteek sonder 'n boer nie.

Dit sal uitgedruk word deur die feit dat elke volgende toestand van die rivier, boot en entiteite slegs op 'n streng beperkte manier van die vorige een kan verskil.

Nie meer as 2 stukkies nie, en met baie ander perke, aangesien die boer net een essensie op 'n slag kan vervoer en nie almal saam gelos kan word nie.

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) ]

Kom ons voer die oplossing uit.

solve(Side + Start + Finish + Safe + Travel)

En ons kry die antwoord!

Z3 het 'n konsekwente en bevredigende stel state gevind.
'n Soort vierdimensionele rolverdeling van ruimte-tyd.

Kom ons vind uit wat gebeur het.

Ons sien op die ou end het almal gekruis, net aan die begin het ons boer besluit om te rus, en hy swem nêrens op die eerste 2 trappe nie.

Human_2 = 0
Human_3 = 0

Dit dui daarop dat ons 'n buitensporige aantal state gekies het, en 8 sal genoeg wees.

In ons geval het die boer dit gedoen: begin, rus, rus, veer die bok, veer terug, veer die kool, keer terug met die bok, veer die wolf, keer terug alleen, lewer die bok weer af.

Maar op die ou end is die probleem opgelos.

#Старт.
 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

Kom ons probeer nou die voorwaardes verander en bewys dat daar geen oplossings is nie.

Om dit te doen, sal ons ons wolf met herbivore toeken, en hy sal kool wil eet.
Dit kan vergelyk word met 'n saak waarin ons doel is om die aansoek te beskerm en ons moet seker maak dat daar geen skuiwergate is nie.

 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 het vir ons die volgende reaksie gegee:

 no solution

Dit beteken dat daar werklik geen oplossings is nie.

So het ons programmaties die onmoontlikheid van kruising met 'n omnivore wolf bewys, sonder verlies vir die boer.

As die gehoor hierdie onderwerp interessant vind, sal ek jou in toekomstige artikels vertel hoe om 'n gewone program of funksie te omskep in 'n vergelyking wat versoenbaar is met formele metodes, en dit op te los en sodoende beide wettige scenario's en kwesbaarhede te openbaar. Eerstens, op dieselfde taak, maar reeds aangebied in die vorm van 'n program, en dan geleidelik gekompliseer en voort te gaan na werklike voorbeelde uit die wêreld van sagteware-ontwikkeling.

Die volgende artikel is gereed:
Skep 'n formele verifikasiestelsel van nuuts af: Skryf 'n simboliese VM in PHP en Python

Daarin beweeg ek van formele verifikasie van probleme, na programme, en beskryf,
hoe jy dit outomaties in stelsels van formele reëls kan omskep.

Bron: will.com

Formele verifikasie oor die voorbeeld van die wolf-, bok- en koolprobleem

Voeg 'n opmerking Kanselleer antwoord