本研究は、Event-B手法を用いてブロックチェーンの合意メカニズムおよびスマートコントラクトのための正式な検証フレームワークを提示します。このアプローチは、表現からの抽象化、不変性に基づく証明、時間的モデルチェックと、安全性、生存性、二重支出防止の形式的なチェックを展開前に組み合わせています。
この記事について
サマリー
要約
本研究は、Event-BとRodinプラットフォームを用いて、ブロックチェーンの合意メカニズムとスマートコントラクトの挙動に関する形式的根拠に基づく検証フレームワークを開発します。従来のアプローチが主にシミュレーションやケースベースの個別契約検証に依存していたのに対し、本研究は有限状態機械(FSM)抽象化、不変駆動証明、精緻モデリング、時間論理検証を統合し、作業証明(PoW)、ステーク証明(PoS)、および二重支出防止のメカニズムを解析しています。ソリディティスマートコントラクトはFSMに抽象化され、イベントBマシンとしてエンコードされるため、状態遷移や安全制約の正式な仕様が可能となります。取引の一意性、状態整合性、アクセス制御の強制、台帳不変保存などの安全性は、Rodinで自動生成される証明義務によって検証されます。合計312件の証明義務が作成され、そのうち287件(92%)は自動的に免除され、25件はインタラクティブに証明され、完全な不変カバレッジを実現しました。ライブネス特性は計算木ロジック(CTL)で指定され、モデルチェックによって検証され、デッドロックフリーと最終的な検証者選択がPoS条件下で確認されました。二重支出防止は、状態整合性台帳モデリングを用いて正式に実施され、すべての到達可能な状態で一意性制約が証明されました。PoWおよびPoSのプロトコルレベルのコンセンサスロジックは3つの抽象化レベルで洗練され、段階的な洗練を通じてブロックの整合性とバリデーターの正確性を確保しました。結果は、機械チェックによる証明がシミュレーションベースの評価を超えた検証可能な正確性保証を提供し、厳密かつ再現性の高い検証パイプラインを構築し、ブロックチェーンシステムにおける正確性保証とプロトコルレベルの堅牢性を高めていることを示しています。
概要
ブロックチェーン技術は、中央集権的な権威に依存せずに分散型記録管理を可能にする分散型台帳パラダイムへと進化しました。参加ノード間で台帳状態を複製し、合意メカニズムを通じて合意を得ることで、ブロックチェーンシステムはオープンかつ対立的な環境において完全性、透明性、改ざん抵抗性を提供します。Yagaら1が説明したように、ブロックチェーンアーキテクチャは暗号学的プリミティブ、分散コンセンサスプロトコル、ピアツーピア通信を組み合わせることで、検証済みの取引を計算的に変更できないものにします。プルーフ・オブ・ワーク(PoW)やプルーフ・オブ・ステーク(PoS)などのコアコンセンサスメカニズムは、バリデーターの選択、ブロック検証、台帳同期を規制します。さらに、スマートコントラクトは、あらかじめ定められたルールを自律的に実行するプログラマブルロジックを埋め込むことで、金融、医療、ガバナンスなどの分野で分散型アプリケーションを可能にします。ブロックチェーン技術が高価値かつ安全性が重要な環境でますます導入される中で、コンセンサスメカニズムやスマートコントラクトの動作の正確性を確保することは、運用上の信頼性を維持するために不可欠となっています。
分散型であるにもかかわらず、ブロックチェーンシステムは論理的およびプロトコルレベルの脆弱性に対して脆弱なままです。台帳の整合性制約が厳格に守られていない場合、二重支出攻撃が発生することがあります。コンセンサスレベルでの弱点、例えば誤った検証者選択ロジックや欠陥のあるブロック検証ルール、さらにスマートコントラクトの脆弱性(再エントリーや不適切なアクセス制御など)が、展開プラットフォームに大きな財務的損失をもたらしています。PoWおよびPoSプロトコルの挙動を評価するために経験的テストやシミュレーションフレームワークが広く用いられていますが、これらのアプローチは包括的な正確性保証ではなく、例示的な観察のみを提供します。シミュレーションベースの検証は、到達可能なすべての状態における不変性の保存を証明したり、すべての実行経路で安全性とライブネス特性を保証したりすることはできません。この制約は、観察分析を超えてブロックチェーンシステムについて厳密に推論できる数学的根拠に基づく検証技術の必要性を浮き彫りにしています。
形式手法は、数理論理を通じたシステム仕様化と検証を可能にすることで、そのような基盤を提供します。イベントBはこのパラダイムを段階的な洗練によって拡張し、システムを不変量によって制約され、遷移がガードされたイベントとしてモデル化される抽象状態機械として表現します。Rodinプラットフォームは証明義務を自動的に生成し、その放電を支持することで、不変性の保存と状態整合性の機械チェックによる検証を可能にします。B-Method7やZ8などの古典的仕様手法は、不変ベースの推論と形式的洗練が異なる開発段階でシステムの正しさを保証できることを示しています。これらの手法は、9、10、11、12、13の展開前に正確性を確保するために、ミッションクリティカルおよび安全重要システムで広く適用されています。UML-Bやグラフィカルな精緻化フレームワークなどの追加拡張は、複雑な産業システム14,15,16,17,18,19における精緻化モデリングのスケーラビリティをさらに示しています。これらの進展は、改良主導型形式モデリングが強力な正しさ保証を維持しつつ、システムの複雑さを効果的に管理できることを示しています。
ブロックチェーンシステムに対しても形式的な検証手法が検討されています。SMTベースの契約検証技術は、Solidityプログラム内のアサーションを自動的にチェックし、論理違反が発生した場合に反例を生成することができます。VERISOLのようなツールはスマートコントラクト検証2に有限状態抽象化を用い、定理証明アプローチは契約をF*21のような形式的推論フレームワークに変換します。さらに、イーサリアム仮想マシンの意味論的形式化により、実行意味論や脆弱性検出に関する厳密な推論が可能になります。同様に、Coqのような定理証明環境は、コンセンサスに関連するセキュリティ特性や取引的正しさの分析に適用されています。これらのアプローチは貴重な洞察を提供しますが、多くの場合、契約レベルの正確性やコンセンサスレベルの性質のいずれかに独立して焦点を当てています。システムレベルの台帳不変量、コンセンサス状態遷移、スマートコントラクトの挙動は、仕様層や検証アーティファクトをまたぐトレーサビリティを維持する統一された精錬ベースのフレームワークに統合されることは稀です。さらに、多くの既存の手法は、複数の精錬レベルにわたる体系的な不変性保持よりも脆弱性検出や論理的主張チェックを重視しています。
本研究は、Solidityスマートコントラクトの有限状態機械(FSM)抽象化と、Rodinプラットフォーム内でのイベントB精緻化モデリングおよび機械チェックによる証明義務の履行を統合した統一形式検証フレームワークを提案することで、この方法論的なギャップを埋めています。契約検証とコンセンサスモデリングを別々の問題として扱うのではなく、提案されたフレームワークは、PoWおよびPoSのプロトコルレベルの状態遷移、台帳整合性制約、トランザクションの一意性条件、スマートコントラクトの状態進化を単一の構造化モデル内で正式に規定しています。安全性特性—不変の保存、取引の一意性、制御された状態遷移、台帳の整合性—はイベントB不変量として表現され、自動生成される証明義務によって検証されます。時間的および実行順序依存の性質は計算木ロジックを用いて指定され、静的不変量を超えた正確性を確保するためにモデルチェックによって検証されます。重要な方法論的貢献は抽象層間での明示的なトレーサビリティの確立にあります。ソリディティ関数はFSM遷移に抽象化され、FSM遷移はイベントBイベントとして符号化され、不変量と時間的仕様は解放された証明義務やモデルチェック結果に直接結びつけられます。この構造化されたマッピングにより、各正しさ主張が機械検証された証拠によって裏付けられ、証明に基づく保証とシミュレーションに基づく観察を明確に区別します。
この作業の範囲は、正確さと分析的明快さを確保するために意図的に制限されています。モデリングは、コンセンサスメカニズムのためのプロトコルレベルの状態遷移、台帳の整合性制約、トランザクションの一意性特性、スマートコントラクトの状態挙動に焦点を当てています。メッセージ伝播遅延、ビザンチン対抗戦略、フォーク解決メカニズム、詳細なイーサリアム仮想マシンのガスセマンティクスなどのネットワークレベルの側面は、定義された抽象化境界の外に含まれます。これらのモデリング仮定を明示的に定義することで、検証請求が正式に検証された証拠と整合性を保つことを保証します。本論文の残りの部分では、抽象化手法、イベントBのモデリングと精緻化プロセス、不変および時間的検証の手順、そしてその結果としての検証結果を提示します。本研究は、ブロックチェーンプロトコルとスマートコントラクト検証を改良に基づく形式的モデリングと機械チェックによる証明に基づけることで、分散型台帳システムの方法論的厳密性を強化し、展開前の正確性保証を強化します。
アクセスが制限されています。このコンテンツを表示するにはログインするか、トライアルを開始してください。
プロトコル
研究の入力
本研究では、検証入力として2つのSolidityスマートコントラクトが使用されました。前者はSimple DAOスタイルの契約で、再参入のケーススタディとして使われました。2つ目は、契約レベルの制約を二重支出に対抗してテストするために設計された、薄くなった台帳/状態移行契約でした。元のSolidityソースコードは、このプロトコルで定義された抽象化および検証プロセスの入力として機能しました。このような契約に用いられる一般的な変換プロセスは 図1に示されており、検証中にSolidityのソースコードがFSM、Event-B、SMVモデルへ徐々に変換される様子を示しています。
境界のモデリング
形式的モデリングは、スマートコントラクトの制御フローロジックに焦点を当てており、関数のエントリーおよび終了の挙動、内部実行、契約レベルの状態遷移などが含まれます。関数の可視性(公開、外部、内部、プライベート)と、再進入解析に関連する対応するコールスタックの挙動が示されました。抽象的な遷移(呼び出し、送信、転送)はエーテルの転送操作として扱われました。
契約レベルの不変量は、取引の一意性を確保し、抽象境界内での二重支出を防ぐために定義されました。検証選択とブロック整合性要件を表現するために、プロトコルロジック抽象化層はプルーフ・オブ・ワークおよびプルーフ・オブ・ステークの両方のプロトコルレベルの状態遷移を基準に定義されました。
抽象化境界には、配信されるメッセージのスケジューリングや任意のホップ数による遅延、フォーク解決、ビザンチン戦略を用いたネットワーク敵対者、イーサリアム仮想マシンの意味論、ネットワークノードによるガスセマンティクス、例外伝播、非同期実行、複雑なフォールバック動作、ネットワークレベルの最終性など、ネットワーク層の要素は含まれていませんでした。したがって、二重支出決定の結果は契約レベルの不変量にのみ適用され、ネットワークレベルの最終性に関する合意にはなりません。
ツールと構成
RodinプラットフォームはEvent-B(バージョン3.7.0)モデルのモデリング、洗練、証明義務の生成、放電に使われました。これによりPP、ML、SMT、Atelier-Bの証明者が自動かつ対話的に証明を放出できるようになりました。nuXmvバージョン2.0.0は生成されたSMVモデル上で完全なCTL探索モードで実行され、CTLモデルチェックが行われました。
すべての検証実行はUbuntu 22.04 LTS、OpenJDK 11、Python 3.10.12を用いた制御された計算環境で行われました。Web3(7.6.0)、NetworkX(3.4.2)、Matplotlib(3.8.0)、Graphviz(0.20.3)、NumPy(1.26.4)、Pandas(2.2.2)がシミュレーションおよび可視化要素の実装に使用されました。この設計により、同じ実行条件下で形式的検証およびシミュレーション結果を再現できることが保証されました。
トランスフォーメーションワークフロー
この検証プロセスは4つの段階に分かれました。ソリディティ契約は最初に有限状態機械(FSM-SC)表現に翻訳されました。FSM-SCモデルはその後、Event-Bでエンコードされ、明確に指定された不変量と精緻度が示されました。FSM-SCの抽象化はnuXmvのSMVモデルに翻訳されました。検証結果は証明義務の免除およびCTLモデルチェックに関する統計として報告され、反例は事例として提供されました。
FSMの構造
各契約は有限状態機械として抽象化され、次のように定義されました。
ここで:
S = 状態の集合
S₀ = 初期状態
T = 遷移関係
V = 可視性マッピング
G = ガード述語
A = アクション/状態更新。
アルゴリズム1:SolidityからのFSM構築
入力:Solidityのソースコード
出力:FSM-SC
1) Solidity契約の抽象構文ツリーを解析する。
2) 構成者定義から初期状態 S₀ を作成する。
3) 各ソリディティ関数fに対して、異なる制御状態S_fを作成し、{public, external, internal, private}∈可視性V(f)を記録します。
4) 関数f内の各文について、状態変数の更新から要求/主張条件やアクションからガード述語を抽出して遷移tを導出します。
5) 遷移tをTに足す。
6) イーサ転送操作(呼び出し、送信、転送)、内部および外部呼び出し、デリゲートコール、自己破壊、tx.originの使用、条件分岐、ループ構造のための明示的な遷移タイプを作成する。
7) FSM-SC = (S, S₀, T, V, G, A) を返す。
そして各Solidity関数は異なるFSM制御状態に関連付けられています。脆弱性理解のために、脆弱性に関連する実行フロー、例えば外部呼び出しの後にバランス更新が続くフローは、順序付けられた遷移に明示的に抽象化されました。 図2 は、SimpleDAOスタイル契約のFSM-SC図の例を示しており、この構築段階でエントリ状態、外部呼び出し遷移、状態更新シーケンスがどのように抽象化されたかを示しています。
FSMをイベントBにエンコードする
FSM移行はイベントB構成として表現されました。すべての遷移はイベントBイベントに対応しており、特定のガードやアクションも含まれます。
アルゴリズム2:FSMからイベントBへの符号化
入力:FSM-SC
出力:イベントBマシンとコンテキスト
1) 契約の文脈でSTATE_SETと機能を定義する。
2) FSM制御状態および契約レベル状態を表す変数を宣言します。
3) 各FSM制御状態s s ∈ S をcurrent_state ∈ STATE_SETを用いて表現します。
4) 各遷移(s → s′, g, a)に対して、以下のイベントBイベントE_tを作成する:
5) ここで current_state = s ∧ g
6) current_state := S′ ∥適用(a)
7) V(f) から導出されたガードを用いて可視制約を符号化する。
8) 安全性と整合性の性質を捉えるためにinv1–inv9の不変量を定義する。
9) S₀とデフォルト値を割り当てて初期化を定義します。
状態の集合、現在の状態、関数の可視性、コールスタック、トランザクションタイムスタンプ、イーサ転送ステータス、代理コールフラグ、自己破壊フラグ、検証条件などがイベントBモデルで捉えられる変数の一部です。不変量(inv1-inv9)および初期化の動作(act1-act6)は形式仕様のものと一致します。 図3 はまた、脆弱性に関連するキーイベント、特に再進入関連の遷移がイベントBエンコーディングでどのように維持されているかのグラフィカルな表現も提供しています。この図は、図2に示されたFSM-SCモデルの構造パターンがどのように検証可能なイベントBイベントにマッピングされるかを説明しています。
洗練戦略
2段階の洗練が実装されました。高レベルの契約制御フローとコア不変量は抽象レベルで表現されました。洗練されたレベルでは、契約固有の制限、通話スタック制限、可視性制限、再入場防止条件が追加されました。
アルゴリズム3:洗練と証明義務の解除
入力:抽象機械および精錬機械
アウトプット:証明義務および統計の履行
1) Rodinの抽象機械に対する証明義務を生成する。
2) 自動校正器の実行と放電結果の記録。
3) 精錬された機械に対して精錬証明義務を生成する。
4) 精錬義務に自動証明を適用する。
5) 必要に応じて残された義務を対話的に履行すること。
6) 輸出証明統計および状況報告。
証明報告には、不変量の数、精緻レベル、生成された証明義務、自動放電率、インタラクティブ放電率、最終放電率が含まれていました。
CTLプロパティ仕様とモデルチェック
FSM-SC抽象化は、nuXmvにおける分岐時間時間検証用にSMVモデルに翻訳されました。
アルゴリズム4: FSMからSMVおよびCTLチェック
出力:PASS/FAIL検証結果および反例トレース(あれば)
1. FSM制御状態を列挙されたSMV変数状態として記録する。
2. FSM遷移をガードされたnext(state)割り当てに変換する。
3. 外部通話や残高更新など、脆弱性に関連する条件のフラグを維持すること。
4. nuXmvでCTLプロパティをエンコードし、モデルチェックを行います。
5. 性質が失敗した場合、FSM遷移列を表す反例トレースを生成する。
CTLチェックには、再エントリー命令の要件、転送操作後の状態更新の最終化、クリティカルセクションへの無制限再帰的エントリーの制限、デッドロックの回避が含まれていました。
セキュリティ特性の検証
再入を防ぐSimple DAOスタイルのコントラクトは、外部呼び出し間の安全な順序付けと不変およびCTL制約による状態更新の確保によって確認されました。許可される場合、これらのガードはアクセス制御の制約を確認し、不正な遷移が不変性によって制限されていることを確実にしました。縮小台帳モデルは、契約内の防止レベルで取引の一意性と台帳の一貫性の不変性を検証しました。
報告された出力
結果セクションでは、FSMの構造指標、イベントBモデル指標、義務証明およびCTL検証のための統計に関する報告が提供されます。形式的証明の結果とCTLモデルチェックの結果は別々に示され、不変量による正しさ保証の証拠と時間検証による時間検証の証拠を区別しています。
アクセスが制限されています。このコンテンツを表示するにはログインするか、トライアルを開始してください。
結果
本研究の成果は、Event-BおよびCTLモデルチェックの形式検証産物と、ブロックチェーンシミュレーションからの実行可能な情報を組み合わせています。これらの多層的な出力の組み合わせにより、スマートコントラクトの主要な動作、コンセンサスシステム、そして設計の限られた例示内での台帳健全性の制限の検証が可能となります。
環境設定と依存性検証
モデル変換、検証、シミュレーションに使用される実行環境は依存性の競合なしに起動されました。Web3、NetworkX、Matplotlib、Graphviz、NumPy、Pandasを使い、すべての暗号、数学、ブロックチェーンインタラクションパッケージが読み込まれました。 図4 に示されたコンソール出力は、実行時に必要なすべてのモジュールが特定され、存在していることを示しています。これは検証およびシミュレーション活動を行う前に計算環境の正確性を検証するためのものでした。
アクセスが制限されています。このコンテンツを表示するにはログインするか、トライアルを開始してください。
ディスカッション
形式的およびシミュレーションベースの検証は、当研究で用いられた多層検証システムが、明確に定義された抽象境界の下でスマートコントラクトの挙動、合意メカニズムの正確性、台帳の整合性を検証できることを示しました。イベントBは、不変量と精緻化に基づく論理5,6の観点から安全性、状態フロー、再侵入防止ロジックを数学的に根拠地に基づけた表現を提供します。証明放電率が高いという事実は、モデル化されるシステムが内部的に論理的に健全であり、9,10,11,12の重要システムの正しさを確立するための既知の形式的手法の使用と一致していることを意味します。PoSおよびPoWのシミュレーションでは、静的およびイベント変調の場合...
アクセスが制限されています。このコンテンツを表示するにはログインするか、トライアルを開始してください。
開示事項
著者には利益相反を主張するものはありません。
材料
| 名前 | 会社 | カタログ番号 | コメント |
|---|---|---|---|
| Rodinプラットフォーム(v3.7.0) | ロダンチーム/エクリプス財団 | https://www.event-b.org/install.html | イベントBのモデリング、精緻化、証明義務の生成と放電 |
| イベントB法 | サウサンプトン大学/ロディン・コミュニティ | https://www.event-b.org/ | 不変仕様と洗練のための形式的モデリングフレームワーク |
| nuXmv Model Checker (v2.0.0) | FBK(ブルーノ・ケスラー財団) | https://nuxmv.fbk.eu/ | CTL特性のシンボリックモデル検査 |
| Graphviz (v0.20.3) | グラフビズチーム | https://graphviz.org/ | FSMの可視化とグラフレンダリング |
| Python (v3.10.12) | Pythonソフトウェア財団 | https://www.python.org/downloads | シミュレーションおよび実行環境 |
| Web3.py (v7.6.0) | イーサリアム財団 / 貢献者 | https://web3py.readthedocs.io/ | ブロックチェーンの相互作用と取引シミュレーション |
| NetworkX(バージョン3.4.2) | NetworkX開発者 | https://networkx.org/ | ブロックチェーンおよびFSM構造のグラフモデリング |
| Matplotlib (v3.8.0) | Matplotlib開発チーム | https://matplotlib.org/ | マイニング時間とバリデーター分布のプロット |
| NumPy(v1.26.4) | NumPy 開発者 | https://numpy.org/ | 数値計算 |
| パンダス(v2.2.2) | パンダス開発チーム | https://pandas.pydata.org/ | データ解析と処理 |
| OpenJDK 11 | Oracle / OpenJDKコミュニティ | https://openjdk.org/projects/jdk/11/ | Rodinプラットフォームの必要な実行時間 |
| Ubuntu 22.04 LTS | キャノニカル社 | https://ubuntu.com/download | すべての実験用のオペレーティングシステム |
| 固体 | イーサリアム財団 | https://soliditylang.org/ | 入力として使用されるスマートコントラクトのソース言語 |
| nuXmv 入力言語(SMV) | FBK | https://nuxmv.fbk.eu/documentation.html | CTL検証のための中間モデル表現 |
参考文献
- Yaga, D., Mell, P., Roby, N., Scarfone, K. Blockchain Technology Overview. , National Institute of Standards and Technology. Gaithersburg, MD, USA. (2018).
- Wang, Y., et al. Formal specification and verification of smart contracts for Azure Blockchain. arXiv preprint. , (2019).
- Huth, M., Ryan, M. Logic in Computer Science: Modelling and Reasoning About Systems. , Cambridge University Press. Cambridge, U.K. (2004).
- Baier, C., Katoen, J. P. Principles of Model Checking. , MIT Press. Cambridge, MA, USA. (2008).
- Abrial, J. R. Modeling in Event-B: System and Software Engineering. , Cambridge University Press. Cambridge, U.K. (2010).
- Abrial, J. R., et al. Rodin: An open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12 (6), 447-466 (2010).
- Abrial, J. R. The B-Book: Assigning Programs to Meanings. , Cambridge University Press. Cambridge, U.K. (1996).
- Jacky, J. The Way of Z: Practical Programming with Formal Methods. , Cambridge University Press. Cambridge, U.K. (1996).
- Verma, S., Yadav, D., Chandra, G. Introduction of formal methods in blockchain consensus mechanism and its associated protocols. IEEE Access. 10, 66611-66621 (2022).
- Guha, S., Nag, A., Karmakar, R. Formal verification of safety-critical systems: A case study in airbag system design. Proc. Int. Conf. Intelligent Systems Design and Applications, , Springer. Cham, Switzerland. 107-116 (2021).
- Karmakar, R. Formal verification techniques: A comparative analysis for critical system design. Proc. Int. Conf. Intelligent Systems Design and Applications, , Springer. Cham, Switzerland. 93-102 (2022).
- Karmakar, R. Symbolic model checking: A comprehensive review for critical system design. Adv. Data Inf. Sci. , Springer. Singapore. 693-703 (2022).
- Said, M. Y., Butler, M., Snook, C. A method of refinement in UML-B. Softw. Syst. Model. 14 (4), 1557-1580 (2015).
- Snook, C. F., Butler, M. J. UML-B: A plug-in for the Event-B tool set. Proc. ABZ 2008: Abstract State Machines, B and Z, , Springer. 344-358 (2008).
- Ben Younes, A., Ben Ayed, L. From UML activity diagrams to Event-B for the specification and the verification of workflow applications. Proc. IEEE 32nd Int. Conf. Computer Software and Applications, , 643-648 (2008).
- Morris, K. V., Snook, C. Reconciling SCXML Statechart Representations and Event-B Lower Level Semantics. , Sandia National Laboratories. Livermore, CA, USA. (2016).
- Butler, M. Decomposition structures for Event-B. Proc. Integrated Formal Methods (IFM 2009), , Springer. Berlin, Heidelberg. 20-38 (2009).
- Butler, M. Incremental design of distributed systems with Event-B. Proc. Integrated Formal Methods (IFM 2009), , Springer. Berlin, Heidelberg. (2009).
- Le, T. C., Garriga, M., Pautasso, C., Stankovic, M. Proving conditional termination for smart contracts. Proc. ACM Workshop Blockchains, Cryptocurrencies, and Contracts, , (2018).
- Alt, L., et al. SMT-based verification of Solidity smart contracts. Proc. ISoLA 2018: Leveraging Applications of Formal Methods, , Springer. Cham, Switzerland. 376-388 (2018).
- Bhargavan, K., et al. Formal verification of smart contracts. Proc. ACM Workshop Programming Languages and Analysis for Security, , 91-96 (2016).
- Grishchenko, I., Maffei, M., Schneidewind, C. A semantic framework for the security analysis of Ethereum smart contracts. Formal Methods Secure Software Systems (PoST 2018), , Springer. Cham. 243-269 (2018).
- Nielsen, J. B., et al. Smart contract interactions in Coq. arXiv preprint. , (2019).
アクセスが制限されています。このコンテンツを表示するにはログインするか、トライアルを開始してください。
再版と許可
このJoVE記事のテキストまたは図の再利用許可をリクエスト
許可をリクエスト