Fl-opinjoni tiegħi, fis-settur tal-Internet bil-lingwa Russa, is-suġġett tal-verifika formali mhuwiex kopert biżżejjed, u hemm speċjalment nuqqas ta 'eżempji sempliċi u ċari.
Se nagħti eżempju minn sors barrani, u nżid is-soluzzjoni tiegħi stess għall-problema magħrufa li naqsam lupu, mogħoż u kaboċċa għan-naħa l-oħra tax-xmara.
Iżda l-ewwel, ser niddeskrivi fil-qosor x'inhi l-verifika formali u għaliex hija meħtieġa.
Verifika formali normalment tfisser verifika ta 'programm jew algoritmu bl-użu ta' ieħor.
Dan huwa meħtieġ biex jiġi żgurat li l-programm iġib ruħu kif mistenni u wkoll biex tiġi żgurata s-sigurtà tiegħu.
Il-verifika formali hija l-aktar mezz b'saħħtu biex issib u telimina l-vulnerabbiltajiet: tippermettilek issib it-toqob u l-bugs eżistenti kollha fi programm, jew tipprova li ma jeżistux.
Ta 'min jinnota li f'xi każijiet dan huwa impossibbli, bħal fil-problema ta' 8 irġejjen b'wisa 'tavla ta' 1000 kwadri: kollox niżel għal kumplessità algoritmika jew il-problema tal-waqfien.
Madankollu, fi kwalunkwe każ, se tiġi riċevuta waħda minn tliet tweġibiet: il-programm huwa korrett, mhux korrett, jew ma kienx possibbli li tiġi kkalkulata t-tweġiba.
Jekk ikun impossibbli li ssib tweġiba, ħafna drabi huwa possibbli li jerġgħu jinħadmu partijiet mhux ċari tal-programm, u titnaqqas il-kumplessità algoritmika tagħhom, sabiex tinkiseb tweġiba speċifika iva jew le.
U l-verifika formali tintuża, pereżempju, fis-sistemi operattivi tal-qalba tal-Windows u d-drone Darpa, biex jiġi żgurat il-livell massimu ta 'protezzjoni.
Se nużaw Z3Prover, għodda b'saħħitha ħafna għall-prova awtomatizzata tat-teoremi u s-soluzzjoni tal-ekwazzjonijiet.
Barra minn hekk, Z3 issolvi l-ekwazzjonijiet, u ma jagħżelx il-valuri tagħhom bl-użu ta 'forza bruta.
Dan ifisser li huwa kapaċi jsib it-tweġiba, anke f'każijiet fejn hemm 10 ^ 100 kombinazzjoni ta 'għażliet ta' input.
Iżda dan huwa biss madwar tużżana argumenti input tat-tip Integer, u dan spiss jiltaqgħu magħhom fil-prattika.
Problema dwar 8 irġejjen (Meħuda mill-Ingliż ).
# 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)
Tmexxi Z3, irridu s-soluzzjoni:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Il-problema tar-reġina hija komparabbli ma 'programm li jieħu bħala input il-koordinati ta' 8 irġejjen u joħroġ ir-risposta jekk ir-irġejjen jegħlbux lil xulxin.
Kieku kellna nsolvu programm bħal dan bl-użu ta' verifika formali, imbagħad meta mqabbel mal-problema, inkunu sempliċiment ikollna bżonn nieħdu pass ieħor fil-forma ta' konverżjoni tal-kodiċi tal-programm f'ekwazzjoni: jirriżulta li jkun essenzjalment identiku għal tagħna ( ovvjament, jekk il-programm inkiteb b'mod korrett).
Kważi l-istess ħaġa se jiġri fil-każ tat-tiftix għal vulnerabbiltajiet: aħna biss nissettjaw il-kundizzjonijiet tal-output li għandna bżonn, pereżempju, il-password tal-amministratur, nittrasformaw is-sors jew il-kodiċi dekompilat f'ekwazzjonijiet kompatibbli mal-verifika, u mbagħad niksbu tweġiba dwar x' id-data jeħtieġ li tiġi fornuta bħala input biex jintlaħaq l-għan.
Fl-opinjoni tiegħi, il-problema dwar il-lupu, il-mogħoż u l-kaboċċi hija saħansitra aktar interessanti, peress li s-soluzzjoni tagħha diġà teħtieġ ħafna (7) passi.
Jekk il-problema tar-reġina hija komparabbli mal-każ fejn tista 'tippenetra server billi tuża talba waħda GET jew POST, allura l-lupu, il-mogħoż u l-kaboċċi juru eżempju minn kategorija ħafna aktar kumplessa u mifruxa, li fiha l-għan jista' jintlaħaq biss minn diversi talbiet.
Dan huwa komparabbli, pereżempju, ma 'xenarju fejn għandek bżonn issib injezzjoni SQL, tikteb fajl minnha, imbagħad tgħolli d-drittijiet tiegħek u mbagħad biss tikseb password.
Kundizzjonijiet tal-problema u s-soluzzjoni tagħhaIl-bidwi jeħtieġ li jittrasporta lupu, mogħoż u kaboċċi tul ix-xmara. Il-bidwi għandu dgħajsa li tista’ takkomoda biss oġġett wieħed, minbarra l-bidwi nnifsu. Il-lupu jiekol il-mogħża u l-mogħoż jiekol il-kaboċċi jekk il-bidwi jħallihom waħedhom.
Is-soluzzjoni hija li fil-pass 4 il-bidwi se jkollu bżonn jieħu l-mogħża lura.
Issa ejja nibdew insolvuha b'mod programmatiku.
Ejja nindikaw il-bidwi, il-lupu, il-mogħoż u l-kaboċċi bħala 4 varjabbli li jieħdu l-valur biss 0 jew 1. Żero ifisser li huma fuq ix-xellug, u wieħed ifisser li huma fuq il-lemin.
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 huwa n-numru ta' passi meħtieġa biex issolvi. Kull pass jirrappreżenta l-istat tax-xmara, id-dgħajsa u l-entitajiet kollha.
Għalissa, ejja nagħżluha bl-addoċċ u b'marġni, ħu 10.
Kull entità hija rappreżentata f'10 kopji - dan huwa l-valur tagħha f'kull wieħed mill-10 passi.
Issa ejja nissettjaw il-kundizzjonijiet għall-bidu u t-tmiem.
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 ]
Imbagħad nistabbilixxu l-kundizzjonijiet fejn il-lupu jiekol il-mogħoż, jew il-mogħoż jiekol il-kaboċċi, bħala restrizzjonijiet fl-ekwazzjoni.
(Fil-preżenza ta 'bidwi, l-aggressjoni hija impossibbli)
# 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) ]
U fl-aħħarnett, aħna se niddefinixxu l-azzjonijiet kollha possibbli tal-bidwi meta jaqsam hemm jew lura.
Jista’ jew jieħu lupu, mogħoż jew kaboċċa miegħu, jew ma jieħu lil ħadd, jew ma jbaħħar imkien.
Ovvjament, ħadd ma jista’ jaqsam mingħajr bidwi.
Dan se jiġi espress mill-fatt li kull stat sussegwenti tax-xmara, dgħajsa u entitajiet jistgħu jvarjaw minn dak preċedenti biss b'mod strettament limitat.
Mhux aktar minn 2 bits, u b'ħafna limiti oħra, peress li l-bidwi jista' jittrasporta biss entità waħda kull darba u mhux kollha jistgħu jitħallew flimkien.
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) ]
Ejja nmexxu s-soluzzjoni.
solve(Side + Start + Finish + Safe + Travel)
U nġibu t-tweġiba!
Z3 sabet sett konsistenti ta 'stati li jissodisfaw il-kundizzjonijiet kollha.
Tip ta 'cast erba' dimensjonali ta 'spazju-ħin.
Ejja naraw x'ġara.
Naraw li fl-aħħar qasmu kulħadd, biss għall-ewwel il-bidwi tagħna ddeċieda li jistrieħ, u fl-ewwel 2 passi ma jgħum imkien.
Human_2 = 0
Human_3 = 0
Dan jissuġġerixxi li n-numru ta 'stati li għażilna huwa eċċessiv, u 8 se jkunu pjuttost biżżejjed.
Fil-każ tagħna, il-bidwi għamel dan: ibda, mistrieħ, mistrieħ, jaqsam il-mogħża, jaqsam lura, jaqsam il-kaboċċa, jirritorna mal-mogħoż, jaqsam il-lupu, lura lura waħdu, jerġa 'jikkonsenja l-mogħża.
Iżda fl-aħħar il-problema ġiet solvuta.
#Старт.
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
Issa ejja nippruvaw nibdlu l-kundizzjonijiet u nipprovaw li m'hemmx soluzzjonijiet.
Biex tagħmel dan, aħna se nagħtu l-erbivorju tal-lupu tagħna, u hu jrid jiekol kaboċċi.
Dan jista' jitqabbel mal-każ li fih l-għan tagħna huwa li niżguraw l-applikazzjoni u rridu niżguraw li ma jkunx hemm lakuni.
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 tana t-tweġiba li ġejja:
no solution
Ifisser li verament m'hemmx soluzzjonijiet.
Għalhekk, aħna ppruvajna b'mod programmatiku l-impossibbiltà li naqsmu ma 'lupu omnivoru mingħajr telf għall-bidwi.
Jekk l-udjenza ssib dan is-suġġett interessanti, allura f'artikoli futuri ngħidlek kif iddawwar programm jew funzjoni ordinarja f'ekwazzjoni kompatibbli ma 'metodi formali, u ssolviha, u b'hekk tiżvela kemm ix-xenarji leġittimi kif ukoll il-vulnerabbiltajiet kollha. L-ewwel, fuq l-istess kompitu, iżda ppreżentat fil-forma ta 'programm, u mbagħad gradwalment tikkomplikaha u timxi fuq eżempji attwali mid-dinja tal-iżvilupp tas-softwer.
L-artiklu li jmiss huwa diġà lest:
Fiha ngħaddi minn verifika formali tal-problemi għal programmi, u niddeskrivi
kif jistgħu jiġu konvertiti f'sistemi ta' regoli formali awtomatikament.
Sors: www.habr.com