スマート・コントラクトのセキュリティツールのガイド

3つの特徴的なテストおよびプログラム分析手法を使用します。

• スリザーを使用した静的解析。 プログラムのすべてのパスが近似され、さまざまなプログラム表現（制御フローグラフなど）を通じて同時に分析されます。
• エキドナを使用したファジング。 トランザクションの疑似乱数生成によってコードが実行されます。ファザーは、指定されたプロパティに違反するトランザクションのシーケンスを見つけようとします。
• マンティコアを使用したシンボリック実行。 各実行パスを数式に変換し、その上で制約をチェックできる形式的検証手法です。

各手法には利点と落とし穴があり、特定のケースで役立ちます。

* タイムアウトせずにすべてのパスが探索された場合

スリザーは数秒でコントラクトを分析しますが、静的解析は誤報を引き起こす可能性があり、複雑なチェック（算術チェックなど）にはあまり適していません。API経由でスリザーを実行すると、組み込みの検出器にボタン1つでアクセスでき、ユーザー定義のチェックもAPI経由で実行できます。

エキドナは数分間実行する必要があり、真陽性のみを生成します。エキドナは、Solidityで記述されたユーザー提供のセキュリティプロパティをチェックします。ランダムな探索に基づいているため、バグを見逃す可能性があります。

マンティコアは「最も重い」分析を実行します。エキドナと同様に、マンティコアはユーザー提供のプロパティを検証します。実行にはより多くの時間が必要ですが、プロパティの妥当性を証明でき、誤報を報告することはありません。

推奨されるワークフロー

スリザーの組み込み検出器から始めて、単純なバグが現在存在しないこと、または後で導入されないことを確認します。スリザーを使用して、継承、変数の依存関係、および構造上の問題に関連するプロパティをチェックします。コードベースが大きくなるにつれて、エキドナを使用して状態マシンのより複雑なプロパティをテストします。再びスリザーを使用して、関数がオーバーライドされるのを防ぐなど、Solidityでは利用できない保護のためのカスタムチェックを開発します。最後に、マンティコアを使用して、算術演算などの重要なセキュリティプロパティの的を絞った検証を実行します。

• スリザーのCLIを使用して一般的な問題を検出する
• エキドナを使用してコントラクトの高度なセキュリティプロパティをテストする
• スリザーを使用してカスタムの静的チェックを記述する
• 重要なセキュリティプロパティの詳細な保証が必要な場合はマンティコアを使用する

単体テストに関する注意。高品質なソフトウェアを構築するには単体テストが必要です。ただし、これらの手法はセキュリティ上の欠陥を見つけるのに最適ではありません。これらは通常、コードの肯定的な動作（つまり、コードが通常のコンテキストで期待どおりに機能すること）をテストするために使用されますが、セキュリティ上の欠陥は開発者が考慮しなかったエッジケースに存在する傾向があります。数十のスマート・コントラクトのセキュリティレビューに関する私たちの調査では、クライアントのコードで見つかったセキュリティ上の欠陥の数や重大度に単体テストのカバレッジは影響を与えませんでした (opens in a new tab)。

セキュリティプロパティの決定

コードを効果的にテストおよび検証するには、注意が必要な領域を特定する必要があります。セキュリティに費やせるリソースは限られているため、労力を最適化するには、コードベースの脆弱な部分や価値の高い部分をスコープすることが重要です。脅威モデリングが役立ちます。以下のレビューを検討してください。

• 迅速なリスク評価 (Rapid Risk Assessments) (opens in a new tab)（時間が限られている場合に推奨されるアプローチ）
• データ中心システムの脅威モデリングガイド (opens in a new tab)（別名 NIST 800-154）
• Shostackの脅威モデリング (opens in a new tab)
• STRIDE (opens in a new tab) / DREAD (opens in a new tab)
• PASTA (opens in a new tab)
• アサーションの使用 (opens in a new tab)

コンポーネント

チェックしたい内容を把握することで、適切なツールを選択するのにも役立ちます。

スマート・コントラクトに頻繁に関連する幅広い領域には、以下が含まれます。

• 状態マシン。 ほとんどのコントラクトは状態マシンとして表現できます。(1) 無効な状態に到達できないこと、(2) 状態が有効であれば到達可能であること、(3) コントラクトをトラップする状態がないことを確認することを検討してください。

  • エキドナとマンティコアは、状態マシンの仕様をテストするのに適したツールです。

• アクセス制御。 システムに特権ユーザー（所有者、コントローラーなど）がいる場合、(1) 各ユーザーが許可されたアクションのみを実行できること、および (2) どのユーザーもより特権のあるユーザーのアクションをブロックできないことを確認する必要があります。

  • スリザー、エキドナ、マンティコアは、正しいアクセス制御をチェックできます。たとえば、スリザーは、ホワイトリストに登録された関数のみに onlyOwner 修飾子がないことをチェックできます。エキドナとマンティコアは、コントラクトが特定の状態に達した場合にのみ付与される権限など、より複雑なアクセス制御に役立ちます。

• 算術演算。 算術演算の健全性をチェックすることは重要です。あらゆる場所で SafeMath を使用することは、オーバーフロー/アンダーフローを防ぐための良いステップですが、丸めの問題やコントラクトをトラップする欠陥など、他の算術上の欠陥も考慮する必要があります。

  • ここではマンティコアが最適な選択肢です。算術演算がSMTソルバーの範囲外である場合は、エキドナを使用できます。

• 継承の正確性。 Solidityのコントラクトは多重継承に大きく依存しています。シャドウイング関数に super 呼び出しが欠落していることや、C3線形化の順序の誤解などの間違いが簡単に導入される可能性があります。

  • スリザーは、これらの問題を確実に検出するためのツールです。

• 外部との相互作用。 コントラクトは互いに相互作用しますが、一部の外部コントラクトは信頼すべきではありません。たとえば、コントラクトが外部のオラクルに依存している場合、利用可能なオラクルの半分が侵害されても安全性を維持できるでしょうか？

  • マンティコアとエキドナは、コントラクトとの外部相互作用をテストするための最適な選択肢です。マンティコアには、外部コントラクトをスタブ化する組み込みメカニズムがあります。

• 標準への準拠。 イーサリアムの標準（ERC-20など）には、設計上の欠陥の歴史があります。構築の基盤としている標準の制限に注意してください。

  • スリザー、エキドナ、マンティコアは、特定の標準からの逸脱を検出するのに役立ちます。

ツール選択のチートシート

目標に応じて他の領域もチェックする必要がありますが、これらの大まかな重点領域は、あらゆるスマート・コントラクトシステムにとって良い出発点となります。

私たちの公開監査には、検証またはテストされたプロパティの例が含まれています。実際のセキュリティプロパティを確認するには、以下のレポートの Automated Testing and Verification セクションを読むことを検討してください。

• 0x (opens in a new tab)
• Balancer (opens in a new tab)