Формална верификација користејќи го примерот на проблемот со волкот, козата и зелката

Според мое мислење, во секторот на интернет на руски јазик, темата за формална верификација не е доволно покриена, а особено недостасуваат едноставни и јасни примери.

Ќе дадам пример од странски извор, и ќе додадам свое решение за познатиот проблем со преминување на волк, коза и зелка на другата страна на реката.

Но, прво, накратко ќе опишам што е формална верификација и зошто е потребна.

Формалната верификација обично значи проверка на една програма или алгоритам користејќи друга.

Ова е неопходно за да се осигури дека програмата се однесува како што се очекува, а исто така и за да се обезбеди нејзината безбедност.

Формалната верификација е најмоќното средство за пронаоѓање и елиминирање на пропустите: ви овозможува да ги пронајдете сите постоечки дупки и грешки во програмата или да докажете дека тие не постојат.
Вреди да се напомене дека во некои случаи тоа е невозможно, како на пример во проблемот со 8 кралици со ширина на табла од 1000 квадрати: сè се сведува на алгоритамска сложеност или проблем со запирање.

Сепак, во секој случај, ќе се добие еден од трите одговори: програмата е точна, неточна или не беше можно да се пресмета одговорот.

Ако е невозможно да се најде одговор, често е можно да се преработат нејасни делови од програмата, намалувајќи ја нивната алгоритамска сложеност, со цел да се добие конкретен одговор да или не.

И формалната верификација се користи, на пример, во оперативните системи на Windows кернелот и дронови Darpa, за да се обезбеди максимално ниво на заштита.

Ќе користиме Z3Prover, многу моќна алатка за автоматско докажување теорема и решавање равенки.

Покрај тоа, Z3 решава равенки и не ги избира нивните вредности користејќи брутална сила.
Ова значи дека може да го најде одговорот, дури и во случаи кога има 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)

Вклучувајќи го 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

Број е бројот на чекори потребни за решавање. Секој чекор ја претставува состојбата на реката, чамецот и сите ентитети.

Засега, да го избереме по случаен избор и со маржа земеме 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)

И го добиваме одговорот!

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

Тоа значи дека навистина нема решенија.

Така, програмски ја докажавме неможноста за вкрстување со сештојаден волк без загуби за земјоделецот.

Ако публиката ја смета оваа тема интересна, тогаш во идните написи ќе ви кажам како да ја претворите обичната програма или функција во равенка компатибилна со формални методи и да ја решите, со што ќе ги откриете и сите легитимни сценарија и ранливости. Прво, на истата задача, но претставена во форма на програма, а потоа постепено се усложнува и преминува на актуелни примери од светот на развој на софтвер.

Следната статија е веќе подготвена:
Создавање формален систем за верификација од нула: пишување симболична VM во PHP и Python

Во него се префрлам од формална проверка на проблемите на програми и опишувам
како може автоматски да се претворат во системи за формални правила.

Извор: www.habr.com