これは、プログラム内のすべての脆弱性を見つけたり、存在しないことを証明したりできる最も強力な方法の1つです。
フォーマル検証のより詳細な説明は、私の以前の記事のウルフ、ヤギ、キャベツの問題を解決する例で見ることができます。
この記事では、タスクの正式な検証からプログラムに移行し、説明します
それらを自動的に正式なルールシステムに変換する方法。
このために、シンボリックな原理に基づいて、仮想マシンの類似物を書きました。
彼女はプログラムコードを解析し、それを連立方程式（SMT）に変換します。これは既にプログラムで解決できます。
シンボリック計算に関する情報はインターネット上ではなく断片的に表示されるため、
簡単に説明します。
文字計算は、広範囲のデータでプログラムを同時に実行する方法であり、プログラムの正式な検証のための主要なツールです。
たとえば、最初の引数が任意の正の値、2番目の負、3番目のゼロ、および出力引数（42など）を取ることができる入力条件を設定できます。
1回の実行でのシンボリック計算により答えが得られます。目的の結果とそのような入力パラメーターのセットの例を取得することは可能ですか。 または、そのようなパラメーターがないことの証明。
さらに、一般的には入力引数を可能な限りすべて設定し、管理者パスワードなどの出力のみを選択できます。
この場合、プログラムのすべての脆弱性を見つけるか、管理者パスワードが安全であることの証拠を取得します。
特定の入力データを使用したプログラムの古典的な実行は、シンボリックの特殊なケースであることに気付くかもしれません。
したがって、私のキャラクターVMは、標準の仮想マシンのエミュレーションモードでも機能します。
前の記事へのコメントでは、弱点についての議論とともに、正式な検証に対する公正な批判を見つけることができます。
主な問題は次のとおりです。
- 正式な検証は最終的にP = NPに基づいているため、組み合わせ爆発
- ファイルシステム、ネットワーク、およびその他の外部ストレージへの呼び出しを処理することは、確認がより困難です
- 顧客またはプログラマーが1つのことを考えたが、作業明細書で適切に説明しなかった場合の仕様のバグ。
その結果、プログラムは検証され、仕様に準拠しますが、作成者が期待したことはまったく実行されません。
この記事では、実際に正式な検証の適用を主に検討しているため、まだ額に負けず、アルゴリズムの複雑さと外部呼び出しの数が最小限のシステムを選択します。
スマートコントラクトはこれらの要件に最適な方法で適合するため、WavesプラットフォームのRIDEコントラクトを選択しました。チューリング完全ではなく、その最大の複雑さは人為的に制限されています。
ただし、それらは技術的な側面からのみ検討します。
すべてに加えて、契約については、正式な検証が特に求められます。原則として、開始後に契約エラーを修正することは不可能です。
また、このようなエラーの価格は非常に高くなる可能性があります。これは、かなりの量の資金がスマートコントラクトに保存されることが多いためです。
私のキャラクター仮想マシンはPHPとPythonで書かれており、Microsoft ResearchのZ3Proverを使用して、結果のSMT式を解決します。
その中心には、強力なマルチトランザクション検索があります。
大量のトランザクションが必要な場合でも、ソリューションまたは脆弱性を見つけることができます。
イーサリアムの脆弱性を検索するための最も強力なシンボリックフレームワークの1つであるMythrilでさえ、ほんの数か月前にこの機能を追加しました。
しかし、エーテルコントラクトはより複雑で、チューリングの完全性があることに注意してください。
PHPは、RIDEスマートコントラクトのソースコードをPythonスクリプトに変換します。このスクリプトでは、プログラムは、Z3 SMTと互換性のある移行の契約状態と条件のシステムの形式で提示されます。
次に、内部で何が起こっているかをより詳細に説明します。
しかし、最初に、スマートコントラクトの言語についてのいくつかの言葉がRIDEに当てはまります。
意図したとおりに怠expressionな関数型および式ベースのプログラミング言語です。
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は、それらをZ3Prover SMTとの互換性のあるPythonシステム記述に変換します。
データは、ストレージ変数がインデックス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("\n\n") 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("\n\n") 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のさらなる開発に焦点を当て、正式に検証されたスマートコントラクトをその助けを借りて作成する方法を示します。
シンボリック仮想マシンは、 http：//2.59.42.98/hyperbox/で入手できます。
ソースはgithubで入手できます： http : //github.com/scp1001/hyperbox
すべてのVMロジックは、hyperbox.phpとhyperbox2.phpの2つのファイルに含まれています