外国のソースからこのような例を挙げ、オオカミ、ヤギ、キャベツを川の反対側に運ぶというよく知られている問題に対する私自身の解決策を補足します。
しかし、最初に、正式な検証とは何か、なぜ検証が必要なのかを簡単に説明します。
正式な検証とは、通常、あるプログラムまたはアルゴリズムを別のプログラムまたはアルゴリズムを使用してチェックすることを意味します。
これは、プログラムの動作が期待どおりであることを確認し、その安全性を確保するために必要です。
フォーマル検証は、脆弱性を見つけて排除するための最も強力なツールです。プログラム内の既存のすべての穴やバグを見つけたり、それらが存在しないことを証明したりできます。
たとえば、1000セルのボード幅を持つ8つのクイーンの問題では、これが不可能な場合があることに注意してください。すべてはアルゴリズムの複雑さまたは停止の問題に依存します。
ただし、いずれの場合でも、プログラムが正しいか、間違っているか、答えを計算できなかったという3つの答えのいずれかを受け取ります。
答えが見つからない場合は、プログラムのあいまいな場所を処理し、アルゴリズムの複雑さを軽減して特定の答え（yesまたはno）を取得することが可能です。
また、WindowsカーネルやDarpaドローンオペレーティングシステムなどでは、最大限の保護を提供するために、正式な検証が使用されます。
Z3Proverを使用します。これは、定理の自動証明と方程式の解法のための非常に強力なツールです。
さらに、Z3は方程式を正確に解き、ブルートフォースで値を選択しません。
これは、入力オプションと10 ^ 100の組み合わせがある場合でも、彼が答えを見つけることができることを意味します。
しかし、これはInteger型の約12個の入力引数にすぎず、実際によく見られます。
クイーン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人の女王の座標を取り込んで、女王がお互いに勝った場合に答えを表示するプログラムに匹敵します。
正式な検証を使用してこのようなプログラムを解決する場合、タスクと比較して、プログラムコードを方程式に変換するという形でもう1つの手順を実行するだけで済みます（プログラムが正しく記述されていれば）
脆弱性を検索する場合もほぼ同じことが起こります。たとえば、管理者パスワードなどの必要な出力条件を設定し、ソースまたは逆コンパイルされたコードを検証と互換性のある方程式に変換してから、目標を達成するために入力するデータの答えを取得します
私の意見では、オオカミ、ヤギ、キャベツの問題は、それを解決するために多くの（7）ステップがすでに必要であるため、さらに興味深いものです。
1つのGETまたはPOSTリクエストを使用してサーバーに侵入できる場合、クイーンのタスクがオプションに匹敵する場合、オオカミ、ヤギ、キャベツは、はるかに複雑で広範にわたるカテゴリからの例を示しており、わずかなリクエストにしか到達できません。
これは、たとえば、SQLインジェクションを見つけ、それを介してファイルを書き込み、次に権限を増やしてからパスワードを取得する必要があるシナリオに匹敵します。
問題条件とその解決策
農夫は川を渡ってオオカミ、ヤギおよびキャベツを運ぶ必要があります。 農夫は、農民自身を除いて、1つのオブジェクトのみが収まるボートを持っています。 オオカミはヤギを食べ、農家がキャベツを放置するとヤギがキャベツを食べます。
解決策は、ステップ4で、農家がヤギを取り戻す必要があることです。
解決策は、ステップ4で、農家がヤギを取り戻す必要があることです。
次に、プログラムでソリューションを開始しましょう。
農家、オオカミ、ヤギ、キャベツを4つの変数として指定します。値は0または1のみです。ゼロは左岸にあり、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) ]
そして最後に、私たちはそこに移動したり戻ったりするとき、農家の可能な行動をすべて尋ねます。
彼は、オオカミ、ヤギ、またはキャベツを連れて行くか、誰も連れて行かないか、どこにも行かないことさえできます。
もちろん、農民なしでは誰も渡れません。
これは、川、ボート、およびエンティティの各後続の状態が厳密に限定された方法でのみ以前の状態と異なる可能性があるという事実によって表されます。
農家は一度に1つのエンティティのみを転送でき、すべてを一緒に残せるわけではないため、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は、一貫した満足のいく一連の条件を見つけました。
一種の時空の4次元キャスト。
何が起こったのか見てみましょう。
結局、全員が交差したことがわかります。最初に農家がリラックスすることを決め、最初の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を作成します
その中で、タスクの正式な検証からプログラムに移行し、説明します
それらを自動的に正式なルールシステムに変換する方法。