Milkomedaブリッジ・スマートコントラクトの形式的検証
TLDR: Milkomedaへの保証をより強固に! Certoraと共同で、MilkomedaブリッジのEVM側でSolidityスマートコントラクトを形式的検証しました。レポートはこちらをご覧ください。
ブロックチェーンの世界におけるセキュリティの重要性は計り知れず、Milkomedaでも非常に重要視しています。ブロックチェーンの相互運用性の拡大に伴い、ブロックチェーン・ブリッジはハッカーにとって大きな価値のあるターゲットになっています。
私たちはすでにMilkomedaブリッジの要素の監査を完了していますが、今回、他のプロトコルがほとんど行っていないことを行ったことを発表します：ブリッジのMilkomeda側でSolidityスマートコントラクトの形式的検証を完了したのです。
この記事では、形式的検証とは何か、スマートコントラクトに何ができるのか、そして手動プロセスとの比較について説明します。そして、Milkomedaのブリッジ・コントラクトの形式的検証の結果について説明します。
注：この事業は、ブリッジのMilkomeda側のSolidityコントラクトのみを対象としています。
形式的検証（Formal Verification）とは？
形式的検証は、スマートコントラクトのセキュリティを強化する方法として、非常に推奨されています。スマートコントラクトが設計通りに動作することを検証するために、形式的な方法を使用します。形式的手法は、数学と論理を組み合わせてコードの抽象的表現を作成し、通常、形式的仕様と呼ばれる別の形式的記述と比較することによって、コードについて推論するものです。
これにより、スマートコントラクトは、特定の形式仕様に照らして、その正しさ（意図したとおりに動作する能力）を評価することができます。仕様は、スマートコントラクトの意図された実行経路を記述する、形式言語で書かれた一連のステートメントで構成されています。
検証ツールは、コードの数学的表現と形式的仕様の両方を与えられ、仕様で記述された経路に従わない動作や出力を検索します。検証ツールは、論理式を操作して、無限の入力範囲におけるコントラクトの動作を推論し、コントラクトが常に有効であるか、コントラクトの意図する目的に反する入力があるかどうかを判断します。
形式的検証のためのオープンソース・ツールは複数存在し、また、独自のツールを持つ専門企業も存在します。私たちは、Certoraの熟練した専門家と協力して、Milkomedaスマートコントラクトの形式的検証を実施しました。彼らのクライアントには、DeFiの世界の大企業や、EVMベースのプロトコルのL1-L2ブリッジなどがあり、Certoraが実施した形式的検証によって保護されたTVLは320億ドル以上にのぼります。Certoraのツール群がどのように機能するかは、ホワイトペーパーで詳しく説明されています。
形式的検証 vs 監査および手動手法
手動による監査とテストはスマートコントラクトのセキュリティの重要な部分ですが、人間ベースの手法には大きな限界があり、形式的検証によって克服することができます。形式的手法は、無限の実行パスについてスマートコントラクトの動作を検証することができ、しばしばバグとなる入力や稀な動作を見つけることができます。これは、手動で行う場合には実現不可能なレベルのテストです。具体的な入力ではなく数式を扱うということは、検証ツールがコントラクトが取り得るあらゆる状態を追跡することを意味し、すぐには明らかにならない問題点にもフラグを立てることができるようになります。
これに対して、手作業による監査とテストでは、限られた数の入力と実行経路しか考慮できないため、バグを見逃す可能性が高くなります。また、手作業による方法は、監査人の専門知識と細部への注意力に依存するため、個人差が生じます。
Milkomedaブリッジ・コントラクトの形式的検証の成果
Milkomedaのブリッジ・コントラクトの形式的検証は成功しました。このプロセスにより、いくつかの問題が特定され、コントラクトが展開される前に対処・修正されました。形式的検証プロセスにより、Milkomedaブリッジ・コントラクトのセキュリティがより保証され、その信頼性と機能性に確信を持つことができました。
私たちは、大きな価値を扱うスマートコントラクトや複雑な構造を持つスマートコントラクトには、形式的検証を強くお勧めします。開発プロセスにおいて追加のステップとなりますが、それによって向上するセキュリティと保証は、その努力に十分見合うものです。
MilkomedaのSolidityスマートコントラクトが形式的検証を完了しました！
Milkomedaのブリッジ・コントラクトの形式的検証を完了したことを嬉しく思うとともに、今後もすべての開発においてセキュリティを優先していきます。この記事で、形式的検証のメリットとブロックチェーンの世界におけるその重要性について、少しでもご理解いただけたなら幸いです。
Solidityスマートコントラクトの形式的検証は、Milkomedaプロトコルの継続的な成長におけるステップの1つに過ぎません。今年もエキサイティングで画期的なアップデートをお届けしますので、ぜひフォローしてください。
Website: milkomeda.com
Twitter: @Milkomeda_com
Medium: @milkomedafoundation
dApp Store: /dapp-store
Formal Verification audit: Certora’s audit
