Manuprāt, interneta krievvalodīgajā sektorā formālās verifikācijas tēma nav pietiekami aplūkota, un īpaši trūkst vienkāršu un skaidru piemēru.
Es minēšu piemēru no ārzemju avota un pievienošu savu risinājumu labi zināmajai problēmai par vilka, kazas un kāpostu šķērsošanu otrpus upei.
Bet vispirms es īsi aprakstīšu, kas ir formālā pārbaude un kāpēc tā ir nepieciešama.
Formālā pārbaude parasti nozīmē vienas programmas vai algoritma pārbaudi, izmantojot citu.
Tas ir nepieciešams, lai nodrošinātu, ka programma darbojas, kā paredzēts, kā arī lai nodrošinātu tās drošību.
Formālā pārbaude ir visspēcīgākais līdzeklis ievainojamību atrašanai un novēršanai: tā ļauj atrast visas esošās programmas caurumus un kļūdas vai pierādīt, ka tās neeksistē.
Ir vērts atzīmēt, ka dažos gadījumos tas nav iespējams, piemēram, 8 dāmu uzdevumā ar dēļa platumu 1000 kvadrātu: tas viss ir saistīts ar algoritmu sarežģītību vai apstāšanās problēmu.
Tomēr jebkurā gadījumā tiks saņemta viena no trim atbildēm: programma ir pareiza, nepareiza, vai arī nebija iespējams aprēķināt atbildi.
Ja atbildi nav iespējams atrast, bieži vien ir iespējams pārstrādāt neskaidras programmas daļas, samazinot to algoritmisko sarežģītību, lai iegūtu konkrētu jā vai nē atbildi.
Un formāla pārbaude tiek izmantota, piemēram, Windows kodola un Darpa drone operētājsistēmās, lai nodrošinātu maksimālu aizsardzības līmeni.
Mēs izmantosim Z3Prover, ļoti jaudīgu rīku automatizētai teorēmu pierādīšanai un vienādojumu risināšanai.
Turklāt Z3 atrisina vienādojumus un neizvēlas to vērtības, izmantojot brutālu spēku.
Tas nozīmē, ka tas spēj atrast atbildi pat gadījumos, kad ir 10^100 ievades opciju kombinācijas.
Bet tas ir tikai aptuveni ducis vesela skaitļa ievades argumentu, un praksē ar to bieži saskaras.
Problēma par 8 dāmām (Ņemts no angļu valodas ).
# 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)
Palaižot Z3, mēs iegūstam risinājumu:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Karalienes problēma ir salīdzināma ar programmu, kas kā ievadi izmanto 8 dāmu koordinātas un izvada atbildi, vai dāmas pārspēj viena otru.
Ja mēs šādu programmu atrisinātu, izmantojot formālu verifikāciju, tad, salīdzinot ar problēmu, mums vienkārši būtu jāveic vēl viens solis, pārvēršot programmas kodu vienādojumā: tas izrādītos būtībā identisks mūsu ( protams, ja programma ir uzrakstīta pareizi).
Gandrīz tas pats notiks ievainojamību meklēšanas gadījumā: mēs vienkārši iestatām nepieciešamos izvades nosacījumus, piemēram, administratora paroli, pārveidojam avota vai dekompilēto kodu vienādojumos, kas ir saderīgi ar verifikāciju, un pēc tam saņemam atbildi, kas dati ir jāiesniedz kā ievade, lai sasniegtu mērķi.
Manuprāt, problēma par vilku, kazu un kāpostiem ir vēl interesantāka, jo tās risināšana jau prasa daudzus (7) soļus.
Ja karalienes problēma ir salīdzināma ar gadījumu, kad var iekļūt serverī, izmantojot vienu GET vai POST pieprasījumu, tad vilks, kaza un kāposti parāda piemēru no daudz sarežģītākas un plašāk izplatītas kategorijas, kurā mērķi var sasniegt tikai pēc vairākiem lūgumiem.
Tas ir salīdzināms, piemēram, ar scenāriju, kad jāatrod SQL injekcija, jāraksta caur to fails, pēc tam jāpaaugstina tiesības un tikai tad jāsaņem parole.
Problēmas nosacījumi un tās risinājumsZemniekam pāri upei jāpārved vilks, kaza un kāposti. Zemniekam ir laiva, kurā var novietot tikai vienu objektu, izņemot pašu zemnieku. Vilks apēdīs kazu un kaza ēdīs kāpostus, ja zemnieks tos atstās bez uzraudzības.
Risinājums ir tāds, ka 4. darbībā lauksaimniekam kaza būs jāpaņem atpakaļ.
Tagad sāksim to risināt programmatiski.
Apzīmēsim zemnieku, vilku, kazu un kāpostu kā 4 mainīgos lielumus, kuru vērtība ir tikai 0 vai 1. Nulle nozīmē, ka tie atrodas kreisajā krastā, un viens nozīmē, ka tie atrodas labajā krastā.
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
Skaitlis ir risināšanai nepieciešamo darbību skaits. Katrs solis atspoguļo upes stāvokli, laivu un visas vienības.
Pagaidām izvēlēsimies nejauši un ar rezervi, ņemsim 10.
Katra entītija ir attēlota 10 eksemplāros – tā ir tās vērtība katrā no 10 soļiem.
Tagad uzstādīsim nosacījumus startam un finišam.
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 ]
Tad mēs uzstādām nosacījumus, kad vilks ēd kazu vai kaza ēd kāpostus, kā ierobežojumus vienādojumā.
(Zemnieka klātbūtnē agresija nav iespējama)
# 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) ]
Un visbeidzot, mēs definēsim visas iespējamās lauksaimnieka darbības, šķērsojot tur vai atpakaļ.
Var vai nu vilku, kazu vai kāpostu paņemt līdzi, vai arī nevienu neņemt, vai vispār nekur nebraukt.
Protams, neviens nevar tikt pāri bez zemnieka.
Tas izpaudīsies ar to, ka katrs nākamais upes, laivas un entītiju stāvoklis var atšķirties no iepriekšējā tikai stingri ierobežotā veidā.
Ne vairāk kā 2 biti un ar daudziem citiem ierobežojumiem, jo lauksaimnieks vienlaikus var pārvadāt tikai vienu vienību, un visus nevar atstāt kopā.
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) ]
Palaidīsim risinājumu.
solve(Side + Start + Finish + Safe + Travel)
Un mēs saņemam atbildi!
Z3 atrada konsekventu stāvokļu kopu, kas atbilst visiem nosacījumiem.
Sava veida četrdimensiju laika telpa.
Noskaidrosim, kas noticis.
Redzam, ka beigās visi šķērsoja, tikai sākumā mūsu zemnieks nolēma atpūsties, un pirmajos 2 soļos viņš nekur nepeld.
Human_2 = 0
Human_3 = 0
Tas liecina, ka izvēlēto štatu skaits ir pārmērīgs, un ar 8 būs pilnīgi pietiekami.
Mūsu gadījumā zemnieks darīja tā: sāc, atpūšas, atpūties, šķērso kazu, šķērso atpakaļ, šķērso kāpostu, atgriezies ar kazu, pārbrauca pāri vilkam, atgriezies viens, nogādā kazu vēlreiz.
Bet galu galā problēma tika atrisināta.
#Старт.
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
Tagad mēģināsim mainīt nosacījumus un pierādīt, ka risinājumu nav.
Lai to izdarītu, mēs iedosim savam vilkam zālēdāju, un viņš gribēs ēst kāpostus.
To var salīdzināt ar gadījumu, kad mūsu mērķis ir nodrošināt lietojumprogrammas drošību, un mums ir jāpārliecinās, ka nav nekādu nepilnību.
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 mums sniedza šādu atbildi:
no solution
Tas nozīmē, ka risinājumu tiešām nav.
Tā mēs programmatiski pierādījām, ka ar visēdāju vilku nav iespējams bez zaudējumiem zemniekam.
Ja auditorijai šī tēma šķitīs interesanta, tad nākamajos rakstos pastāstīšu, kā parastu programmu vai funkciju pārvērst par vienādojumu, kas ir savietojams ar formālām metodēm, un atrisināt to, tādējādi atklājot gan visus likumīgos scenārijus, gan ievainojamības. Pirmkārt, par to pašu uzdevumu, bet parādīts programmas veidā, un pēc tam pakāpeniski to sarežģījot un pārejot uz pašreizējiem piemēriem no programmatūras izstrādes pasaules.
Nākamais raksts jau ir gatavs:
Tajā es pāreju no formālas problēmu pārbaudes uz programmām un aprakstu
kā tos var automātiski pārvērst formālās noteikumu sistēmās.
Avots: www.habr.com