この記事はコミュニティからの投稿です。著者は、Web3 スマート コントラクト監査会社である CertiK のエンジニアリング担当副社長である David Tarditi 氏です。
まとめ
正式な検証により、スマート コントラクトにバグ、脆弱性、その他の望ましくない動作が存在しないことが保証されます。このプロセスでは、専門家がスマート コントラクト ロジックを数学的ステートメントで表し、実際のロジックとコントラクトの予想される動作のモデルを比較する自動化されたプロセスを通じてそれを実行します。正式な検証と手動監査を組み合わせることで、スマート コントラクトのセキュリティを包括的に評価できます。
導入
スマート コントラクトは、特定の条件が満たされたときに自動的に実行される、ブロックチェーン上に実装されたコンピューター プログラムです。スマート コントラクトは単純なものから非常に複雑なものまで多岐にわたり、数百万ドル、場合によっては数十億ドル相当の資産を保管することができます。
スマート コントラクト コードのセキュリティの脆弱性は、スマート コントラクトによって保存されているすべての資産の盗難など、有害な結果を引き起こす可能性があります。 2021年、スマートコントラクトのミスにより、オートメーションマーケットメーカー（AMM）ウラニウムファイナンスの資金5000万ドルが盗まれた。
また、2021年には、Compound Financeは、単一の文字エラーにより、8,000万ドルの不獲得報酬を発行しました。 2022 年、スマート コントラクトの 1 つのバグにより、ワームホール ブリッジから 3 億 2,000 万ドルが盗まれました。
最初にスマート コントラクトを正しくプログラムすることが重要です。スマート コントラクトはオープンソースです。つまり、コントラクトの実装後にコードが公開されます。ハッカーはバグを発見すると、すぐにそれを悪用することができます。さらに、スマート コントラクト コードは通常、展開後に変更できないため、時間をかけてセキュリティの脆弱性を修正することは良い選択肢ではありません。
スマートコントラクトの検証はどのように機能しますか?
正式なスマート コントラクトの検証は、スマート コントラクトのロジックと望ましい動作を数学的ステートメントの形式で提示することによって機能します。次に、監査人は自動ツールを使用して、記述が正しいことを確認します。
プロセスには次のものが含まれます。
契約の仕様と望ましい特性を正式な言語で定義します。
契約コードを数学的モデルや論理モデルなどの形式的な表現に変換します。
定理証明器または自動モデルチェッカーを使用して、契約の仕様と特性を検証します。
検証プロセスを繰り返して、エラーや望ましい特性からの逸脱を見つけて修正します。
スマートコントラクトの検証が重要な理由
数学的推論を使用すると、正式な検証を受けたスマート コントラクトにバグ、脆弱性、その他の望ましくない動作が存在しないことを確認できます。これは、契約の特徴が真実であることが証明されるため、契約に対する信頼と自信を高めるのにも役立ちます。
以下は、スマート コントラクトの検証が大きな経済的損失やその他の悪影響を防ぐのに役立ったことを示すいくつかの例です。
ユニスワップ
Uniswap はよく知られた AMM です。 Uniswap V1 スマート コントラクトは実装時に正式な検証を経ています。リリースに先立って、この正式な検証により、Uniswap V1 の資金流出の原因となった可能性のある丸め誤差が発見され、修正されました。
バランサー
Balancer V2 も正式な検証を経た AMM です。正式な検証により、取引所を盗難に対して脆弱にする可能性があるフラッシュ ローン機能に関連する誤った手数料計算が発見され、修正されました。
セーフムーン
SafeMoon V1 には、展開後の正式な検証によって発見された微妙なバグが含まれていました。所有者は、契約の所有権を放棄し、所有権を放棄する前に特定の操作を実行した場合に契約を取り戻すことができます。
このバグは、プログラム変数値の特定の組み合わせを分析する必要があるため、SafeMoon V1 フォークのほとんどの手動監査では見逃されました。これらのバグは人間にとっては見落とされやすく、機械にとっては追跡しやすいものです。
正式な検証と手動監査を組み合わせる利点
正式な検証は、契約のロジックと動作を望ましい特性と比較する体系的かつ自動化された方法を提供します。これにより、潜在的なエラーやバグの特定と修正が容易になります。このプロセスは、手動検査では検出するのが難しい複雑で微妙な問題を発見するのに特に役立ちます。
手動監査では、専門家が契約のコード、設計、実装をレビューします。監査人は、その経験と専門知識を活用してセキュリティ リスクを特定し、契約の全体的なセキュリティ体制を評価します。また、正式な検証プロセスが正しく実行されていることを確認し、自動ツールでは検出できない可能性のある問題を探すこともできます。
正式な検証と手動監査を組み合わせることで、スマート コントラクトのセキュリティを包括的かつ徹底的に評価できます。これにより、脆弱性を発見して修正できる可能性が高まります。その結果、人間とマシンの固有の機能を活用したセキュリティに対する多層防御のアプローチが実現します。
閉鎖
スマートコントラクトのセキュリティを確保するには、正式な検証と手動監査を使用して、スマートコントラクトのセキュリティ体制を包括的かつ包括的に評価することが重要です。
多くのリソースが必要ですが、高価値または高リスクの要素を含む契約の場合、正式な検証は投資する価値があります。最終的には、セキュリティを優先し、スマート コントラクトにバグ、脆弱性、望ましくない動作が存在しないようにすることが重要です。
参考文献
スマートコントラクトとは何ですか?
スマートコントラクトのセキュリティ監査とは何ですか?
免責事項とリスク警告: このコンテンツは、一般情報および教育目的のみを目的として「現状のまま」提供されており、いかなる種類の表明や保証もありません。このコンテンツは財務上のアドバイスとみなされるべきではなく、特定の製品やサービスの購入を推奨することを目的としたものでもありません。デジタル資産の価格は変動する可能性があります。投資価値は下落または上昇する可能性があります。投資金額が戻ってこない場合があります。投資決定についてはお客様ご自身が全責任を負います。 Binance Academy は、お客様が経験する可能性のある損失に対して責任を負いません。この資料は財務上のアドバイスとして解釈されるべきではありません。
