Sa palagay ko, sa sektor ng Internet sa wikang Ruso, ang paksa ng pormal na pag-verify ay hindi sapat na sakop, at lalo na ang kakulangan ng simple at malinaw na mga halimbawa.
Magbibigay ako ng isang halimbawa mula sa isang dayuhang mapagkukunan, at magdagdag ng aking sariling solusyon sa kilalang problema ng pagtawid ng isang lobo, isang kambing at isang repolyo sa kabilang panig ng ilog.
Ngunit una, maikling ilalarawan ko kung ano ang pormal na pagpapatunay at kung bakit ito kinakailangan.
Ang pormal na pag-verify ay karaniwang nangangahulugan ng pagsuri sa isang programa o algorithm gamit ang isa pa.
Ito ay kinakailangan upang matiyak na ang programa ay kumikilos tulad ng inaasahan at upang matiyak din ang seguridad nito.
Ang pormal na pag-verify ay ang pinakamabisang paraan ng paghahanap at pag-aalis ng mga kahinaan: pinapayagan ka nitong mahanap ang lahat ng umiiral na butas at bug sa isang programa, o patunayan na wala ang mga ito.
Ito ay nagkakahalaga ng noting na sa ilang mga kaso na ito ay imposible, tulad ng sa problema ng 8 queens na may isang board lapad ng 1000 mga parisukat: ang lahat ng ito ay bumaba sa algorithmic kumplikado o ang paghinto ng problema.
Gayunpaman, sa anumang kaso, isa sa tatlong sagot ang matatanggap: tama ang programa, mali, o hindi posibleng kalkulahin ang sagot.
Kung imposibleng makahanap ng sagot, madalas na posible na muling isagawa ang hindi malinaw na mga bahagi ng programa, na binabawasan ang kanilang pagiging kumplikado ng algorithm, upang makakuha ng tiyak na sagot na oo o hindi.
At ang pormal na pag-verify ay ginagamit, halimbawa, sa Windows kernel at Darpa drone operating system, upang matiyak ang pinakamataas na antas ng proteksyon.
Gagamitin namin ang Z3Prover, isang napakalakas na tool para sa automated theorem proving at equation solving.
Bukod dito, nilulutas ng Z3 ang mga equation, at hindi pinipili ang kanilang mga halaga gamit ang malupit na puwersa.
Nangangahulugan ito na nagagawa nitong mahanap ang sagot, kahit na sa mga kaso kung saan mayroong 10^100 na kumbinasyon ng mga opsyon sa pag-input.
Ngunit ito ay halos isang dosenang input na argumento ng uri ng Integer, at ito ay madalas na nakatagpo sa pagsasanay.
Problema tungkol sa 8 reyna (Kinuha mula sa English ).
# 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)
Pagpapatakbo ng Z3, nakuha namin ang solusyon:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Ang problema ng reyna ay maihahambing sa isang programa na kumukuha bilang input ng mga coordinate ng 8 queens at naglalabas ng sagot kung ang mga reyna ay matalo sa isa't isa.
Kung lutasin natin ang naturang programa gamit ang pormal na pag-verify, kung ihahambing sa problema, kailangan lang nating gumawa ng isa pang hakbang sa anyo ng pag-convert ng program code sa isang equation: ito ay magiging mahalagang magkapareho sa atin ( siyempre, kung ang programa ay isinulat nang tama).
Halos pareho ang mangyayari sa kaso ng paghahanap ng mga kahinaan: itinakda lang namin ang mga kundisyon ng output na kailangan namin, halimbawa, ang password ng admin, i-transform ang source o decompiled code sa mga equation na tugma sa pag-verify, at pagkatapos ay makakuha ng sagot kung ano kailangang maibigay ang data bilang input upang makamit ang layunin.
Sa aking palagay, ang problema tungkol sa lobo, kambing at repolyo ay mas kawili-wili, dahil ang paglutas nito ay nangangailangan na ng maraming (7) hakbang.
Kung ang problema ng reyna ay maihahambing sa kaso kung saan maaari kang tumagos sa isang server gamit ang isang kahilingan sa GET o POST, kung gayon ang lobo, kambing at repolyo ay nagpapakita ng isang halimbawa mula sa isang mas kumplikado at malawak na kategorya, kung saan ang layunin ay makakamit lamang sa pamamagitan ng ilang mga kahilingan.
Ito ay maihahambing, halimbawa, sa isang senaryo kung saan kailangan mong maghanap ng SQL injection, magsulat ng isang file sa pamamagitan nito, pagkatapos ay itaas ang iyong mga karapatan at pagkatapos ay kumuha ng password.
Mga kondisyon ng problema at solusyon nitoAng magsasaka ay kailangang maghatid ng lobo, kambing at repolyo sa kabila ng ilog. Ang magsasaka ay may bangka na maaari lamang tumanggap ng isang bagay, bukod sa magsasaka mismo. Kakainin ng lobo ang kambing at kakainin ng kambing ang repolyo kung iiwan sila ng magsasaka nang walang pag-aalaga.
Ang solusyon ay na sa hakbang 4 ang magsasaka ay kailangang ibalik ang kambing.
Ngayon simulan natin ang paglutas nito sa programmatically.
Tukuyin natin ang magsasaka, lobo, kambing at repolyo bilang 4 na variable na kumukuha ng halaga lamang 0 o 1. Ang ibig sabihin ng zero ay nasa kaliwang bangko sila, at ang isa ay nangangahulugang nasa kanan sila.
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
Ang Num ay ang bilang ng mga hakbang na kinakailangan upang malutas. Ang bawat hakbang ay kumakatawan sa estado ng ilog, ang bangka at lahat ng entidad.
Sa ngayon, piliin natin ito nang random at may margin, kumuha ng 10.
Ang bawat entity ay kinakatawan sa 10 kopya - ito ang halaga nito sa bawat isa sa 10 hakbang.
Ngayon, itakda natin ang mga kondisyon para sa simula at pagtatapos.
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 ]
Pagkatapos ay itinakda namin ang mga kondisyon kung saan kinakain ng lobo ang kambing, o ang kambing ay kumakain ng repolyo, bilang mga hadlang sa equation.
(Sa presensya ng isang magsasaka, imposible ang pagsalakay)
# 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) ]
At sa wakas, tutukuyin natin ang lahat ng posibleng aksyon ng magsasaka kapag tumatawid doon o pabalik.
Maaari siyang kumuha ng isang lobo, isang kambing o isang repolyo sa kanya, o hindi kumuha ng sinuman, o hindi maglayag kahit saan.
Syempre, walang makatawid kung walang magsasaka.
Ito ay ipahahayag ng katotohanan na ang bawat kasunod na estado ng ilog, bangka at mga nilalang ay maaaring mag-iba mula sa nauna lamang sa isang mahigpit na limitadong paraan.
Hindi hihigit sa 2 bits, at may maraming iba pang mga limitasyon, dahil ang magsasaka ay maaari lamang maghatid ng isang entity sa isang pagkakataon at hindi lahat ay maaaring iwanang magkasama.
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) ]
Patakbuhin natin ang solusyon.
solve(Side + Start + Finish + Safe + Travel)
At nakuha namin ang sagot!
Nakakita ang Z3 ng pare-parehong hanay ng mga estado na nakakatugon sa lahat ng kundisyon.
Isang uri ng four-dimensional na cast ng space-time.
Alamin natin kung ano ang nangyari.
Nakikita namin na sa huli ay tumawid ang lahat, noong una ay nagpasya ang aming magsasaka na magpahinga, at sa unang 2 hakbang ay hindi siya lumangoy kahit saan.
Human_2 = 0
Human_3 = 0
Iminumungkahi nito na ang bilang ng mga estado na pinili namin ay sobra-sobra, at 8 ay magiging sapat na.
Sa aming kaso, ginawa ito ng magsasaka: magsimula, magpahinga, magpahinga, tumawid sa kambing, tumawid pabalik, tumawid sa repolyo, bumalik kasama ang kambing, tumawid sa lobo, bumalik nang mag-isa, muling ihatid ang kambing.
Ngunit sa huli ay nalutas ang problema.
#Π‘ΡΠ°ΡΡ.
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
Ngayon subukan nating baguhin ang mga kondisyon at patunayan na walang mga solusyon.
Upang gawin ito, bibigyan namin ang aming lobo ng herbivory, at gusto niyang kumain ng repolyo.
Ito ay maihahambing sa kaso kung saan ang layunin namin ay i-secure ang aplikasyon at kailangan naming tiyakin na walang mga butas.
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) ]
Ibinigay sa amin ni Z3 ang sumusunod na tugon:
no solution
Ibig sabihin wala talagang solusyon.
Kaya, pinatunayan namin sa programmatically ang imposibilidad ng pagtawid sa isang omnivorous na lobo nang walang pagkalugi para sa magsasaka.
Kung natutuklasan ng madla ang paksang ito na kawili-wili, pagkatapos ay sa mga artikulo sa hinaharap sasabihin ko sa iyo kung paano gawing isang equation na katugma ang isang ordinaryong programa o function sa mga pormal na pamamaraan, at lutasin ito, at sa gayon ay ibinubunyag ang parehong mga lehitimong sitwasyon at kahinaan. Una, sa parehong gawain, ngunit ipinakita sa anyo ng isang programa, at pagkatapos ay unti-unting kumplikado ito at lumipat sa kasalukuyang mga halimbawa mula sa mundo ng pagbuo ng software.
Ang susunod na artikulo ay handa na:
Dito ako lumipat mula sa pormal na pag-verify ng mga problema patungo sa mga programa, at naglalarawan
paano sila awtomatikong mako-convert sa mga pormal na sistema ng panuntunan.
Pinagmulan: www.habr.com