この記事はコミュニティへの寄稿です。著者: Dimitris Tsapis 氏、Web3 スマート コントラクト監査会社である CertiK のエンジニアリング担当副社長。
TL;DR
正式な検証により、スマート コントラクトにバグ、脆弱性、その他の意図しない動作が存在しないことが保証されます。このプロセスには、人間の専門家がスマート コントラクトのロジックを数学的データの形式で表示し、コントラクトの予想される動作のモデルに対して実際のロジックを自動的にチェックするプロセスを実行します。正式な検証と手動監査を組み合わせることで、スマート コントラクトのセキュリティを包括的に評価できます。
はじめに
スマート コントラクトは、ブロックチェーン上に展開され、特定の条件が満たされたときに自動的に実行されるコンピューター プログラムであり、単純なプログラムから複雑なプログラムまで多岐にわたり、数十億ドル相当の資産を保持することができます。
スマート コントラクト コードのセキュリティの脆弱性は、スマート コントラクトが保持するすべての資産の盗難など、壊滅的な結果をもたらす可能性があります。 2021 年、自動マーケットメーカーの Uranium Finance は、スマート コントラクトの 1 つのタイプミスにより 5,000 万ドルの盗難に遭いました。
また、2021 年には、Compound Finance プロトコルにより、単一のトークン エラーの結果として 8,000 万ドル相当の不獲得報酬が配信されました。 2022 年中に、スマート コントラクトの 1 つにおけるプログラミング エラーの結果、ワームホール ブリッジから 3 億 2,000 万ドルが盗まれました。
最初からスマート コントラクト ソフトウェアを正しく使用することが重要です。スマート コントラクトはオープンソース コントラクトです。つまり、コントラクトが公開されると、コードは一般公開されます。ハッカーがバグを見つけた場合、すぐにそれを悪用する可能性があります。さらに、スマート コントラクト コードは通常、展開後に変更できないため、時間をかけてセキュリティの脆弱性に対処することはできません。
スマートコントラクトの検証はどのように機能しますか?
スマート コントラクトの正式な検証は、スマート コントラクトに必要なロジックと動作を計算データの形式で公開することによって機能します。監査人は自動ツールを使用してデータを検証できます。
プロセスには次のものが含まれます。
契約の望ましい仕様と特徴を公用語で指定する。
契約コードをモデルや数理論理学フレームワークなどの正式なプレゼンテーションに変換します。
定理証明またはモデル検査ツールを使用して、契約の仕様と特性を監査します。
検証プロセスを繰り返して、エラーや必要な特性からの逸脱を見つけて修正します。
スマートコントラクトの検証が重要なのはなぜですか?
数学的推論を使用すると、正式に検証されたスマート コントラクトにバグ、脆弱性、その他の意図しない動作がないことを確認できます。また、契約の特性が注意深く検証されているため、契約に対する信頼性も高まります。
ここでは、スマート コントラクトの検証が重大な経済的損失やその他の悲惨な結果を防ぐのにどのように役立つかを示す例をいくつか紹介します。
ユニスワップ
Uniswap は有名な自動マーケットメーカーです。 Uniswap V1 スマート コントラクトが開発されたとき、それは正式に検証されました。この公式検証プロセスは、開始前に、Uniswap V1 資金の盗難につながる可能性のある丸めエラーを見つけて修正することができました。
バランサー
Balancer V2 は、正式に検証された自動マーケットメーカーでもあります。公式検証プロセスでは、間違った手数料アカウントを見つけて修正することができ、スマートコントラクトにフラッシュローン機能が組み込まれていたため、取引プラットフォームが盗難の危険にさらされる可能性がありました。
セーフムーン
SafeMoon V1 には、公開後の公式検証によって発見された気づかれないバグが含まれていました。所有権が放棄される前に特定の操作が実行された場合、所有者は契約の所有権を放棄し、再度取得することが可能でした。
このエラーを見つけるには、特定のプログラム変数値のセットを分析する必要があるため、SafeMoon V1 分割のほとんどの手動監査ではエラーは気付かれません。これは人間にとっては見落としやすいものですが、機械にとっては見つけやすいものです。
正式な検証と手動監査がどのように連携するか
形式的検証は、契約のロジックと動作を目的のプロパティに対して検証する体系的かつ自動的な方法を提供します。これにより、潜在的なエラーやバグを特定して修正することが容易になります。これは、手動スキャンでは検出するのが難しい複雑で気づかれていない問題を見つける場合に特に役立ちます。
手動監査プロセスには、契約コードと設計、およびその公開に対する専門家のレビューが含まれます。監査人は専門知識を活用してセキュリティ リスクを特定し、契約全体のセキュリティ ステータスを評価します。また、正式な検証プロセスが正しく完了したことを確認し、自動ツールでは検出できない可能性のある問題がないかチェックします。
正式な検証と手動監査を組み合わせることで、スマート コントラクトのセキュリティを包括的に評価できます。これにより、脆弱性を発見して修正できる可能性が高まります。その結果、人間とマシンの独自の機能を活用した、セキュリティに対する多層防御のアプローチが実現します。
まとめ
スマート コントラクトのセキュリティを確保するには、正式な検証プロセスと手動監査の両方を使用して、スマート コントラクトのセキュリティ ステータスを包括的かつ正確に評価する必要があります。
正式な検証はリソースを大量に消費する可能性がありますが、高価値または高リスクのスマート コントラクトにとっては価値のある投資です。最後に、セキュリティを優先し、スマート コントラクトにバグ、脆弱性、その他の意図しない動作がないことを保証することが重要です。
関連記事
スマートコントラクトとは何ですか?
スマートコントラクトのセキュリティ監査とは何ですか?
免責事項とリスク警告: このコンテンツは、一般的な情報および教育目的のみを目的として「現状のまま」提供されており、いかなる種類の表明や保証もありません。これは財務上のアドバイスとして解釈されるべきではなく、特定の製品やサービスの購入を推奨するものでもありません。デジタル資産の価格は変動する可能性があります。投資価値は増減する可能性があり、投資額を取り戻せない場合があります。あなたは自分の投資決定に対して単独で責任を負い、Binance Academyはあなたが被る可能性のある損失については責任を負いません。これは経済的なアドバイスではありません。