我認為，在網路的俄語領域，形式化驗證的主題還沒有得到充分的涵蓋，尤其缺乏簡單明了的例子。
我將舉一個國外的例子，並對著名的將狼、山羊和捲心菜渡到河對岸的問題添加我自己的解決方案。
但首先，我將簡要描述什麼是形式驗證以及為什麼需要它。
形式驗證通常意味著使用一種程式或演算法來檢查另一種程式或演算法。
這對於確保程式按預期運作並確保其安全性是必要的。
形式驗證是尋找和消除漏洞的最強大手段：它允許您找到程式中所有現有的漏洞和錯誤，或證明它們不存在。
值得注意的是，在某些情況下這是不可能的，例如在棋盤寬度為 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。XNUMX 表示它們在左岸，XNUMX 表示它們在右岸。
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 找到了一組滿足所有條件的一致狀態。
一種時空的四維投射。
讓我們弄清楚發生了什麼事。
我們看到最後每個人都過了河，只是一開始我們的農民決定休息，在前兩步中他沒有游到任何地方。
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
這意味著確實沒有解決方案。
因此，我們以程式證明了與雜食性狼雜交而不給農民帶來損失的可能性。
如果觀眾覺得這個主題有趣，那麼在以後的文章中我將告訴你如何將一個普通的程式或函數變成一個與形式方法相容的方程，並求解它，從而揭示所有合法的場景和漏洞。首先，執行相同的任務，但以程式的形式呈現，然後逐漸使其複雜化，並轉向軟體開發領域的當前範例。
下一篇文章已經準備好了：
在其中，我從問題的形式驗證轉向程序，並描述
如何將它們自動轉換為正式的規則系統？
來源： www.habr.com