オオカミとヤギとキャベツの問題を例にした形式的検証

私の意見では、インターネットのロシア語分野では、形式的検証のテーマが十分にカバーされておらず、特に単純かつ明確な例が不足しています。

外国の情報源からの例を挙げ、オオカミ、ヤギ、キャベツを川の向こう岸に渡るというよく知られた問題に私なりの解決策を加えます。

その前に、正式な検証とは何か、そしてなぜそれが必要なのかについて簡単に説明します。

正式な検証は通常、あるプログラムまたはアルゴリズムを別のプログラムまたはアルゴリズムを使用してチェックすることを意味します。

これは、プログラムが期待どおりに動作することを保証し、またそのセキュリティを確保するために必要です。

正式検証は、脆弱性を発見して排除するための最も強力な手段です。これにより、プログラムに存在するすべてのホールやバグを見つけたり、それらが存在しないことを証明したりすることができます。
ボード幅 8 マスの 1000 クイーンの問題など、場合によってはこれが不可能であることに注意してください。すべてはアルゴリズムの複雑さまたは停止問題に帰着します。

ただし、いずれの場合も、プログラムが正しい、間違っている、または答えを計算できなかったという XNUMX つの答えのうち XNUMX つが返されます。

答えを見つけることができない場合は、多くの場合、特定の「はい」または「いいえ」の答えを得るために、プログラムの不明確な部分を再加工してアルゴリズムの複雑さを軽減することが可能です。

また、最大レベルの保護を確保するために、Windows カーネルや Darpa ドローン オペレーティング システムなどで正式な検証が使用されます。

自動定理証明と方程式解決のための非常に強力なツールである Z3Prover を使用します。

さらに、Z3 は方程式を解き、力ずくで値を選択しません。
これは、入力オプションの組み合わせが 10^100 通りある場合でも、答えを見つけることができることを意味します。

ただし、これは Integer 型の入力引数が約 XNUMX 個だけであり、実際にはよく発生します。

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 つのクイーンの座標を入力として受け取り、クイーンが互いに勝つかどうかの答えを出力するプログラムに相当します。

このようなプログラムを形式的検証を使用して解決する場合、問題と比較すると、プログラム コードを方程式に変換するという形でもう XNUMX つの手順を実行するだけで済みます。つまり、それは本質的に私たちのものと同じであることがわかります (もちろん、プログラムが正しく書かれていればの話ですが)。

脆弱性の検索の場合もほぼ同じことが起こります。必要な出力条件 (管理者パスワードなど) を設定し、ソースまたは逆コンパイルされたコードを検証に適合する式に変換するだけで、結果が何であるかについての答えが得られます。目標を達成するには、データを入力として提供する必要があります。

私の意見では、オオカミ、ヤギ、キャベツの問題はさらに興味深いものです。なぜなら、それを解くにはすでに多くの (7) ステップが必要だからです。

クイーンの問題が、単一の GET または POST リクエストを使用してサーバーに侵入できる場合に匹敵する場合、オオカミ、ヤギ、キャベツは、より複雑で広範なカテゴリの例を示しており、その中でのみ目標を達成できます。いくつかのリクエストにより。

これは、たとえば、SQL インジェクションを見つけて、それを介してファイルを書き込み、権限を昇格してからパスワードを取得する必要があるシナリオに相当します。

問題の状況とその解決策農夫はオオカミ、ヤギ、キャベツを川を渡って運ぶ必要があります。 農場主は、農場主自身の他に、XNUMX つのオブジェクトのみを収容できるボートを持っています。 農夫が放っておくとオオカミがヤギを食べ、ヤギがキャベツを食べてしまいます。

解決策は、ステップ 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 つのエンティティのみを転送でき、すべてを一緒にしておくことはできないため、XNUMX ビット以下であり、その他多くの制限があります。

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

それは本当に解決策がないことを意味します。

このようにして、農夫に損失を与えずに雑食性のオオカミと交配することは不可能であることをプログラム的に証明しました。

読者がこのトピックに興味があると感じたら、今後の記事で、通常のプログラムまたは関数を形式的手法と互換性のある方程式に変換し、それを解く方法を説明します。これにより、すべての正当なシナリオと脆弱性の両方が明らかになります。 最初は同じタスクですが、プログラムの形式で提示され、次にそれを徐々に複雑にして、ソフトウェア開発の世界の最新の例に移ります。

次の記事はすでに準備されています。
正式な検証システムを最初から作成する: PHP と Python でシンボリック VM を作成する

その中で、問題の正式な検証からプログラムに移り、次のように説明します。
それらを正式なルールシステムに自動的に変換するにはどうすればよいでしょうか。

出所： habr.com