На мой погляд, у рускамоўным сектары інтэрнета тэматыка фармальнай верыфікацыі асветлена недастаткова, і асабліва не хапае простых і наглядных прыкладаў.
Я прывяду такі прыклад з замежнай крыніцы, і дапоўню ўласным рашэннем вядомай задачы аб пераправе ваўка, козы і капусты на іншы бок ракі.
Але спачатку сцісла апішу, што з сябе ўяўляе фармальная верыфікацыя і навошта яна патрэбная.
Пад фармальнай верыфікацыяй звычайна разумеюць праверку адной праграмы або алгарытму з дапамогай іншай.
Гэта трэба для таго, каб пераканацца, што паводзіны праграмы адпавядаюць чаканаму, а таксама гарантуюць яе бяспеку.
Фармальная верыфікацыя з'яўляецца самым магутным сродкам пошуку і ўхіленні ўразлівасцяў: яна дазваляе знайсці ўсе існыя дзюры і багі ў праграме, ці ж давесці, што іх няма.
Варта заўважыць, што ў некаторых выпадках гэта бывае немагчыма, як напрыклад, у задачы аб 8 ферзях з шырынёй дошкі 1000 клетак: усё ўпіраецца ў алгарытмічную складанасць або праблему прыпынку.
Аднак у любым выпадку будзе атрыманы адзін з трох адказаў: праграма карэктная, некарэктная, ці ж - вылічыць адказ не ўдалося.
У выпадку немагчымасці знаходжання адказу, часцяком можна перапрацаваць невыразныя месцы праграмы, паменшыўшы іх алгарытмічную складанасць, для таго каб атрымаць пэўны адказ так ці не.
А прымяняецца фармальная верыфікацыя, напрыклад, у ядры Windows і аперацыйных сістэмах беспілотнікаў Darpa, для забеспячэння максімальнага ўзроўню абароны.
Мы будзем выкарыстоўваць Z3Prover, вельмі магутны інструмент для аўтаматызаванага доказу тэарэм і вырашэння ўраўненні.
Прычым Z3 менавіта вырашае ўраўненні, а не падбірае іх значэння грубым брутфорсам.
Гэта азначае, што ён здольны знаходзіць адказ, нават у выпадках калі камбінацый уваходных варыянтаў і 10^100.
А бо гэта ўсяго толькі каля тузіна ўваходных аргументаў тыпу Integer, і падобнае часцяком сустракаецца на практыку.
Задача аб 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)
Запусціўшы Z3, мы атрымліваем рашэнне:
[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) крокаў.
Калі задача аб ферзя параўнальная з варыянтам, калі можна пракрасціся на сервер з дапамогай аднаго GET або POST запыту, то воўк, каза і капуста дэманструе прыклад са значна больш складанай і распаўсюджанай катэгорыі, у якой мэты можна дасягнуць толькі некалькімі запытам.
Гэта параўнальна, напрыклад, са сцэнарам, дзе трэба знайсці SQL ін'екцыю, запісаць праз яе файл, пасля падвысіць свае правы і толькі затым атрымаць пароль.
Умовы задачы і яе разгадкаФермеру трэба перавезці праз раку ваўка, казу і капусту. У фермера ёсць лодка, у якой можа змясціцца, акрамя самога селяніна толькі адзін аб'ект. Воўк з'есць казу, а каза з'есць капусту, калі фермер пакіне іх без нагляду.
Разгадка ў тым, што на 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
Num - гэты лік крокаў неабходных для рашэння. Кожны крок уяўляе сабой стан рэчкі, лодкі і ўсіх сутнасцяў.
Пакуль што выберам яго наўздагад і з запасам, возьмем дзесяць.
Кожная сутнасць прадстаўлена ў 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)
І мы атрымліваем адказ!
Z3 знайшоў несупярэчлівую, і якая задавальняе ўсім умовам сукупнасць станаў.
Гэтакі чатырохмерны злепак прасторы-часу.
Давайце разбяромся, што ж адбылося.
Мы бачым, што ў выніку ўсё пераправіліся, вось толькі спачатку наш фермер вырашыў адпачыць, і нікуды на першых 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) ]
Z3 Выдаў нам наступны адказ:
no solution
Ён азначае, што рашэньняў сапраўды няма.
Такім чынам мы праграмным спосабам даказалі немагчымасць пераправы са ўсяедным ваўком, без страт для фермера.
Калі аўдыторыя палічыць гэтую тэматыку цікавай, то ў далейшых артыкулах я раскажу, як ператварыць звычайную праграму або функцыю ў сумяшчальнае з фармальнымі метадамі раўнанне, і вырашыць яго, выявіўшы тым самым як усе легітымныя сцэнары, так і ўразлівасці. Спачатку на гэтай жа задачы, але прадстаўленай ужо ў выглядзе праграмы, а затым паступова ўскладняючы і пераходзячы да актуальных прыкладаў са свету распрацоўкі ПЗ.
Наступны артыкул ужо гатовы:
У ёй я пераходжу ад фармальнай верыфікацыі задач, да праграм, і апісваю,
якім чынам можна канвертаваць іх у сістэмы фармальных правіл аўтаматычна.
Крыніца: habr.com