形式的検証は、あるプログラムまたはアルゴリズムを別のプログラムまたはアルゴリズムを使用して検証することです。
これは、プログラム内のすべての脆弱性を見つけたり、脆弱性が存在しないことを証明したりできる最も強力な方法の XNUMX つです。
形式的検証のより詳細な説明は、次の問題を解決する例で見ることができます。 前回の記事で。
この記事では、問題の正式な検証からプログラムに移り、その方法について説明します。
それらを正式なルールシステムに自動的に変換するにはどうすればよいでしょうか。
これを行うために、私はシンボリックな原則を使用して、仮想マシンの類似物を独自に作成しました。
プログラム コードを解析して方程式系 (SMT) に変換します。これはすでにプログラムで解くことができます。
記号計算に関する情報はインターネット上でかなり断片的に提供されているため、
それが何なのかを簡単に説明します。
シンボリック計算は、広範囲のデータに対してプログラムを同時に実行する方法であり、正式なプログラム検証の主要なツールです。
たとえば、最初の引数が任意の正の値、42 番目の引数が負の値、XNUMX 番目の引数が XNUMX、出力引数が XNUMX などの値をとる入力条件を設定できます。
XNUMX 回の実行でシンボリック計算を行うと、望ましい結果が得られるかどうかの答えと、そのような入力パラメーターのセットの例が得られます。 または、そのようなパラメーターが存在しないことを証明します。
さらに、入力引数をすべての可能な引数に設定し、出力引数 (管理者パスワードなど) のみを選択することができます。
この場合、プログラムのすべての脆弱性を見つけるか、管理者のパスワードが安全であるという証拠を入手します。
特定の入力データを使用したプログラムの古典的な実行は、シンボリック実行の特殊なケースであることに注意してください。
したがって、私のキャラクター VM は、標準の仮想マシンのエミュレーション モードでも動作できます。
前の記事へのコメントでは、形式的検証の弱点についての議論を伴う、形式的検証に対する公正な批判を見つけることができます。
主な問題は次のとおりです。
- 正式な検証は最終的に P=NP になるため、組み合わせ爆発
- ファイル システム、ネットワーク、その他の外部ストレージへの呼び出しの処理は検証がより困難です
- 仕様のバグ。顧客またはプログラマが XNUMX つのことを意図していたが、それを技術仕様に十分正確に記述しなかった場合。
その結果、プログラムは検証されて仕様に準拠していますが、作成者が期待したものとはまったく異なる動作をすることになります。
この記事では形式的検証を実際に使用することを主に検討しているため、今のところは壁に頭をぶつけることはせず、アルゴリズムの複雑さと外部呼び出しの数が最小限であるシステムを選択します。
スマート コントラクトはこれらの要件に最も適しているため、Waves プラットフォームの RIDE コントラクトが選択されました。これらはチューリングが完全ではなく、最大の複雑さは人為的に制限されています。
ただし、ここでは技術的な側面からのみ検討します。
あらゆる契約に加えて、正式な検証が特に求められるのは、契約開始後に契約上の誤りを修正することは通常不可能であるためです。
そして、スマートコントラクトには多額の資金が保管されることが多いため、このようなエラーのコストは非常に高くなる可能性があります。
私のシンボリック仮想マシンは PHP と Python で書かれており、Microsoft Research の Z3Prover を使用して結果の SMT 式を解きます。
その中心となるのは強力なマルチトランザクション検索です。
多くのトランザクションが必要な場合でも、解決策や脆弱性を見つけることができます。
偶数 は、イーサリアムの脆弱性を発見するための最も強力なシンボリック フレームワークの XNUMX つですが、この機能は数か月前に追加されたばかりです。
しかし、イーサ契約はより複雑であり、チューリング完全であることは注目に値します。
PHP は、RIDE スマート コントラクトのソース コードを Python スクリプトに変換します。このスクリプトでは、プログラムが、コントラクトの状態とその遷移条件の Z3 SMT 互換システムとして表示されます。
ここで、内部で何が起こっているのかを詳しく説明します。
その前に、RIDE スマート コントラクト言語について少し説明します。
これは関数型の式ベースのプログラミング言語であり、設計上遅延しています。
RIDE はブロックチェーン内で独立して実行され、ユーザーのウォレットにリンクされたストレージから情報を取得および書き込みできます。
RIDE コントラクトは各ウォレットにアタッチでき、実行結果は TRUE または FALSE のみとなります。
TRUE はスマート コントラクトがトランザクションを許可することを意味し、FALSE はトランザクションを禁止することを意味します。
簡単な例: ウォレット残高が 100 未満の場合、スクリプトで送金を禁止できます。
例として、同じオオカミ、ヤギ、キャベツを取り上げますが、すでにスマート コントラクトの形式で提示されています。
ユーザーは、全員を相手側に送信するまで、コントラクトが展開されているウォレットからお金を引き出すことはできません。
#Извлекаем положение всех объектов из блокчейна
let contract = tx.sender
let human= extract(getInteger(contract,"human"))
let wolf= extract(getInteger(contract,"wolf"))
let goat= extract(getInteger(contract,"goat"))
let cabbage= extract(getInteger(contract,"cabbage"))
#Это так называемая дата-транзакция, в которой пользователь присылает новые 4 переменные.
#Контракт разрешит её только в случае если все объекты останутся в сохранности.
match tx {
case t:DataTransaction =>
#Извлекаем будущее положение всех объектов из транзакции
let newHuman= extract(getInteger(t.data,"human"))
let newWolf= extract(getInteger(t.data,"wolf"))
let newGoat= extract(getInteger(t.data,"goat"))
let newCabbage= extract(getInteger(t.data,"cabbage"))
#0 обозначает, что объект на левом берегу, а 1 что на правом
let humanSide= human == 0 || human == 1
let wolfSide= wolf == 0 || wolf == 1
let goatSide= goat == 0 || goat == 1
let cabbageSide= cabbage == 0 || cabbage == 1
let side= humanSide && wolfSide && goatSide && cabbageSide
#Будут разрешены только те транзакции, где с козой никого нет в отсутствии фермера.
let safeAlone= newGoat != newWolf && newGoat != newCabbage
let safe= safeAlone || newGoat == newHuman
let humanTravel= human != newHuman
#Способы путешествия фермера туда и обратно, с кем-то либо в одиночку.
let t1= humanTravel && newWolf == wolf + 1 && newGoat == goat && newCabbage == cabbage
let t2= humanTravel && newWolf == wolf && newGoat == goat + 1 && newCabbage == cabbage
let t3= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage + 1
let t4= humanTravel && newWolf == wolf - 1 && newGoat == goat && newCabbage == cabbage
let t5= humanTravel && newWolf == wolf && newGoat == goat - 1 && newCabbage == cabbage
let t6= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage - 1
let t7= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage
let objectTravel = t1 || t2 || t3 || t4 || t5 || t6 || t7
#Последняя строка в разделе транзакции описывает разрешающее транзакцию условие.
#Переменные транзакции должны иметь значения 1 или 0, все объекты должны
#быть в безопасности, а фермер должен переплывать реку в одиночку
#или с кем-то на каждом шагу
side && safe && humanTravel && objectTravel
case s:TransferTransaction =>
#Транзакция вывода средств разрешена только в случае если все переплыли на другой берег
human == 1 && wolf == 1 && goat == 1 && cabbage == 1
#Все прочие типы транзакций запрещены
case _ => false
}
PHP はまず、スマート コントラクトからすべての変数をキーと対応するブール式変数の形式で抽出します。
cabbage: extract ( getInteger ( contract , "cabbage" ) )
goat: extract ( getInteger ( contract , "goat" ) )
human: extract ( getInteger ( contract , "human" ) )
wolf: extract ( getInteger ( contract , "wolf" ) )
fState: human== 1 && wolf== 1 && goat== 1 && cabbage== 1
fState:
wolf:
goat:
cabbage:
cabbageSide: cabbage== 0 || cabbage== 1
human: extract ( getInteger ( contract , "human" ) )
newGoat: extract ( getInteger ( t.data , "goat" ) )
newHuman: extract ( getInteger ( t.data , "human" ) )
goatSide: goat== 0 || goat== 1
humanSide: human== 0 || human== 1
t7: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage
t3: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage + 1
t6: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage - 1
t2: humanTravel && newWolf== wolf && newGoat== goat + 1 && newCabbage== cabbage
t5: humanTravel && newWolf== wolf && newGoat== goat - 1 && newCabbage== cabbage
t1: humanTravel && newWolf== wolf + 1 && newGoat== goat && newCabbage== cabbage
t4: humanTravel && newWolf== wolf - 1 && newGoat== goat && newCabbage== cabbage
safeAlone: newGoat != newWolf && newGoat != newCabbage
wolfSide: wolf== 0 || wolf== 1
humanTravel: human != newHuman
side: humanSide && wolfSide && goatSide && cabbageSide
safe: safeAlone || newGoat== newHuman
objectTravel: t1 || t2 || t3 || t4 || t5 || t6 || t7
次に、PHP はそれらを Python の Z3Prover SMT 互換システム記述に変換します。
データはループ内にラップされ、ストレージ変数はインデックス i、トランザクション変数はインデックス i + 1 を受け取り、式を持つ変数は前の状態から次の状態への遷移のルールを設定します。
これは仮想マシンのまさに心臓部であり、マルチトランザクション検索エンジンを提供します。
fState: And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 )
final: fState[Steps]
fState:
wolf:
goat:
cabbage:
cabbageSide: Or( cabbage[i] == 0 , cabbage[i] == 1 )
goatSide: Or( goat[i] == 0 , goat[i] == 1 )
humanSide: Or( human[i] == 0 , human[i] == 1 )
t7: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
t3: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] + 1 )
t6: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] - 1 )
t2: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage == cabbage[i] )
t5: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage == cabbage[i] )
t1: And( And( And( humanTravel[i] , wolf == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
t4: And( And( And( humanTravel[i] , wolf == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
safeAlone: And( goat[i+1] != wolf , goat[i+1] != cabbage )
wolfSide: Or( wolf[i] == 0 , wolf[i] == 1 )
humanTravel: human[i] != human[i+1]
side: And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] )
safe: Or( safeAlone[i] , goat[i+1] == human[i+1] )
objectTravel: Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] )
data: And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] )
条件はソートされ、Python で SMT システムを記述するように設計されたスクリプト テンプレートに挿入されます。
空のテンプレート
import json
from z3 import *
s = Solver()
Steps=7
Num= Steps+1
$code$
#template, only start rest
s.add(data + start)
#template
s.add(final)
ind = 0
f = open("/var/www/html/all/bin/python/log.txt", "a")
while s.check() == sat:
ind = ind +1
print ind
m = s.model()
print m
print "traversing model..."
#for d in m.decls():
#print "%s = %s" % (d.name(), m[d])
f.write(str(m))
f.write("nn")
exit()
#s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model
print "Total solution number: "
print ind
f.close()
チェーン全体の最後の状態には、転送トランザクション セクションで指定されたルールが適用されます。
これは、Z3Prover が最終的に契約から資金を引き出すことを可能にする一連の条件を正確に探すことを意味します。
その結果、契約の完全に機能する SMT モデルを自動的に受け取ります。
これは、手動でコンパイルした前の記事のモデルと非常によく似ていることがわかります。
完成したテンプレート
import json
from z3 import *
s = Solver()
Steps=7
Num= Steps+1
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) ]
nothing= [ And( human[i] == human[i+1], wolf[i] == wolf[i+1], goat[i] == goat[i+1], cabbage[i] == cabbage[i+1] ) for i in range(Num-1) ]
start= [ human[0] == 1, wolf[0] == 0, goat[0] == 1, cabbage[0] == 0 ]
safeAlone= [ And( goat[i+1] != wolf[i+1] , goat[i+1] != cabbage[i+1] ) for i in range(Num-1) ]
safe= [ Or( safeAlone[i] , goat[i+1] == human[i+1] ) for i in range(Num-1) ]
humanTravel= [ human[i] != human[i+1] for i in range(Num-1) ]
cabbageSide= [ Or( cabbage[i] == 0 , cabbage[i] == 1 ) for i in range(Num-1) ]
goatSide= [ Or( goat[i] == 0 , goat[i] == 1 ) for i in range(Num-1) ]
humanSide= [ Or( human[i] == 0 , human[i] == 1 ) for i in range(Num-1) ]
t7= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t3= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] + 1 ) for i in range(Num-1) ]
t6= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] - 1 ) for i in range(Num-1) ]
t2= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t5= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t1= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t4= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
wolfSide= [ Or( wolf[i] == 0 , wolf[i] == 1 ) for i in range(Num-1) ]
side= [ And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] ) for i in range(Num-1) ]
objectTravel= [ Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] ) for i in range(Num-1) ]
data= [ Or( And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] ) , nothing[i]) for i in range(Num-1) ]
fState= And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 )
final= fState
#template, only start rest
s.add(data + start)
#template
s.add(final)
ind = 0
f = open("/var/www/html/all/bin/python/log.txt", "a")
while s.check() == sat:
ind = ind +1
print ind
m = s.model()
print m
print "traversing model..."
#for d in m.decls():
#print "%s = %s" % (d.name(), m[d])
f.write(str(m))
f.write("nn")
exit()
#s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model
print "Total solution number: "
print ind
f.close()
起動後、Z3Prover はスマート コントラクトを解決し、資金を引き出すことができる一連のトランザクションを提供します。
Winning transaction chain found:
Data transaction: human= 0, wolf= 0, goat= 1, cabbage= 0
Data transaction: human= 1, wolf= 0, goat= 1, cabbage= 1
Data transaction: human= 0, wolf= 0, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 0, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Transfer transaction
フェリー契約に加えて、独自の契約を試したり、2 つのトランザクションで解決されるこの簡単な例を試したりすることができます。
let contract = tx.sender
let a= extract(getInteger(contract,"a"))
let b= extract(getInteger(contract,"b"))
let c= extract(getInteger(contract,"c"))
let d= extract(getInteger(contract,"d"))
match tx {
case t:DataTransaction =>
let na= extract(getInteger(t.data,"a"))
let nb= extract(getInteger(t.data,"b"))
let nc= extract(getInteger(t.data,"c"))
let nd= extract(getInteger(t.data,"d"))
nd == 0 || a == 100 - 5
case s:TransferTransaction =>
( a + b - c ) * d == 12
case _ => true
}
これは最初のバージョンであるため、構文が非常に限られており、バグがある可能性があります。
次の記事では、VM のさらなる開発について取り上げ、問題を解決するだけでなく、その助けを借りて正式に検証されたスマート コントラクトを作成する方法を示す予定です。
キャラクター仮想マシンは次の場所から入手できます。
シンボリック VM のソース コードを整理してコメントを追加した後、GitHub に公開して自由にアクセスできるようにする予定です。
出所： habr.com