Miaopinie, en la ruslingva sektoro de Interreto, la temo de formala kontrolado ne estas sufiĉe traktata, kaj precipe mankas simplaj kaj klaraj ekzemploj.
Mi donos ekzemplon el fremda fonto, kaj aldonos mian propran solvon al la konata problemo transiri lupon, kapron kaj brasikon al la alia bordo de la rivero.
Sed unue, mi mallonge priskribos kio estas formala konfirmo kaj kial ĝi estas bezonata.
Formala konfirmo kutime signifas kontroli unu programon aŭ algoritmon uzante alian.
Ĉi tio estas necesa por certigi, ke la programo kondutas kiel atendite kaj ankaŭ por certigi ĝian sekurecon.
Formala konfirmo estas la plej potenca rimedo por trovi kaj forigi vundeblecojn: ĝi permesas vin trovi ĉiujn ekzistantajn truojn kaj cimojn en programo, aŭ pruvi, ke ili ne ekzistas.
Rimarkindas, ke en iuj kazoj ĉi tio estas neebla, kiel en la problemo de 8 reĝinoj kun tabullarĝo de 1000 kvadratoj: ĉio dependas de algoritma komplekseco aŭ la halta problemo.
Tamen ĉiuokaze oni ricevos unu el tri respondoj: la programo estas ĝusta, malĝusta, aŭ ne eblis kalkuli la respondon.
Se estas neeble trovi respondon, estas ofte eble reverki neklarajn partojn de la programo, reduktante ilian algoritman kompleksecon, por akiri specifan jes aŭ nean respondon.
Kaj formala konfirmo estas uzata, ekzemple, en la Vindoza kerno kaj Darpa dronaj operaciumoj, por certigi la maksimuman nivelon de protekto.
Ni uzos Z3Prover, tre potenca ilo por aŭtomatigita teorema pruvo kaj ekvacia solvado.
Plie, Z3 solvas ekvaciojn, kaj ne elektas iliajn valorojn per krudforto.
Ĉi tio signifas, ke ĝi kapablas trovi la respondon, eĉ en kazoj kie estas 10^100 kombinaĵoj de enigo-opcioj.
Sed ĉi tio estas nur ĉirkaŭ dekduo da enigargumentoj de tipo Entjero, kaj ĉi tio estas ofte renkontata en la praktiko.
Problemo pri 8 reĝinoj (Prenite el la angla ).
# 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)
Kurante Z3, ni ricevas la solvon:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
La reĝinproblemo estas komparebla al programo kiu prenas kiel enigaĵon la koordinatojn de 8 reĝinoj kaj eligas la respondon ĉu la reĝinoj batas unu la alian.
Se ni solvus tian programon per formala konfirmo, tiam kompare kun la problemo, ni simple bezonus fari unu plian paŝon en la formo de konverti la programkodon en ekvacion: ĝi montrus esence identa al la nia ( kompreneble, se la programo estis skribita ĝuste).
Preskaŭ la sama afero okazos en la kazo de serĉado de vundeblecoj: ni nur agordas la eligkondiĉojn, kiujn ni bezonas, ekzemple la administran pasvorton, transformas la fonton aŭ malkompilitan kodon en ekvaciojn kongruajn kun konfirmo, kaj tiam ricevas respondon pri kio datumoj devas esti liveritaj kiel enigaĵo por atingi la celon.
Miaopinie, la problemo pri la lupo, la kapro kaj la brasiko estas eĉ pli interesa, ĉar solvi ĝin jam postulas multajn (7) paŝojn.
Se la reĝinproblemo estas komparebla al la kazo, kie vi povas penetri servilon uzante ununuran GET aŭ POST-peton, tiam la lupo, kapro kaj brasiko montras ekzemplon el multe pli kompleksa kaj disvastigita kategorio, en kiu la celo povas esti atingita nur. per pluraj petoj.
Ĉi tio estas komparebla, ekzemple, al scenaro, kie vi devas trovi SQL-injekton, skribi dosieron tra ĝi, poste altigi viajn rajtojn kaj nur tiam ricevi pasvorton.
Kondiĉoj de la problemo kaj ĝia solvoLa farmisto bezonas transporti lupon, kapron kaj brasikon trans la riveron. La farmisto havas boaton kiu povas alĝustigi nur unu objekton, krom la farmisto mem. La lupo manĝos la kapron kaj la kapro manĝos la brasikon, se la farmisto lasas ilin neprizorgitaj.
La solvo estas, ke en la paŝo 4 la farmisto devos repreni la kapron.
Nun ni komencu solvi ĝin programe.
Ni nomu la farmiston, lupon, kapron kaj brasikon kiel 4 variablojn, kiuj prenas la valoron nur 0 aŭ 1. Nulo signifas, ke ili estas sur la maldekstra bordo, kaj unu signifas, ke ili estas dekstre.
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 estas la nombro da paŝoj necesaj por solvi. Ĉiu paŝo reprezentas la staton de la rivero, la boato kaj ĉiuj entoj.
Nuntempe, ni elektu ĝin hazarde kaj kun marĝeno prenu 10.
Ĉiu ento estas reprezentita en 10 kopioj - ĉi tiu estas ĝia valoro ĉe ĉiu el la 10 paŝoj.
Nun ni starigu la kondiĉojn por la komenco kaj fino.
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 ]
Tiam ni starigas la kondiĉojn kie la lupo manĝas la kapron, aŭ la kapro manĝas la brasikon, kiel limojn en la ekvacio.
(En ĉeesto de farmisto, agreso estas neebla)
# 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) ]
Kaj fine, ni difinos ĉiujn eblajn agojn de la kamparano dum transiro tien aŭ reen.
Li povas aŭ kunporti lupon, kapron aŭ brasikon, aŭ ne preni iun ajn, aŭ tute ne veli ien.
Kompreneble, neniu povas transiri sen kamparano.
Ĉi tio estos esprimita per la fakto, ke ĉiu posta stato de la rivero, boato kaj entoj povas diferenci de la antaŭa nur en strikte limigita maniero.
Ne pli ol 2 bitoj, kaj kun multaj aliaj limoj, ĉar la farmisto povas nur transporti unu enton samtempe kaj ne ĉiuj povas esti lasitaj kune.
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) ]
Ni rulu la solvon.
solve(Side + Start + Finish + Safe + Travel)
Kaj ni ricevas la respondon!
Z3 trovis konsekvencan aron de statoj kiuj kontentigas ĉiujn kondiĉojn.
Speco de kvardimensia rolantaro de spactempo.
Ni eltrovu kio okazis.
Ni vidas, ke fine ĉiuj transiris, nur komence nia kamparano decidis ripozi, kaj en la unuaj 2 paŝoj li nenie naĝas.
Human_2 = 0
Human_3 = 0
Ĉi tio sugestas, ke la nombro da ŝtatoj, kiujn ni elektis, estas troa, kaj 8 estos sufiĉe sufiĉa.
En nia kazo, la kamparano faris tion: komenci, ripozi, ripozi, transpasi la kapron, transiri reen, transiri la brasikon, reveni kun la kapro, transiri la lupon, reveni sole, re-liveri la kapron.
Sed finfine la problemo estis solvita.
#Старт.
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
Nun ni provu ŝanĝi la kondiĉojn kaj pruvi, ke ne ekzistas solvoj.
Por fari tion, ni donos al nia lupo herbivoron, kaj li volos manĝi brasikon.
Ĉi tio povas esti komparita kun la kazo en kiu nia celo estas sekurigi la aplikaĵon kaj ni devas certigi, ke ne estas kaŝpasejoj.
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 donis al ni la sekvan respondon:
no solution
Ĝi signifas, ke vere ne ekzistas solvoj.
Tiel, ni programe pruvis la neeblecon kruciĝi kun ĉiomanĝanta lupo sen perdoj por la farmisto.
Se la spektantaro trovas ĉi tiun temon interesa, tiam en estontaj artikoloj mi rakontos al vi kiel transformi ordinaran programon aŭ funkcion en ekvacion kongrua kun formalaj metodoj, kaj solvi ĝin, tiel malkaŝante ambaŭ ĉiujn legitimajn scenarojn kaj vundeblecojn. Unue, pri la sama tasko, sed prezentita en formo de programo, kaj poste iom post iom kompliki ĝin kaj transiri al aktualaj ekzemploj el la mondo de la programaro.
La sekva artikolo jam estas preta:
En ĝi mi transiras de formala konfirmo de problemoj al programoj, kaj priskribas
kiel ili povas esti konvertitaj en formalajn regulsistemojn aŭtomate.
fonto: www.habr.com