紹介

暗号経済内で異なるユースケースを立ち上げるいくつかのプロジェクトが急速にブロックチェーン上の資産の価値を増やす中、可能な弱点や脅威に先んじて対策を講じることがますます重要になっています。

Bitcoinは銀行を置き換えるために発明されましたが、その基盤技術であるブロックチェーンはほぼあらゆる中間業者を置き換えることができることが証明されました。さらに、デジタルマネーが持つ巨大なポテンシャルに目を向け、紙幣ではできなかったプログラム可能なお金の能力が含まれます。突然、弁護士や契約は金融取引で置き換えることができるようになりました。この形式のデジタル通貨は、契約の自動実行を可能にすることで分散化を進め、完全な透明性と人間の介入のないものとしました。しかし、スマートコントラクトは実際にはどのように動作するのでしょうか？信頼がないこれらのシステムを信頼することは本当に頼りになるのでしょうか？

この記事では、スマートコントラクトの形式的認証について、その利点、欠点、暗号生態系への影響などについて詳しく取り上げます。特にEthereumに重点を置いています。

スマートコントラクトの簡潔な歴史

Source: CryptoSlate

ニック・ザボは、アメリカのコンピューター科学者であり、しばしば中本哲史であると推測されている暗号学者であり、スマートコントラクトの先駆者であり、1994年にこの概念を初めて紹介しました。ザボは、スマートコントラクトを、契約条件を自動的に強制するように設計されたデジタル取引プロトコルとして説明しました。彼の目標は、POSシステムなどの電子取引方法を向上させ、その機能をデジタル世界に拡張することでした。

Szaboは、契約が自動化され、信頼性があり、改ざん防止された自動販売機のように機能する未来を想像していました。彼の時代のテクノロジーは彼のビジョンを完全に実現するには進化していませんでしたが、Szaboの考えは後にブロックチェーン業界を革命化する基盤を築きました。イーサリアムがローンチされました2015年、スマートコントラクトを実用化し、Szaboの理論的な概念を分散型アプリケーションの必須コンポーネントに変えました。

契約のビジョンは、精密な自動化された条件で関係を管理し、人間の介入と監視の必要性を減らすことでした。このアプローチは、合意を処理するより安全で効率的な方法を作り出し、スマートコントラクトがブロックチェーンエコシステムで強力なツールに進化する道を開くことを目指していました。Szaboの早期の洞察は、デジタルトランザクションとスマートコントラクトの開発の景観を今日も形作っています。

形式的認証とは何ですか？

ソース：中庸

形式的認証は、スマートコントラクトのようなシステムが定義されたルールや仕様に従って動作するかどうかを厳密に評価するプロセスです。基本的には、システムが期待通りに動作するかどうかをチェックし、必要な条件を満たし、意図した機能をエラーなく実行するかどうかを確認します。

このために、システムの予想される動作は、形式モデルを使用して概説され、仕様言語を使用して契約が満たす必要のある正確な性質を定義します。また、記事が進むにつれて、より実践的なシナリオも見ることができます。形式的検証技術では、契約の実装をその仕様と照合し、その正確性の数学的な証明を提供します。これらの仕様を満たす契約は、「機能的に正しい」または「設計による正しい」と見なされ、ブロックチェーン環境での信頼性とセキュリティが確認されます。

スマートコントラクトの形式的仕様の種類

ソース：エバースケール

形式的仕様は、数学的推論を使用してプログラムの実行の正確性を検証するための構造化された方法を提供します。これらの仕様は、全体的な動作に焦点を当てた高レベルなプロパティまたは契約が内部でどのように動作するかの詳細な説明を記述できます。これらの振る舞いを数学的に定義することにより、形式的仕様は、契約が意図した通りに機能することを保証します。

高レベルな仕様

ハイレベル仕様、またはモデル指向仕様としても知られるものは、スマートコントラクトの全体的な振る舞いを記述し、それを特定の操作を通じて異なる状態に遷移する有限状態機械（FSM）として扱います。時間論理は、これらの遷移を統治する形式的なルールを定義するためによく使用され、契約が時間の経過とともにどのように状態間を移動し、それを正しく行うための条件を詳細に説明します。

これらの仕様は、安全性と生存性という2つの重要な特性を捉えています。安全性は、送信者の残高がトランザクションに必要な金額以下になることを防止するなど、望ましくないイベントが発生しないようにします。一方、生存性は、ユーザーが要求したときに資金を引き出せるように流動性を維持するなど、契約が機能し続けて進行することを保証します。両方の特性は、スマートコントラクトが安全かつ信頼性があり、ユーザーの相互作用と資産を保護します。

低レベル仕様

低レベルの仕様は、プロパティ指向の仕様とも呼ばれ、スマートコントラクトの内部実行プロセスを分析して正しい動作を定義することに重点を置いています。高レベルの仕様が契約を有限状態機としてモデル化するのに対して、低レベルの仕様はスマートコントラクトを数学的関数のシステムとして捉え、契約の状態を変更するトレースと呼ばれる関数の実行シーケンスを調べます。

スマートコントラクトの形式的認証のための技術

ソース: エバースケール

モデルチェック

モデルチェックは、スマートコントラクトのモデルが仕様と一致しているかどうかを評価するためにアルゴリズムを使用する形式的検証手法です。スマートコントラクトは通常、状態遷移システムとして表現され、そのプロパティは時間的な論理このプロセスには、契約の数学モデルを作成し、論理式を通じてその特性を表現し、アルゴリズムがそのモデルがこれらの仕様を満たしているかどうかを検証できるようにすることが含まれています。

定理証明

モデル検査とは異なり、定理証明はスマートコントラクトを含むプログラムの正確性を確立するために使用される数学的アプローチです。この方法は、契約のモデルと仕様を論理式に変換して、それらの論理的同値性を検証することを含みます。つまり、一方の文が真であればもう一方も真であることを意味します。この関係を定理として定式化することで、自動定理証明器が契約モデルの正確性をその仕様に対して検証することができます。

モデル検査が有限状態システムに限定されているのに対し、定理証明は無限状態システムを分析できますが、複雑な論理問題を航行するために人間のガイダンスを必要とすることがよくあります。そのため、定理証明は完全に自動化されたモデル検査プロセスよりもリソースを多く必要とする傾向があります。

シンボリックエグゼキューション

シンボリック実行は、具体的な入力ではなくシンボリックな値を使用して関数を実行するスマートコントラクトの強力な分析手法です。この形式的な検証技術により、実行パスを数学的な式で表すことにより、契約のコードのトレースレベルのプロパティについての推論が可能になります。次に、SMTソルバを使用してこれらの述語が満足しているかどうかを判断します。つまり、条件を満たす入力が存在するかどうかを確認します。

たとえば、値が 5 から 10 の間にあるときにコントラクト関数が元に戻る場合、シンボリック実行では、条件を X > 5 ∧ X < 10 として評価することで、そのようなトリガー値を効率的に識別できます。この方法は、従来のテストよりも効果的であることが多く、誤検知が少なく、SMTソルバーを複製する具体的な値を直接生成して、見つかったエラーを特定するために採用されるため、スマートコントラクトの信頼性を確保するための貴重なツールになります。

スマートコントラクトとは何ですか？

Source: 優しく

スマートコントラクトは、特定の条件が満たされたときにアクションを実行するブロックチェーン上で動作する自動化されたコンピュータープログラムです。それらは単純な合意から非常に複雑なプロセスまでさまざまであり、数百万ドルまたは数十億ドルに評価される資産を管理することができます。

スマートコントラクトには、政治的投票、サプライチェーン管理、医療、不動産など、さまざまなセクターを革命化する可能性がありますが、この記事では引き続き、これらの影響に焦点を当てています。その設計により、複数の当事者が操作のリスクなしに協力することが可能であり、効率とイノベーションを高める透明性と安全なフレームワークを提供します。ただし、スマートコントラクトには脆弱性や課題も存在することを認識することが重要です。

スマートコントラクトの脆弱性

セキュリティの脆弱性スマートコントラクトコード内の脆弱性は、最近の事例で示されたように、契約内に格納された資産の完全な損失などの壊滅的な結果につながる可能性があります。

• 2021年、自動市場メーカーのウランファイナンスは5000万ドルの盗難被害を受けましたスマートコントラクト内の単純なタイプミスのために。
• 2021年もCompound Financeは誤って8000万ドルを配布しました未獲得の報酬が再び一文字のエラーのために発生しました。
• より重大な侵害が2022年に発生しましたWormhole Bridgeから3億2000万ドルが盗まれた時そのスマートコントラクトのバグのために。

これらの例を考慮すると、スマートコントラクトが最初から正確にコーディングされていることが重要です。デプロイされると、スマートコントラクトはオープンソースであり、そのコードは一般にアクセス可能です。これにより、ハッカーが発見された脆弱性を悪用することが容易になります。さらに、スマートコントラクトの不変性は、一度起動されると、通常、セキュリティ上の欠陥を修正するためにコードを変更することができないことを意味します。したがって、最高の精度で開発されていない場合、スマートコントラクトは常にリスクにさらされることになります。

スマートコントラクトの検証はどのように機能しますか？

Source: Certik

プロセスには次のものが含まれます:

• 形式的な言語を使用して契約の仕様と希望する特性を定義する。
• 契約のコードを数学モデルや論理式などの形式的表現に変換すること。
• 契約の仕様と特性の妥当性を確認するために、自動定理証明器またはモデルチェッカーが使用されています。
• 意図したプロパティからのエラーや逸脱を特定し、修正するために、検証プロセスを反復的に繰り返します。

スマートコントラクトの主な特長

ソース：Certik

スマートコントラクトを、作成されたら変更できない石に刻まれた契約と考えてください。ブロックチェーンの不変の台帳上で動作するこれらの契約は、中間者の必要なく条件を自動的に強制し、取引を加速しコストを下げます。この固定された性質はセキュリティを向上させ、コントロールを分散化し、詐欺や汚職の可能性を大幅に減らします。

スマートコントラクトの検証の重要性

数学的な推論は、形式的に検証されたスマートコントラクトがバグ、脆弱性、予期しない動作から解放されていることを保証する上で重要な役割を果たしています。この厳格なプロセスにより、契約の性質が徹底的に検証されるため、信頼と自信が高まります。

成功したスマートコントラクトの検証の例は、重大な財務的損失を防ぐ上でその重要性を示しています。

ユニスワップ

例えば、Uniswap、よく知られた自動化市場メーカー（AMM）は、V1スマートコントラクトの開発中に形式的な検証を受け、丸め誤差を特定して修正しました資金を失っていた可能性があります。

Balancer

同様に、別のAMMであるBalancer V2も、形式的な認証によって恩恵を受けました。誤った手数料計算フラッシュローンに関連する、潜在的な盗難を防止します。

SAFEMOON

SafeMoon V1には微妙なバグがありましたデプロイ後に形式的検証によって特定されました。 このバグにより、特定の条件下で所有権を放棄し、再取得することが可能となりました。 これは、複雑さのため、ほとんどの手動監査で見逃されていた詳細です。形式的検証の変数値の特定の組み合わせを分析する能力は、人間の監査者が見落す可能性のある問題をキャッチするための効果的なツールとなっています。

形式的認証と手動監査がどのように協力するか

形式的認証は、スマートコントラクトのロジックと動作を意図した特性に対して、体系的かつ自動化された方法を提供します。このアプローチにより、手動の検査では見落とされるかもしれない特に複雑な問題やバグを特定して修正することが容易になります。

一方、手動の監査では、契約のコード、デザイン、展開について、専門家が徹底的にレビューします。監査人は、自分の経験を活かしてセキュリティリスクを特定し、契約の全体的なセキュリティポストを評価します。また、形式的な検証プロセスの正確さを検証し、自動化ツールが見逃す可能性のある問題を特定することもできます。形式的な検証と手動監査を組み合わせることで、包括的なセキュリティ評価が行われ、脆弱性の発見と解決の可能性が高まり、人間の専門知識と自動化分析の両方の強みを活用した堅牢な防御戦略が確立されます。

スマートコントラクトの利点と欠点

ソース:ブロックノミ

スマートコントラクトは完璧ではありませんが、その利点は欠点を大幅に上回ります。複雑な取引を簡素化し、時間とお金を節約するだけでなく、透明性を促進し、紛争を減らします。コード上で動作するため、人為的なエラーを最小限に抑えます。暗号保護により、セキュリティが強固です。ただし、スマートコントラクトは柔軟性に欠け、予期しない状況に適応するのが難しい場合があります。また、それらを設定するには専門のコーディングスキルが必要であり、これが一部の人にとって障壁となる場合があります。これらの課題にもかかわらず、スマートコントラクトは産業を変革しています。

スマートコントラクトの利点

• タスクを自動化して、時間とお金を節約して効率を向上させます。
• 全ての関係者に同じ情報へのアクセスを提供することで透明性を向上させ、紛争を減らします。
• コードに頼ることで、人為的なミスを排除し、間違いを減らします。
• 改ざんを困難にするために暗号保護を利用し、セキュリティを強化する。

スマートコントラクトのデメリット

• 彼らの硬直した性質のために予測できない状況に対応する柔軟性が不足しています。
• 専門のコーディング知識が必要であり、普及が制限されています。

Ethereumスマートコントラクトのための形式的認証ツール

ソース：Calibraint

形式的認証の仕様言語

• Act: Actは、ユーザーがストレージの更新、事前条件、事後条件、および契約不変条件を定義できるようにします。ツールスイートには、Coq、SMTソルバー、またはhevmを使用してさまざまなプロパティを検証できる証明バックエンドが含まれています。

GitHub

ドキュメンテーション

• Scribble：Scribbleは、その仕様言語で書かれたコードアノテーションを特定のアサーションに変換して、仕様を検証します。

ドキュメンテーション

• Dafny: Dafnyは、高レベルの注釈を使用して検証のために設計されたプログラミング言語で、コードの正確性について推論し確認するのに役立ちます。

GitHub

正確性を確認するためのプログラム検証ツール

• Certora Prover: Certora Proverは、スマートコントラクトコードの正確性をチェックする自動形式的検証ツールです。仕様はCertora Verification Language（CVL）を使用して作成され、静的解析と制約解決技術の組み合わせによってプロパティの違反を検出します。

ウェブサイト

ドキュメンテーション

• Solidity SMTChecker: SolidityのSMTCheckerは、充足可能性モジュロ理論（SMT）とホーン解決を使用する統合モデルチェッカーです。コンパイル中に契約のソースコードが仕様と整合しているかどうかを検証し、安全性の違反をチェックします。

GitHub

• Solc-verify: Solc-verifyは、アノテーションとモジュラープログラムの検証を介して、Solidityコードの自動形式検証を可能にするSolidityコンパイラの拡張バージョンです。

GitHub

• KEVM：KEVMはEthereum仮想マシンを形式的に表現します(EVM)Kフレームワークを使用して作成されました。実行可能であり、到達可能性論理を介して特定のプロパティ関連の主張を検証できます。

GitHub

ドキュメンテーション

定理証明のための論理フレームワーク

• Isabelle: Isabelle/HOL は、ユーザーが数式を形式言語で表現するのを支援し、それらを証明するためのツールを提供する証明アシスタントです。その主な用途は、特にコンピューターのハードウェアとソフトウェアの正確性、およびプログラミング言語とプロトコルの特性を検証するための数学的証明を形式化することです。

GitHubの

ドキュメンテーション

• Coq - Coqは、定理とその正確性を検証するためのマシンチェックされた証明を対話的なプロセスを通じて作成することができるインタラクティブな定理証明器です。プログラムを定義することも可能です。

GitHub

ドキュメンテーション

スマートコントラクト内の脆弱なパターンを検出するためのシンボリック実行ベースのツール

• Manticore - シンボリック実行を使用してEVMバイトコードを解析するツール。

GitHub

ドキュメンテーション

• Hevm - hevmはEVMバイトコードの同等性をチェックするシンボリック実行エンジンです。

GitHub

• Mythril - Ethereumのスマートコントラクトにある脆弱性を見つけるために使用されるシンボリック実行ツール。

GitHub

ドキュメンテーション

結論

スマートコントラクトを保護するには、形式検証と手動監査を組み合わせて、セキュリティを包括的に評価することが重要です。正式な検証はリソースを大量に消費する可能性がありますが、高い利害関係や重大なリスクを伴う契約にとっては貴重な投資です。スマートコントラクトは単なる流行の概念ではありません。グローバルなビジネスオペレーションを変革しており、課題もありますが、効率を高め、エラーを最小限に抑え、セキュリティを強化する比類のない能力は無視できません。スマートコントラクトは、プロセスを簡素化し、デジタル取引への信頼を育む大きな可能性を秘めています。この目的のために、このテクノロジーを今日採用する組織は、透明性と信頼性を優先する未来で成功する態勢を整えることができます。