ფორმალური გადამოწმება მგლის, თხისა და კომბოსტოს პრობლემის მაგალითის გამოყენებით

ჩემი აზრით, ინტერნეტის რუსულენოვან სექტორში ფორმალური გადამოწმების თემა საკმარისად არ არის დაფარული და განსაკუთრებით მარტივი და ნათელი მაგალითების ნაკლებობაა.

მაგალითს მოვიყვან უცხოური წყაროდან და ჩემს გადაწყვეტას დავამატებ ცნობილ პრობლემას, მგლის, თხისა და კომბოსტოს გაღმა გადაკვეთას.

მაგრამ პირველ რიგში, მოკლედ აღვწერ რა არის ფორმალური გადამოწმება და რატომ არის საჭირო.

ფორმალური გადამოწმება ჩვეულებრივ ნიშნავს ერთი პროგრამის ან ალგორითმის შემოწმებას მეორის გამოყენებით.

ეს აუცილებელია იმის უზრუნველსაყოფად, რომ პროგრამა იქცევა ისე, როგორც მოსალოდნელია და ასევე მისი უსაფრთხოების უზრუნველსაყოფად.

ფორმალური გადამოწმება არის ყველაზე ძლიერი საშუალება მოწყვლადობის პოვნისა და აღმოფხვრის მიზნით: ის საშუალებას გაძლევთ იპოვოთ ყველა არსებული ხვრელი და ხარვეზი პროგრამაში, ან დაამტკიცოთ, რომ ისინი არ არსებობს.
აღსანიშნავია, რომ ზოგიერთ შემთხვევაში ეს შეუძლებელია, მაგალითად, 8 დედოფლის პრობლემაში, რომელთა დაფის სიგანე 1000 კვადრატია: ეს ყველაფერი ალგორითმულ სირთულემდე ან გაჩერების პრობლემასთან არის დაკავშირებული.

თუმცა, ნებისმიერ შემთხვევაში, სამი პასუხიდან ერთ-ერთი მიიღება: პროგრამა სწორია, არასწორია, ან პასუხის დათვლა ვერ მოხერხდა.

თუ პასუხის პოვნა შეუძლებელია, ხშირად შესაძლებელია პროგრამის გაურკვეველი ნაწილების გადამუშავება, მათი ალგორითმული სირთულის შემცირება, კონკრეტული დიახ ან არა პასუხის მისაღებად.

და ფორმალური გადამოწმება გამოიყენება, მაგალითად, Windows kernel და 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

Num არის გადასაჭრელად საჭირო ნაბიჯების რაოდენობა. ყოველი ნაბიჯი წარმოადგენს მდინარის, ნავის და ყველა არსების მდგომარეობას.

ახლა ავირჩიოთ ის შემთხვევით და ზღვრით, ავიღოთ 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