Dina pamanggih kuring, dina sektor Rusia-basa Internet, topik verifikasi formal teu cukup katutupan, sarta aya utamana kurangna conto basajan tur jelas.
Kuring bakal masihan conto tina sumber asing, sareng nambihan solusi kuring sorangan pikeun masalah anu dipikanyaho nyebrang ajag, embe sareng kol ka sisi séjén walungan.
Tapi ke heula, kuring bakal ngajelaskeun sakeudeung naon verifikasi formal sareng naha éta diperyogikeun.
Verifikasi formal biasana hartosna mariksa hiji program atanapi algoritma nganggo anu sanés.
Ieu diperlukeun pikeun mastikeun yén program behaves sakumaha ekspektasi sarta ogé pikeun mastikeun kaamanan na.
Verifikasi formal mangrupa sarana pangkuatna pikeun manggihan tur ngaleungitkeun vulnerabilities: eta ngidinan Anjeun pikeun manggihan sagala liang aya na bug dina program, atawa ngabuktikeun yén maranéhna teu aya.
Eta sia noting yén dina sababaraha kasus ieu teu mungkin, kayaning dina masalah 8 Queens kalayan rubak dewan 1000 kuadrat: eta sadayana turun ka pajeulitna algorithmic atawa masalah stopping.
Nanging, dina hal naon waé, salah sahiji tina tilu jawaban bakal ditampi: programna leres, salah, atanapi henteu tiasa ngitung jawaban.
Lamun teu mungkin pikeun manggihan jawaban, éta mindeng mungkin mun rework bagian jelas tina program, ngurangan pajeulitna algorithmic maranéhna, dina urutan pikeun ménta hiji enya atawa henteu jawaban husus.
Jeung verifikasi formal dipaké, contona, dina kernel Windows jeung sistem operasi drone Darpa, pikeun mastikeun tingkat maksimum panyalindungan.
Urang bakal ngagunakeun Z3Prover, alat anu pohara kuat pikeun téoréma otomatis ngabuktikeun jeung ngarengsekeun persamaan.
Sumawona, Z3 ngarengsekeun persamaan, sareng henteu milih nilaina nganggo gaya kasar.
Ieu ngandung harti yén éta téh bisa manggihan jawaban, sanajan dina kasus dimana aya 10 ^ 100 kombinasi pilihan input.
Tapi ieu ngan ngeunaan belasan argumen input tipe Integer, sarta ieu mindeng encountered dina prakna.
Masalah ngeunaan 8 ratu (dicokot tina 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)
Ngajalankeun Z3, urang meunang 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 téh comparable kana program nu nyokot salaku input koordinat 8 Queens sarta outputs jawaban naha ratu ngéléhkeun silih.
Upami urang ngabéréskeun program sapertos kitu nganggo verifikasi formal, teras dibandingkeun sareng masalahna, urang ngan saukur kedah nyandak hiji léngkah deui dina bentuk ngarobih kode program kana persamaan: éta bakal janten dasarna sami sareng milik urang ( tangtu, lamun program ieu ditulis leres).
Ampir hal anu sami bakal kajantenan dina kasus milarian kerentanan: urang ngan ukur nyetél kaayaan kaluaran anu urang peryogikeun, contona, sandi admin, ngarobih sumber atanapi kode decompiled kana persamaan anu cocog sareng verifikasi, teras kéngingkeun jawaban naon. data perlu disadiakeun salaku input pikeun ngahontal tujuan.
Dina pamanggih kuring, masalah ngeunaan ajag, embe jeung kol malah leuwih metot, sabab ngarengsekeun eta geus merlukeun loba (7) léngkah.
Upami masalah ratu tiasa dibandingkeun sareng kasus dimana anjeun tiasa nembus server nganggo pamundut GET atanapi POST tunggal, maka ajag, embe sareng kol nunjukkeun conto tina kategori anu langkung rumit sareng nyebar, dimana tujuanna ngan ukur tiasa dihontal. ku sababaraha pamundut.
Ieu tiasa dibandingkeun, contona, kana skenario dimana anjeun kedah milarian suntikan SQL, nyerat file ngalangkunganana, teras angkat hak anjeun sareng ngan ukur kéngingkeun kecap konci.
Kaayaan masalah sareng solusinaPatani kedah ngangkut ajag, embe sareng kol meuntas walungan. Patani boga parahu anu ngan bisa nampung hiji barang, salian ti patani sorangan. Ajag bakal ngahakan embe jeung embe bakal ngahakan kol lamun patani ninggalkeun eta tanpa dijaga.
Solusina nyaéta dina léngkah 4 patani kedah nyandak embe deui.
Ayeuna hayu urang mimitian ngarengsekeun éta programmatically.
Hayu urang denote nu tani, ajag, embe jeung kol salaku 4 variabel nu nyokot nilai ngan 0 atawa 1. Nol hartina aranjeunna dina bank kénca, sarta hiji hartina aranjeunna dina katuhu.
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 nyaéta jumlah léngkah anu diperlukeun pikeun ngajawab. Unggal hambalan ngagambarkeun kaayaan walungan, parahu jeung sakabéh éntitas.
Pikeun ayeuna, hayu urang milih sacara acak sareng nganggo margin, cokot 10.
Unggal éntitas diwakilan dina 10 salinan - ieu mangrupikeun nilaina dina unggal 10 léngkah.
Ayeuna hayu urang nyetel kaayaan pikeun ngamimitian jeung rengse.
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 ]
Teras we netepkeun kaayaan dimana ajag tuang embe, atanapi embe tuang kol, salaku konstrain dina persamaan.
(Dina ayana patani, agresi mustahil)
# 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) ]
Sarta pamustunganana, urang bakal nangtukeun sagala lampah mungkin tina patani nalika nyebrang dinya atawa balik.
Anjeunna tiasa nyandak ajag, embe atanapi kol sareng anjeunna, atanapi henteu nyandak saha waé, atanapi henteu balayar dimana waé.
Tangtu, teu saurang ogé bisa meuntas tanpa patani.
Ieu bakal dinyatakeun ku kanyataan yén unggal kaayaan saterusna walungan, kapal jeung éntitas bisa béda ti saméméhna ngan dina cara mastikeun kawates.
Henteu langkung ti 2 bit, sareng seueur wates anu sanés, sabab patani ngan ukur tiasa ngangkut hiji éntitas dina hiji waktos sareng henteu sadayana tiasa ditinggalkeun babarengan.
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) ]
Hayu urang ngajalankeun solusi.
solve(Side + Start + Finish + Safe + Travel)
Sarta kami meunang jawaban!
Z3 mendakan set konsistén nagara anu nyugemakeun sadaya kaayaan.
A jenis tuang opat diménsi spasi-waktu.
Hayu urang terang naon anu lumangsung.
Kami ningali yén tungtungna sadayana nyebrang, ngan mimitina patani urang mutuskeun istirahat, sareng dina 2 léngkah anu munggaran anjeunna henteu ngojay di mana waé.
Human_2 = 0
Human_3 = 0
Ieu nunjukkeun yén jumlah nagara bagian anu urang pilih kaleuleuwihan, sareng 8 bakal cekap.
Dina hal urang, patani ngalakukeun ieu: ngamimitian, istirahat, istirahat, meuntas embe, meuntas deui, meuntas kol, balik jeung embe, meuntas ajag, balik deui nyalira, ulang pangiriman embe.
Tapi dina tungtungna masalah ieu direngsekeun.
#Старт.
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
Ayeuna hayu urang cobian ngarobih kaayaan sareng ngabuktikeun yén teu aya solusi.
Jang ngalampahkeun ieu, urang bakal masihan herbivora ajag urang, sarta anjeunna bakal hoyong tuang kol.
Ieu tiasa dibandingkeun sareng kasus dimana tujuan urang nyaéta pikeun ngamankeun aplikasi sareng urang kedah mastikeun yén teu aya 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 masihan kami réspon ieu:
no solution
Éta hartosna leres-leres henteu aya solusi.
Ku kituna, urang programmatically ngabuktikeun impossibility nyebrang jeung ajag omnivora tanpa karugian pikeun patani.
Upami pamiarsa mendakan topik ieu pikaresepeun, maka dina tulisan anu bakal datang kuring bakal nyarioskeun ka anjeun kumaha cara ngarobah program biasa atanapi fungsina janten persamaan anu cocog sareng metode formal, sareng ngabéréskeunana, ku kituna ngungkabkeun sadayana skenario anu sah sareng kerentanan. Kahiji, dina tugas anu sarua, tapi dibere dina bentuk program, lajeng laun complicating eta sarta pindah ka conto ayeuna ti dunya ngembangkeun software.
Artikel salajengna parantos siap:
Di jerona kuring mindahkeun tina verifikasi formal masalah pikeun program, sareng ngajelaskeun
kumaha aranjeunna bisa dirobah jadi sistem aturan formal otomatis.
sumber: www.habr.com