Ing mratelakake panemume, ing sektor Internet basa Rusia, topik verifikasi formal ora cukup dijamin, lan ana utamané lack saka conto prasaja lan cetha.
Aku bakal menehi conto saka sumber manca, lan nambah solusi dhewe kanggo masalah kondhang nyebrang asu ajag, wedhus lan kubis menyang sisih liyane kali.
Nanging pisanan, aku bakal njlèntrèhaké kanthi ringkes apa verifikasi resmi lan ngapa perlu.
Verifikasi formal biasane tegese mriksa siji program utawa algoritma nggunakake liyane.
Iki perlu kanggo mesthekake yen program kasebut tumindak kaya sing dikarepake lan uga njamin keamanane.
Verifikasi formal minangka cara sing paling kuat kanggo nemokake lan ngilangi kerentanan: ngidini sampeyan nemokake kabeh bolongan lan bug sing ana ing program, utawa mbuktekake manawa ora ana.
Wigati dicathet yen ing sawetara kasus iki ora mungkin, kayata ing masalah 8 ratu kanthi jembar papan 1000 kothak: kabeh iki teka ing kerumitan algoritma utawa masalah sing mandheg.
Nanging, ing kasus apa wae, salah siji saka telung jawaban bakal ditampa: program kasebut bener, salah, utawa ora bisa ngetung jawaban.
Yen ora bisa nemokake jawaban, asring bisa ngolah maneh bagean program sing ora jelas, nyuda kerumitan algoritma, supaya entuk jawaban ya utawa ora.
Lan verifikasi formal digunakake, contone, ing kernel Windows lan sistem operasi mbengung Darpa, kanggo mesthekake tingkat maksimum pangayoman.
Kita bakal nggunakake Z3Prover, alat sing kuat banget kanggo pembuktian téorema otomatis lan pemecahan persamaan.
Kajaba iku, Z3 ngrampungake persamaan, lan ora milih nilai kasebut kanthi nggunakake kekerasan.
Iki tegese bisa nemokake jawaban, sanajan ana 10 ^ 100 kombinasi pilihan input.
Nanging iki mung babagan puluhan argumen input saka jinis Integer, lan iki asring ditemoni ing praktik.
Masalah babagan 8 ratu (Dijupuk saka basa Inggris ).
# 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)
Mlaku Z3, kita entuk solusi:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Masalah ratu iku iso dibandhingke kanggo program sing njupuk minangka input koordinat 8 ratu lan output jawaban apa ratu ngalahake saben liyane.
Yen kita bakal ngrampungake program kasebut kanthi nggunakake verifikasi resmi, banjur dibandhingake karo masalah kasebut, kita mung kudu njupuk langkah liyane ing bentuk ngowahi kode program dadi persamaan: mesthine bakal padha karo kita ( mesthi, yen program iki ditulis bener).
Bab sing meh padha bakal kedadeyan ing kasus nggoleki kerentanan: kita mung nyetel kahanan output sing dibutuhake, contone, sandi admin, ngowahi kode sumber utawa decompiled dadi persamaan sing kompatibel karo verifikasi, banjur entuk jawaban apa data perlu diwenehake minangka input kanggo nggayuh goal.
Miturut kula, masalah bab asu ajag, wedhus lan kubis malah luwih menarik, amarga kanggo ngrampungake iku wis mbutuhake akeh (7) langkah.
Yen masalah ratu bisa dibandhingake karo kasus sing sampeyan bisa nembus server kanthi nggunakake panjaluk GET utawa POST siji, mula serigala, wedhus lan kubis nuduhake conto saka kategori sing luwih rumit lan nyebar, sing tujuane mung bisa digayuh. dening sawetara panjalukan.
Iki iso dibandhingke, contone, kanggo skenario ngendi sampeyan kudu golek injeksi SQL, nulis file liwat, banjur elevate hak lan mung njaluk sandhi.
Kondisi masalah lan solusiPetani kudu ngeterake serigala, wedhus lan kubis nyabrang kali. Petani duwe prau sing mung bisa nampung siji barang, kajaba petani dhewe. Serigala bakal mangan wedhus lan wedhus bakal mangan kubis yen petani ninggalake dheweke tanpa dijaga.
Solusine yaiku ing langkah 4 petani kudu njupuk wedhus maneh.
Saiki ayo miwiti ngrampungake kanthi program.
Ayo dadi ndudohke petani, asu ajag, wedhus lan Gobis minangka 4 variabel sing njupuk Nilai mung 0 utawa 1. Zero tegese padha ing bank kiwa, lan siji tegese padha ing sisih tengen.
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 minangka jumlah langkah sing dibutuhake kanggo ngatasi. Saben langkah nggambarake kahanan kali, prau lan kabeh entitas.
Saiki, ayo milih kanthi acak lan kanthi margin, njupuk 10.
Saben entitas diwakili ing 10 salinan - iki minangka nilai ing saben 10 langkah.
Saiki ayo nyetel kahanan kanggo wiwitan lan rampung.
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 ]
Banjur kita nyetel kahanan ing ngendi asu ajag mangan wedhus, utawa wedhus mangan kubis, minangka kendala ing persamaan.
(Ing ngarsane petani, agresi ora mungkin)
# 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) ]
Lan pungkasane, kita bakal nemtokake kabeh tumindak sing bisa ditindakake petani nalika nyabrang ana utawa bali.
Dheweke bisa njupuk asu ajag, wedhus utawa kubis karo dheweke, utawa ora njupuk sapa-sapa, utawa ora lelayaran ing ngendi wae.
Mesthi, ora ana sing bisa nyabrang tanpa petani.
Iki bakal ditulis dening kasunyatan sing saben negara sakteruse saka kali, prau lan entitas bisa beda-beda saka sadurunge mung ing cara strictly winates.
Ora luwih saka 2 bit, lan akeh watesan liyane, amarga petani mung bisa ngeterake siji entitas sekaligus lan ora kabeh bisa ditinggalake bebarengan.
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) ]
Ayo dadi mbukak solusi.
solve(Side + Start + Finish + Safe + Travel)
Lan kita entuk jawaban!
Z3 nemokake set konsisten negara sing marem kabeh kahanan.
A jinis papat-dimensi cast saka papan-wektu.
Ayo ngerteni apa sing kedadeyan.
Kita weruh yen ing pungkasan kabeh wong nyabrang, mung pisanan petani kita mutusake kanggo ngaso, lan ing 2 langkah pisanan dheweke ora nglangi ing endi wae.
Human_2 = 0
Human_3 = 0
Iki nuduhake yen jumlah negara sing kita pilih akeh banget, lan 8 bakal cukup.
Ing kasus kita, petani nindakake iki: miwiti, ngaso, ngaso, nyabrang wedhus, nyabrang maneh, nyabrang kubis, bali karo wedhus, nyabrang asu ajag, bali dhewe, ngirim wedhus maneh.
Nanging ing pungkasan masalah iki ditanggulangi.
#Старт.
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
Saiki ayo nyoba ngganti kahanan lan mbuktekake manawa ora ana solusi.
Kanggo nindakake iki, kita bakal menehi herbivora serigala, lan dheweke bakal pengin mangan kubis.
Iki bisa dibandhingake karo kasus sing tujuane kanggo ngamanake aplikasi kasebut lan kita kudu nggawe manawa ora ana celah.
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 menehi respon ing ngisor iki:
no solution
Tegese pancen ora ana solusi.
Mangkono, kita kanthi program mbuktekake manawa ora bisa nyebrang karo serigala omnivora tanpa kerugian kanggo petani.
Yen pamirsa nemokake topik iki menarik, banjur ing artikel sabanjure aku bakal pitutur marang kowe carane ngowahi program utawa fungsi biasa dadi persamaan sing cocog karo metode formal, lan ngrampungake, saéngga mbukak kabeh skenario lan kerentanan sing sah. Pisanan, ing tugas sing padha, nanging diwenehi ing wangun program, banjur mboko sithik complicating lan pindhah menyang conto saiki saka donya pangembangan piranti lunak.
Artikel sabanjure wis siyap:
Ing aku pindhah saka verifikasi formal masalah kanggo program, lan njlèntrèhaké
carane bisa diowahi dadi sistem aturan resmi kanthi otomatis.
Source: www.habr.com