この記事はコミュニティからの投稿です。著者は、Web3 スマート コントラクト監査会社 CertiK のエンジニアリング担当副社長である David Tarditi です。
この記事の見解は寄稿者/著者のものであり、必ずしも Binance Academy の見解を反映するものではありません。
TL;DR
スマート コントラクトの形式検証により、スマート コントラクトにバグ、脆弱性、その他の意図しない動作がないことが保証されます。この検証では、人間の専門家がスマート コントラクトのロジックを数学的なステートメントとして提示し、実際のロジックをコントラクトの予想される動作のモデルと照合する自動プロセスを実行します。形式検証と手動監査を組み合わせることで、スマート コントラクトのセキュリティを包括的に評価できます。
導入
スマート コントラクトは、ブロックチェーン上に展開され、特定の条件が満たされると自動的に実行されるコンピュータ プログラムです。シンプルなものから非常に複雑なものまでさまざまで、数百万ドル、さらには数十億ドル相当の資産を保有できます。
スマート コントラクト コードのセキュリティ上の脆弱性は、スマート コントラクトが保有するすべての資産の盗難など、壊滅的な結果をもたらす可能性があります。2021 年には、自動マーケット メーカー (AMM) の Uranium Finance が、スマート コントラクトの 1 つのタイプミスにより 5,000 万ドルを盗まれました。
また、2021年には、Compound Financeが1文字の間違いで8000万ドルの未獲得報酬を支払った。2022年には、スマートコントラクトの1つにバグがあったため、Wormhole Bridgeから3億2000万ドルが盗まれた。
スマート コントラクト プログラムを最初から正しく実行することが重要です。スマート コントラクトはオープン ソースです。つまり、コントラクトがデプロイされると、コードは公開されます。ハッカーがバグを見つけた場合、すぐにそれを利用できます。さらに、スマート コントラクトのコードは通常、デプロイ後に変更できないため、時間の経過とともにセキュリティの脆弱性を修正することはできません。
スマートコントラクトの検証はどのように機能しますか?
スマート コントラクトの形式検証は、スマート コントラクトのロジックと望ましい動作を数学的なステートメントとして提示することによって機能します。その後、監査人は自動化されたツールを使用して、これらのステートメントが正しいかどうかを確認します。
このプロセスには以下が含まれます。
契約の仕様と望ましい特性を正式な言語で定義します。
契約のコードを数学モデルやロジックなどの正式な表現に変換します。
自動化された定理証明器またはモデルチェッカーを使用して、契約の仕様とプロパティを検証します。
検証プロセスを繰り返して、エラーや目的の特性からの逸脱を見つけて修正します。
スマートコントラクト検証が重要な理由
数学的推論を使用すると、正式に検証されたスマート コントラクトにバグ、脆弱性、その他の意図しない動作がないことが保証されます。また、そのプロパティが正しいことが厳密に証明されているため、コントラクトに対する信頼性と自信を高めることにも役立ちます。
以下は、スマート コントラクト検証が、重大な経済的損失やその他の悲惨な結果を防ぐのにどのように役立ったかを示す例です。
ユニスワップ
Uniswap は有名な AMM です。Uniswap V1 スマート コントラクトが開発されたとき、正式に検証されました。リリース前に、この正式な検証により、Uniswap V1 の資金枯渇につながる可能性のある丸め誤差が見つかり、修正されました。
バランサー
Balancer V2 も正式に検証された AMM です。正式な検証により、スマート コントラクトのフラッシュ ローン機能に関する誤った手数料計算が見つかり、修正されました。この計算により、取引所が盗難に対して脆弱になる可能性がありました。
セーフムーン
SafeMoon V1 には、導入後の正式な検証によって発見された微妙なバグが含まれていました。所有権を放棄する前に特定の操作を実行すると、所有者が契約の所有権を放棄して再度取得することが可能でした。
このバグは、SafeMoon V1 フォークのほとんどの手動監査では見逃されていました。これは、このバグを見つけるには、プログラム変数値の特定の組み合わせを分析する必要があったためです。これは、人間が見逃しやすいものですが、機械が見つけやすいものです。
形式検証と手動監査の連携方法
形式検証は、契約のロジックと動作を望ましい特性と照らし合わせてチェックする体系的かつ自動化された方法を提供します。これにより、潜在的なエラーやバグの特定と修正が容易になります。手動の検査では検出が難しい複雑で微妙な問題を見つけるのに特に役立ちます。
手動監査には、契約のコード、設計、展開の専門家によるレビューが含まれます。監査人は経験と専門知識を活用してセキュリティ リスクを特定し、契約の全体的なセキュリティ体制を評価します。また、正式な検証プロセスが正しく実行されたことを確認したり、自動化ツールでは検出できない問題がないか確認したりすることもできます。
形式検証と手動監査を組み合わせることで、スマート コントラクトのセキュリティを包括的かつ徹底的に評価できます。これにより、脆弱性を発見して修正できる可能性が高まります。その結果、人間と機械の両方の独自の機能を活用した、セキュリティに対する多層防御アプローチが実現します。
終わりに
スマート コントラクトのセキュリティを確保するには、形式検証と手動監査の両方を使用して、スマート コントラクトのセキュリティ体制を包括的かつ徹底的に評価することが不可欠です。
形式検証は多くのリソースを必要とする可能性がありますが、価値の高い契約やリスク要因の高い契約の場合は価値のある投資となります。最終的には、セキュリティを優先し、スマート コントラクトにバグ、脆弱性、意図しない動作がないことを確認することが重要です。
参考文献
スマートコントラクトとは何ですか?
スマートコントラクトのセキュリティ監査とは何ですか?
免責事項とリスク警告：このコンテンツは、一般的な情報と教育目的のみで「現状のまま」提供されており、いかなる表明や保証もありません。財務、法律、その他の専門的なアドバイスとして解釈されるべきではなく、特定の製品やサービスの購入を推奨することを意図したものでもありません。適切な専門アドバイザーから独自のアドバイスを求める必要があります。記事が第三者寄稿者によって寄稿されている場合、表明された見解は第三者寄稿者のものであり、必ずしもBinance Academyの見解を反映するものではないことにご注意ください。詳細については、こちらで完全な免責事項をお読みください。デジタル資産の価格は変動する可能性があります。投資の価値は下落または上昇する可能性があり、投資額が戻ってこない可能性があります。投資決定はお客様自身の責任であり、Binance Academyはお客様が被る損失について責任を負いません。この資料は、財務、法律、その他の専門的なアドバイスとして解釈されるべきではありません。詳細については、利用規約とリスク警告をご覧ください。
