この記事はコミュニティ メンバーによって投稿されました。著者は、Web3 スマート コントラクト監査会社である CertiK のエンジニアリング担当副社長である David Tarditi です。
まとめ
スマート コントラクトを正式に検証することで、スマート コントラクトをエラー、脆弱性、その他の悪条件から保護します。このプロセスでは、人間の専門家がスマート コントラクトのロジックを数学的ステートメントに変換し、自動化されたプロセスを使用して実際のロジックをコントラクトの予想される動作のモデルと照合してチェックします。正式な検証と手動監査を組み合わせることで、スマートコントラクトのセキュリティの包括的な評価を行うことができます。
導入
スマート コントラクトは、ブロックチェーン上に展開され、特定の条件が満たされたときに自動的に実行されるコンピューター プログラムです。スマート コントラクトは、非常に単純な場合も非常に複雑な場合もあり、数百万ドル、場合によっては数十億ドル相当の資産を保持する場合があります。
スマートコントラクトのコードにセキュリティホールがある場合、犯罪者が保有するすべての資産が盗まれるなど、壊滅的な結果を招く可能性があります。 2021年、スマートコントラクトのタイプミスにより、オートメーションマーケットメーカー（AMM）のウラニウム・ファイナンスから5000万ドルが盗まれた。
2021年にも、Compound Financeは単一のコーディングエラーにより、誤って8,000万ドルの報酬を発行しました。 2022年、スマートコントラクトのミスにより、ワームホールブリッジから3億2000万ドルが盗まれました。
したがって、最初からスマート コントラクト プログラムを正しく入手することが重要です。スマート コントラクトはオープン ソース モデルを採用しています。これは、コントラクトがデプロイされるとコードが公開されることを意味します。ハッカーがバグを発見すると、すぐにそれを悪用する可能性があります。さらに、スマート コントラクトのコードは展開後に変更できないことが多いため、時間をかけてセキュリティの脆弱性にパッチを適用する通常の方法は効果がありません。
スマートコントラクトの検証はどのように機能しますか?
スマート コントラクトの正式な検証は、スマート コントラクトのロジックと予想される動作を数学的ステートメントとして提示することによって実現されます。次に、監査人は自動ツールを使用して、これらの記述が正しいかどうかをチェックします。
このプロセスには以下が含まれます。
契約の仕様と期待される特性を正式な言語で定義します。
契約のコードを数学モデルやロジックなどの正式なステートメントに変換します。
自動化された定理証明またはモデル検査を使用して、契約の仕様とプロパティを検証します。
検証プロセスを繰り返して、エラーや期待される特性からの逸脱を見つけて修正します。
スマートコントラクトの検証が重要な理由
数学的推論を適用することで、正式に検証されたスマート コントラクトにエラー、脆弱性、その他の不利な状況がないことを確認できます。また、検証は、契約のプロパティが厳密にテストされており、正確で信頼できるものであるため、契約に対する信頼性と信頼性を高めるのにも役立ちます。
以下の例では、スマート コントラクトの検証が、重大な経済的損失やその他の壊滅的な結果を防ぐのにどのように役立つかを概説します。
ユニスワップ
Uniswap はよく知られた AMM です。 Uniswap V1 スマート コントラクトは、開発プロセス中に正式な検証を受けました。リリース前に、この正式な検証によりいくつかの丸めエラーが発見および修正され、Uniswap V1 から資金が枯渇するのを防ぎました。
バランサー
Balancer V2 も実績のある AMM です。正式検証により、取引プラットフォームが盗難に対して脆弱な状態になっていたスマートコントラクトのフラッシュローン機能の手数料計算エラーが発見され、修正されました。
セーフムーン
SafeMoon V1 の導入後、正式な検証により非常に小さなエラーが発見されましたが、エラーが発見されなかった場合、契約所有者が所有権を放棄する前に特定の操作を実行した場合、契約所有者は契約を放棄した後にそれを取り戻す可能性があります。
SafeMoon V1 フォークの手動監査のほとんどは、このバグを見逃します。これは、バグを見つけるためにプログラム変数値の特定の組み合わせを分析する必要があるためです。人間はこの問題を見逃しがちですが、機械は時間内に発見することができます。
正式な検証と手動監査がどのように連携するか
正式な検証は、契約のロジックと動作を、期待される特性に照らしてチェックする体系的かつ自動化された方法を提供します。これにより、潜在的なバグや脆弱性の特定と修正が容易になります。これは、手動検査では検出するのが難しい複雑で微妙な問題に特に役立ちます。
手動監査には、契約のコード、設計、展開をレビューする専門家が関与します。監査人は、その経験と専門知識を活用してセキュリティ リスクを特定し、契約の全体的なセキュリティ体制を評価します。また、正式な検証プロセスが正しく実行されたことを確認し、自動ツールでは検出できない可能性のある問題がないかチェックすることもできます。
正式な検証と手動監査を組み合わせることで、スマートコントラクトのセキュリティの包括的な評価を行うことができます。これにより、脆弱性が発見されて修正される可能性が高まります。その際、私たちは人間と機械の専門知識を組み合わせた多層防御のセキュリティ アプローチを採用しています。
結論
スマート コントラクトのセキュリティを確保するには、正式な検証と手動監査を組み合わせて、スマート コントラクトのセキュリティ体制を包括的かつ徹底的に評価する必要があります。
正式な検証はより多くのリソースを消費しますが、価値の高い契約やリスク要因が高い契約にとっては価値のある投資です。結局のところ、セキュリティは何よりも重要なので、必ずセキュリティを優先し、スマート コントラクトにバグ、脆弱性、予期せぬ有害な動作がないことを確認してください。
参考文献
スマートコントラクトとは何ですか?
スマートコントラクトのセキュリティ監査とは何ですか?
免責事項とリスク警告: この記事の内容は事実であり、一般的な情報および教育のみを目的としており、いかなる表明や保証も構成するものではありません。この記事は財務上のアドバイスとして解釈されるべきではなく、特定の製品やサービスの購入を推奨するものではありません。デジタル資産の価格は変動する可能性があります。投資価値は上昇することもあれば下落する可能性があり、投資元本が返還されない可能性があります。あなたは自分自身の投資決定に対して単独で責任を負い、Binance Academyはあなたが被る可能性のある損失に対して責任を負いません。この資料は財務上のアドバイスを構成するものではありません。
