一文で理解するスマートコントラクトの形式的認証

イントロダクション

ブロックオンチェーン資産の価値が急速に上昇するにつれ、各プロジェクトはさまざまな暗号化経済アプリケーションシナリオを次々に提供しています。このような状況では、潜在的な脆弱性や脅威を予防することが以前よりも重要になります。

BTCは最初は銀行を置き換えるために設計されましたが、ブロックチェーン技術はすべての仲介者を置き換える能力を持っていることを示しています。このプロセスで、デジタルマネーの新たな可能性がもたらされました。たとえば、プログラマブルな通貨は紙幣では実現不可能です。このデジタルマネーは契約の自動実行を許可し、透明性が高く人為的な介入を必要としない方法で分散化の発展を推進しています。これにより、弁護士や契約は金融取引で置き換えられる可能性があります。しかし、スマートコントラクトは実際にはどのように機能し、信頼できる信頼性のないシステムとは何でしょうか？

本文では、スマートコントラクトの形式的認証について詳しく探求し、その利点や欠点、暗号化エコシステムへの影響について分析し、特にイーサリアムの応用に焦点を当てます。

スマートコントラクト发展简史

源： CryptoSlate

ニック・サボ（Nick Szabo）は、アメリカのコンピュータ科学者および暗号学者であり、しばしば中本聡とされています。スマートコントラクトの創始者として、彼は1994年に「スマートコントラクト」という概念を初めて提案しました。サボは、デジタルトランザクションプロトコルによって自動的にプロトコル条項を実行するためのものとしてスマートコントラクトを定義しました。彼の意図は、POSシステムなどの電子取引方法を改善し、その能力をデジタル領域に拡張することです。

サーボの未来のプロトコルは、自動化され、信頼性があり、改ざんできないように自動販売機のようになると想定されています。当時の技術的条件では彼の考えを完全に実現することはできませんでしたが、その理念は後のブロックチェーン産業の革新の基礎を築きました。2015年、イーサリアムの発表により、スマートコントラクトが実際に利用されるようになり、サーボの理論も分散化アプリケーションの重要な技術となりました。

彼のビジョンは、契約が正確で自動化された条項で関係を管理し、人為的な介入と監視の必要性を減らすことを可能にすることです。この方法は、より安全で効率的なプロトコル管理方法を提供し、スマートコントラクトの発展を促進し、それをブロックチェーンエコシステムの重要なツールにします。サボの初期の洞察は、今日でもデジタル取引とスマートコントラクトの発展に影響を与え続けています。01928374656574839201

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

源： Medium

形式的認証は、システム（スマートコントラクトなど）が既定のルールや仕様に適合しているかを厳密に検証するプロセスです。要するに、システムが予期通りに動作し、必要条件を満たし、所定の機能をエラーなく実行できるかを検証するものです。

この目標を達成するために、この検証技術はまず形式モデルを使用してシステムの期待される動作を記述し、次に仕様言語を使用して契約が満たす必要がある具体的な条件を定義します。記事が進むにつれて、より多くの実際のケースを見ることができます。形式的認証技術は、数学的な手法を使用して契約の実際の実行状況とその仕様を対照し、その正確性を確保します。これらの仕様に合致すると、契約は「機能的に正しい」または「設計が正しい」と見なされ、それにより、そのブロックチェーン環境での信頼性と安全性が確認されます。

スマートコントラクトの形式化された仕様タイプ

出典: Ever Scale

形式的な仕様は、プログラムの実行が正確であるかどうかを数学的な推論によって検証するために使用されます。これらの仕様は、全体的な動作（ハイレベル）や契約の内部の実行の詳細（ローレベル）から記述することができます。数学的に契約の動作を定義することで、形式的な仕様は契約が予想どおりに動作することを保証します。

ハイレベルな仕様

高層仕様、またはモデル駆動仕様とも呼ばれるものは、スマートコントラクトの全体的な実行状態を記述し、有限状態機（FSM）として扱います。特定の操作によって異なる状態間を変換します。時系列ロジックは、これらの変換のルールを定義するためによく使われ、契約が時間とともに状態を変化させる方法や満たす必要のある条件を詳細に説明します。

高層規範は主に2つの側面に重点を置いています：セキュリティと活性化。セキュリティは、送信者の口座残高がトランザクションを行うために不十分な場合など、予期しないイベントの発生を防ぐことができます。活性化は、契約が正常に継続して実行されることを保証し、十分な流動性を維持してユーザーがいつでも資金を引き出せるようにします。両方がスマートコントラクトの安全性と信頼性を確保し、ユーザーの資産と相互作用の体験を保護します。

低レベルのスペック

低水準仕様は、属性指向型仕様とも呼ばれ、コントラクトの内部実行プロセスを分析して、その動作が正しいかどうかを定義することに重点が置かれます。高水準仕様がコントラクトを有限状態機として扱うのに対して、低水準仕様はスマートコントラクトを数学的な関数システムとして扱い、関数の実行順序（軌跡と呼ばれる）を分析し、これらの軌跡がコントラクトの状態変化を引き起こすことがあります。

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

出典: Ever Scale

モデル検出

モデル検出は、スマートコントラクトのモデルが予め定義された規格に準拠しているかを確認するために、アルゴリズムを使用する検証方法です。スマートコントラクトは通常、状態遷移システムとして表され、その特性は時系列論理によって定義されます。この手法は、数学モデルを作成し、その振る舞いを論理式で記述することで、アルゴリズムがそのモデルが要件を満たしているかを検証します。

定理の証明

モデル検査とは異なり、定理証明はプログラム（スマートコントラクトを含む）の正確性を検証するための数学的手法です。この手法は契約のモデルと仕様を論理式に変換し、それらの論理的同値性を検証するものであり、つまり、1つの命題が真であるとき、別の命題も真となります。この関係を定理として表現することで、自動定理証明ツールは契約モデルとその仕様の正確性を検証できます。

有限状態システムに限定されたモデル検査とは異なり、定理証明は無限状態システムを分析することができますが、通常、複雑な論理問題を解決するために人の指導が必要です。したがって、定理証明は完全自動化されたモデル検査よりも時間と労力がかかることがよくあります。

シンボルの実行

シンボル実行は、関数を具体的な入力ではなく、シンボル値を使用して実行する強力なスマートコントラクト分析手法です。この方法により、契約の実行パスが数学的式（パス述語と呼ばれる）に変換され、SMTソルバーを利用してこれらの述語が成立するかどうか、つまり条件に合致する入力が存在するかどうかが決定されます。

例えば、ある契約関数が値が5から10の間でロールバックが発生する場合、シンボリック実行は条件X > 5 および X < 10 を評価することで、この条件をトリガーする値を迅速に見つけることができます。この方法は従来のテストよりも効果的であり、誤検知率が低く、エラーを引き起こす具体的な数値を直接生成することができるため、スマートコントラクトの信頼性を確保する強力なツールとなります。

什么是スマートコントラクト？

源： Tenderly

スマートコントラクトはブロックチェーン上で動作する自動化プログラムであり、特定の条件を満たすと自動的に対応する操作を実行します。それらは簡単なプロトコルから複雑なプログラムまで、数百万ドルまたは数十億ドルの資産を管理することができます。

スマートコントラクトは、政治投票、サプライチェーン管理、医療、不動産などの領域を根本的に変革する可能性がありますが、この記事では、暗号資産の領域での利用に焦点を当てています。スマートコントラクトの設計により、ロングはリスクを心配することなく協力できるようになり、透明かつ安全なフレームワークを提供し、効率とイノベーションを向上させることができます。ただし、スマートコントラクトにはまだセキュリティの脆弱性や課題が存在することにも注意が必要です。

スマートコントラクトのセキュリティの脆弱性

スマートコントラクトコードのセキュリティ上の欠陥は、コントラクト内のすべての資産の損失など、壊滅的な結果につながる可能性があります。 最近の出来事は、この点を十分に示しています。

• 2021年、自動マーケットメーカーであるUranium Financeは、スマートコントラクトのタイプミスにより、5,000万ドル(https://cointelegraph.com/news/50m-reportedly-stolen-from-bsc-based-uranium-finance)を盗みました。 ※また2021年、Compound Financeは文字ミスにより誤って8,000万ドルを発行 未獲得の報酬。
• 2022年、Wormhole Bridgeはスマートコントラクトの脆弱性により3億2000万ドルを盗まれました。

これらの例は、スマートコントラクトのデプロイ前に、そのコードの正確性を確認する必要があることを示しています。スマートコントラクトはオープンソースであり、一度デプロイされると、コードは公開され、ハッカーは見つけた脆弱性を簡単に悪用できます。さらに、スマートコントラクトの不変性は、一度公開されると、セキュリティ上の脆弱性は通常修正できないことを意味します。したがって、開発が不正確な場合、それらは常にリスクの中にあります。

スマートコントラクト的验证是如何进行的？

源： Certik

このプロセスには、次の手順が含まれます：

• 形式言語を使用して契約の仕様と期待される機能を明確にします。 *契約コードを数学的モデルや論理式などの形式的な表現に変換します。
• 自動定理検証器またはモデルチェッカーを使用して、契約の仕様とプロパティが有効かどうかを確認します。
• 繰り返し検証し、予期された属性と一致しないエラーや偏差を発見し修正する。

スマートコントラクト的关键特性

源： Certik

スマートコントラクトは、一度作成されると変更することはできない「石に刻まれたプロトコル」と見なすことができます。これらの契約は、改ざんできないブロックチェーン台帳上で実行され、仲介者なしで条項を自動的に実行するため、取引を加速しコストをドロップします。この固定された特性は、安全性を高めるだけでなく、分散化された管理を実現し、詐欺や腐敗のリスクを大幅にドロップします。

スマートコントラクトの検証がなぜ重要なのか？

数学的推論により、形式的認証は、スマートコントラクトに欠陥、エラー、または予期しない動作がないことを保証します。契約の実行プロセスの厳格さは、契約への信頼を大幅に高めます。なぜなら、その機能と特性が徹底的に検証されているからです。

スマートコントラクトの検証の成功事例は、重大な財務損失を回避する上での重要な役割を示しています。

ユニスワップ

例えば、有名な自動マーケットメーカーであるUniswapは、V1スマートコントラクトの開発中に資金の損失(https://hexn.io/blog/exploring-the-need-for-formal-verification-in-smart-contracts-323)につながる可能性のあるバグを発見し、修正しました。

バランサー

同様に、別のAMMバランサーV2は、フラッシュローンに関連する手数料計算エラーを正式に検証することで、盗難の潜在的なリスクを回避します。

セーフムーン

SafeMoon V1はデプロイ後に形式的認証によって微妙なバグが特定されました。このバグにより、所有者は特定の条件下で所有権を放棄し、制御権を再取得することができます。この詳細は、複雑さのためにほとんどの人間の監査に見落とされています。形式的認証は、変数値の特定の組み合わせを分析することで、監査の漏れがある可能性を効果的に捕捉することができます。

形式検証と手動監査はどのように連携するのですか?

形式的認証は、スマートコントラクトの論理と振る舞いが予想される機能に合致しているかどうかを検査するための自動化されたシステム的方法です。この方法により、特に人工的な監査では見落とす可能性がある複雑な問題を発見し、修正するプロセスが簡素化されます。

一方、人工監査は専門家が契約のコード、設計、展開を包括的にチェックするものです。監査人は彼らの経験を活用して潜在的なセキュリティ上のリスクを発見し、契約の全体的なセキュリティ状況を評価することができます。彼らはまた、形式的な認証プロセスの正確性を検証し、自動化ツールが見落とす可能性のある脆弱性を見つけることができます。形式的な認証と人工監査を組み合わせることで、包括的なセキュリティ評価を提供し、脆弱性の発見と修正の可能性を高め、過去の経験と自動化分析を組み合わせて強力なセキュリティ防御線を確立することができます。

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

源： Blockonomi

スマートコントラクトは完璧ではありませんが、利点は欠点を大幅に上回ります。複雑な取引を簡素化し、時間とコストを節約し、ワークフローの透明性を高め、紛争を減らすことができます。さらに、スマートコントラクトはコードの実行に依存しているため、人為的なエラーも減少します。また、暗号化により、非常に高いセキュリティが確保されています。ただし、スマートコントラクトは柔軟性に欠け、予期しない状況に対応するのが難しいです。また、スマートコントラクトを設定するには専門のプログラミングスキルが必要であり、これは一部の人にとって障壁となります。課題は存在しますが、スマートコントラクトは複数の産業の変革を推進しています。

スマートコントラクト的优点

• 自動化された操作により、効率が向上し、時間とお金が節約されます。
• 透明性を高め、論争を減らし、すべての関係者が同じ情報にアクセスできます。
• エラーを減らし、コードに依存するため人為的なエラーを排除します。
• 暗号化技術によるセキュリティの強化により、改ざんが困難になります。

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

• 柔軟性に欠け、予期せぬ状況に対応するのが難しいです。
• 専門のプログラミングスキルが必要で、技術的なハードルに依存して広く使用されています。

ETH坊スマートコントラクト的形式的認証工具

源： Calibraint

形式的な仕様を記述するための言語

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

(https://github.com/ethereum/act)[GitHub]

[ユーザードキュメント] (https://ethereum.github.io/act/)

• Scribble：Scribbleは、特定の言語で書かれたコードコメントを検証仕様のアサーションに変換することができます。

[ユーザードキュメント] (https://docs.scribble.codes/)

• Dafny: Dafnyは設計の検証に特化したプログラミング言語であり、高度な注釈を使用してコードの正確性を推論および検証するのに役立ちます。

(https://github.com/dafny-lang/dafny)[GitHub]

コントラクトの正当性を検証するためのツール

• Certora Prover：Certora Proverは、スマートコントラクトのコードの正確性をチェックするために特別に設計された自動形式的認証ツールです。Certora検証言語（CVL）を使用して契約の仕様を作成し、静的解析および制約解決技術を使用して潜在的な属性違反を検出します。

【公式サイト】 (https://www.certora.com/)

[ユーザードキュメント] (https://docs.certora.com/en/latest/index.html)

• Solidity SMTChecker: これはSolidityの組み込みモデル検査ツールであり、SMT（充足可能性モデル理論）およびHorn解決技術を使用して、コントラクトのソースコードがコンパイル時に指定された仕様を満たし、セキュリティプロパティが違反されていないかを検出します。

(https://github.com/ethereum/solidity)[GitHub]

• Solc-verify：Solc-verifyはSolidityコンパイラの拡張版であり、コメントとモジュール化されたプログラムの検証により、Solidityコードの自動形式の認証を実現することができます。

(https://github.com/SRI-CSL/solidity)[GitHub]

• KEVM：KEVMは、Kフレームワークを使用して作成されたETHブロックチェーンの仮想マシン（EVM）の形式的表現です。 KEVMは、可達性ロジックを使用して特定の属性を検証し、実行することができます。

(https://github.com/runtimeverification/evm-semantics)[GitHub]

[ユーザードキュメント] (https://jellopaper.org/)

定理証明ツールフレームワーク

• Isabelle: Isabelle/HOLは、数学の公式を形式言語で表現し、それらの証明を提供するための証明アシスタントであり、これらの公式を証明するためのツールを提供します。主に数学的な証明を形式化するために使用され、特にコンピュータハードウェア、ソフトウェア、プログラミング言語などの正確性を検証するために使用されます。

(https://github.com/isabelle-prover)[GitHub]

[ユーザードキュメント] (https://isabelle.in.tum.de/documentation.html)

• Coq：Coqは、対話型定理証明ツールであり、対話型プロセスを通じて、ユーザーがプログラムや定理を定義し、機械が検証可能な正当性の証明を作成するのを支援します。

(https://github.com/coq/coq)[GitHub]

[ユーザードキュメント] (https://coq.github.io/doc/v8.13/refman/index.html)

シンボリック実行に基づく脆弱性検出ツール

• Manticore - Manticoreは、EVMバイトコードをシンボリックに実行して解析するツールであり、脆弱性の検出に特化しています。GitHub

[ユーザードキュメント] (https://github.com/trailofbits/manticore/wiki)

• Hevm- hevmはEVMバイトコードの等価性を検査するためのシンボル実行エンジンです。

(https://github.com/dapphub/dapptools/tree/master/src/hevm)[GitHub]

• Mythril - Mythrilは、ETHブロックチェーンのスマートコントラクト内の潜在的な脆弱性を発見するためのシンボリック実行ツールです。

(https://github.com/ConsenSys/mythril-classic)[GitHub]

[ユーザードキュメント] (https://mythril-classic.readthedocs.io/en/develop/)

まとめ

スマートコントラクトの安全性を確保するためには、形式的認証と人工監査を組み合わせることが重要です。この組み合わせにより、契約の安全性を総合的に評価できます。形式的認証はリソースを消費するため、高リスクまたは大量の資金が関係する契約にとっては、投資する価値があります。スマートコントラクトは人気のある概念にとどまらず、世界のビジネスにおいて重要な役割を果たしています。いくつかの課題が存在するにもかかわらず、スマートコントラクトは効率の向上、エラーの減少、セキュリティの向上において独自の優位性を持っています。彼らはビジネスプロセスを簡素化し、デジタル取引における信頼性を高めるでしょう。この技術を採用している企業は、将来、暗号化経済の透明性と信頼性を強調することになるでしょう。01928374656574839201