По мом мишљењу, у сектору интернета на руском језику тема формалне верификације није довољно обрађена, а посебно недостају једноставни и јасни примери.
Навешћу пример из страног извора, а добро познатом проблему преласка вука, козе и купуса на другу страну реке додаћу своје решење.
Али прво ћу укратко описати шта је формална верификација и зашто је потребна.
Формална верификација обично значи проверу једног програма или алгоритма помоћу другог.
Ово је неопходно како би се осигурало да се програм понаша како се очекује и да би се осигурала његова сигурност.
Формална верификација је најмоћније средство за проналажење и елиминисање рањивости: омогућава вам да пронађете све постојеће рупе и грешке у програму или да докажете да не постоје.
Вреди напоменути да је у неким случајевима то немогуће, као на пример у проблему са 8 дама са ширином табле од 1000 поља: све се своди на алгоритамску сложеност или проблем заустављања.
Међутим, у сваком случају, добиће се један од три одговора: програм је тачан, нетачан или није било могуће израчунати одговор.
Ако је немогуће пронаћи одговор, често је могуће прерадити нејасне делове програма, смањујући њихову алгоритамску сложеност, како би се добио конкретан одговор са да или не.
А формална верификација се користи, на пример, у оперативним системима Виндовс кернел и Дарпа дрон, како би се обезбедио максимални ниво заштите.
Користићемо З3Провер, веома моћан алат за аутоматизовано доказивање теорема и решавање једначина.
Штавише, З3 решава једначине, а не бира њихове вредности грубом силом.
То значи да је у стању да пронађе одговор, чак иу случајевима када постоји 10^100 комбинација улазних опција.
Али ово је само десетак улазних аргумената типа Интегер, и то се често сусреће у пракси.
Проблем о 8 краљица (преузето са енглеског ).
# 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)
Покретањем З3 добијамо решење:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Проблем са краљицом је упоредив са програмом који узима као улаз координате 8 дама и даје одговор да ли су даме победиле једна другу.
Ако бисмо решили такав програм користећи формалну верификацију, онда би у поређењу са проблемом једноставно морали да предузмемо још један корак у виду претварања програмског кода у једначину: испоставило се да је суштински идентичан нашем ( наравно, ако је програм правилно написан).
Готово иста ствар ће се десити у случају тражења рањивости: само постављамо излазне услове који су нам потребни, на пример, администраторску лозинку, трансформишемо изворни или декомпајлиран код у једначине компатибилне са верификацијом, а затим добијамо одговор шта податке треба доставити као улаз да би се постигао циљ.
По мом мишљењу, проблем о вуку, кози и купусу је још интересантнији, јер је за његово решавање потребно много (7) корака.
Ако је проблем матице упоредив са случајем када можете продрети на сервер помоћу једног ГЕТ или ПОСТ захтева, онда вук, коза и купус показују пример из много сложеније и распрострањеније категорије, у којој се циљ може постићи само по неколико захтева.
Ово је упоредиво, на пример, са сценаријем где треба да пронађете СКЛ ињекцију, да напишете датотеку кроз њу, затим да подигнете своја права и тек онда добијете лозинку.
Услови проблема и његово решењеСељак треба да превезе вука, козу и купус преко реке. Пољопривредник има чамац који може да прими само један објекат, поред самог фармера. Вук ће појести козу, а коза купус ако их сељак остави без надзора.
Решење је да ће у кораку 4 фармер морати да врати козу.
Сада почнимо да га решавамо програмски.
Означимо фармера, вука, козе и купуса као 4 варијабле које узимају вредност само 0 или 1. Нула значи да се налазе на левој обали, а један значи да су на десној.
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
Број је број корака потребних за решавање. Сваки корак представља стање реке, чамца и свих ентитета.
За сада, хајде да га изаберемо насумично и са маргином, узмимо 10.
Сваки ентитет је представљен у 10 копија - ово је његова вредност у сваком од 10 корака.
Сада да поставимо услове за почетак и крај.
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 ]
Затим постављамо услове у којима вук једе козу, или коза једе купус, као ограничења у једначини.
(У присуству фармера, агресија је немогућа)
# 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) ]
И коначно, дефинисаћемо све могуће радње фармера при преласку тамо или назад.
Може или да поведе са собом вука, козу или купус, или да не води никога, или да уопште не плови нигде.
Наравно, нико не може да пређе без фармера.
То ће бити изражено чињеницом да се свако наредно стање реке, чамца и ентитета може разликовати од претходног само на строго ограничен начин.
Не више од 2 бита, и са многим другим ограничењима, пошто фармер може да транспортује само један ентитет у исто време и не могу се сви оставити заједно.
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) ]
Хајде да покренемо решење.
solve(Side + Start + Finish + Safe + Travel)
И добијамо одговор!
З3 је пронашао конзистентан скуп стања који задовољава све услове.
Нека врста четвородимензионалног одливања простор-времена.
Хајде да схватимо шта се догодило.
Видимо да су на крају сви прешли, само је наш фармер испрва одлучио да се одмори, а у прва 2 корака не плива нигде.
Human_2 = 0
Human_3 = 0
То сугерише да је број држава које смо изабрали превелик, а 8 ће бити сасвим довољно.
У нашем случају, сељак је урадио ово: почни, одмори се, одмори се, пређи козу, пређи назад, укрсти купус, врати се са козом, пређе вука, врати се назад сам, поново испоручи козу.
Али на крају је проблем решен.
#Старт.
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
Покушајмо сада да променимо услове и докажемо да нема решења.
Да бисмо то урадили, даћемо нашем вуку биљоједи, а он ће желети да једе купус.
Ово се може упоредити са случајем у којем је наш циљ да обезбедимо апликацију и морамо да се уверимо да нема рупа.
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) ]
З3 нам је дао следећи одговор:
no solution
То значи да заиста нема решења.
Тако смо програмски доказали немогућност укрштања са вуком свеједом без губитака за фармера.
Ако публика сматра да је ова тема занимљива, онда ћу вам у будућим чланцима рећи како да претворите обичан програм или функцију у једначину компатибилну са формалним методама, и да је решите, откривајући на тај начин све легитимне сценарије и рањивости. Прво на истом задатку, али представљеном у форми програма, а затим га постепено компликовати и прећи на актуелне примере из света развоја софтвера.
Следећи чланак је већ спреман:
У њему прелазим са формалне провере проблема на програме и описујем их
како се могу аутоматски претворити у формалне системе правила.
Извор: ввв.хабр.цом