セキュアなスマートコントラクト開発ライフサイクルの最新情報
2023年にREKTされないための考察とベストプラクティス
Tom Lindeman（トム・リンデマン、 CEO、5thnode LTD
本書には、スマートコントラクトのセキュリティに関する最新の開発モデルが含まれており、複数の大手監査法人による実際の事例と、いくつかの最新のリソースやツールへのリンクが含まれています。本書は、新しいブロックチェーン・プロジェクトの概要、ガイド、チェックリストとして使用されることを意図しており、多くの例がイーサリアムのものですが、どのチェーン上のどのプロジェクトにも適用することができます。本書には、現在のスマートコントラクトのセキュリティに関する学習と技術を包括的に示すために、さまざまなソースやツールへのリンクが含まれています。また、これは次のフェーズに進む前に完了しなければならない厳格なステップであることを意図しているわけではなく、むしろこれらは特定のプロジェクトに適合させることができる潜在的なアクションとみなすべきであることにご留意ください。
デザイン＆モデル
仕様書の作成
新しいブロックチェーン・プロジェクトを始める際には、現在のスマートコントラクトのセキュリティに精通し、スマートコントラクトのベストプラクティスや準備ガイドに従い、シミュレーションを行い、Open Zeppelin標準ライブラリを使用して、「それほどスマートではない」コントラクトという落とし穴を避けることで、コントラクトやシステム・アーキテクチャ、経済性、エンドユーザー行動を計画・設計することが重要です。これらのガイドはイーサリアムに基づいて書かれていますが、他のチェーンやスマートコントラクト言語にも通じる有用なアイデアや事例がいくつかあります。
一般的に、以下のパターンに従うことができ、各開発チームのスタイルや専門性に応じて適応させることができます。より多くのステップを完了させることができればベターです。
セキュリティ、テスト、不変条件などを考慮したビジネス・ロジックと詳細な仕様を作成する。これらは最終的にプロの監査法人に渡され、コードが仕様に合致しているかどうかを検証してもらう。
すべてのコア・プロパティと機能を定義し、100％包括的な仕様書を作成するようにする。すべての外部機能をリストアップしたテーブルを検討する。
初期のテストケースを作成し、プロパティの潜在的な不変条件を考慮する。使用するテストツールやハーネスを決定し、ツールの使用方法について教育を開始する。ツールを作成したチームと話したり、Discordに参加したり、サンプルを見たりするのもよいでしょう。
他のプロトコルと統合する場合や、外部市場について想定している場合は、複雑なDeFiシナリオのシミュレーションを実行する。スマートコントラクトの相互作用、特にブリッジのようなクロスチェーンのシナリオの潜在的な挙動を予測することは非常に重要です。
潜在的な監査法人に接触し、デプロイ後のセキュリティと監視を早期に行う監査の計画を立てる。多くの監査法人は数ヶ月以上先まで立て込んでいるため、コード完成までのロードマップができ次第、監査法人に連絡してください。
信頼できるセキュリティ会社に設計と仕様の全面的な見直しを依頼する。仕様をより多くチェックしてもらうほうがベターですので、あなたのビジネス・ロジック、機能、スマートコントラクトの使用が一般的に安全であることを第三者機関が独立して確認する必要があります。 セキュリティ監査で見つかる問題は、コードの間違いではなく、仕様の間違いに帰結することが多いので、これはよいお金の使い方です。コード・レビューで問題が見つかると、大規模な再設計が必要になるため、コストや手間がかかることがあります。
上級者向け：ビジネス・ロジックを数式で正式にモデル化し、形式的検証の準備を整えることができるセキュリティ会社と連携する。この作業は、自動化ツールまたは手作業で行うことができますが、ほとんどの場合、その組み合わせになります。
デザイン・レビューの例
ここに、Runtime VerificationによるFolks Financeのデザイン・レビューが公開されています。これは、セキュリティ会社がスマートコントラクトについてどの程度深く推論することを期待すべきか、またどのようなフィードバックを受けるべきかを示す良い例となります。
強固なセキュリティを必要とする高価値のプロジェクトでは、仕様の形式的なモデルを作成することが強く推奨され、完全な形式的検証（後のセクションを参照）に向けた必須ステップでもあります。形式仕様の作成プロセスは、ビジネス・ロジックとプロパティの形式モデルを手動で作成し、有界モデル・チェックとモデルベースのテストを実行することからなります。この種のデザイン・レビューは、コードが書かれた時点で行うことも可能です。
形式的なモデリング例
Algofi v2仕様から、仕様を数学モデルに正式に変換する方法の例を紹介します。
「B資産の為替レートは決して低下してはならない。市場の利回り資産Bは貸し手の利息を発生させ、市場の原資産Uとの交換レートは、プロトコルとの相互作用のたびに、同じか増加しなければならない」
という数学的不等式が作成されました：
正式な数学モデルがあれば、テストやツールを使って、入力値がどうであれ式が常に真であることを検証することができます。
開発＆テスト
デベロッパー・ツール
開発チームは、Truffle、VS Code、Solidity plug-in for Visual Studio、Remix、Embark、Hardhat、Foundry、IntelliJ IDEA desktop IDEなど、さまざまなツールやフレームワークを使用してコーディングを行っています。新しいツールやIDEフレームワークが頻繁に登場しますが、どんなツールを使っても、目標は明確でテストや監査がしやすいコードを書くことです。
以下に他のツールをいくつか紹介しますが、ターゲットとするチェーンやプロジェクトに最適なものを見つけるために、ご自身で調べてみてください。
一般的な開発ガイドライン
見つけることのできるすべてのセキュリティ・ベストプラクティスに従い、特にあなたのプロジェクトと同じカテゴリーで、すべての既知のハッキングを研究してください。Solidityを使用している場合は、スマートコントラクト開発に関する公式の最新の変更とセキュリティに関する考慮事項を常に把握しておくこと。
可能な限り、検証済みのコントラクト・ライブラリ、テンプレート、関数を使用してください。Open Zeppelinはイーサリアムのローンチ以来、この分野のパイオニアであり、優れたセキュリティ監査サービスも提供しています。
高度なDeFi、ブリッジ、クロスチェーン、外部依存を持つシナリオとの統合には特に注意すること。思いつく限りのシナリオをカバーする手動テスト群を作成する。
スマートコントラクトのテスト・カバレッジを100%作成する。80%でも90%でもなく、100%です。これは、セキュリティ監査会社からの要求事項であることが多く、あなたの要求事項でもあるはずです。
主要な（理想的にはピア・レビューされた）コードのチェックインや変更のたびに、理想的には統合CD/CIプロセスで、コードのサニティ・チェックを実行すること。古いタイプの開発者から教訓を得て、簡単かつ頻繁に実行できるビルド検証テスト（BVT）を作成し、新しいコードにリグレッションが発生しないことを確認します。
利用可能な自動化ツールを早期に、そして頻繁に活用する。これらのツールの一部は、ConsenSys Diligenceの「Security Tooling Guide for Smart Contracts」に掲載されており、Web3全体で使用されている22のセキュリティ・ツールの詳細を見ることができます。
上級者向け：高度なツール（ファジング、形式的検証、不変性証明）を持ち、必要に応じてサイクルを通してチームをサポートできるセキュリティ会社と協力する。
スマートコントラクトのテストと検証の詳細
開発とテストは非常に密接な関係にあり、プロジェクトのライフサイクル全体の中で一つのサイクルを形成しています。 さらに、チーム内のテストがうまくいけばいくほど、プロの監査人は、基本的なテストの作成と実行よりも、より不明瞭で抽象的な攻撃ベクトルに焦点を当てることが容易になるのです。
手動か自動化か？
正解は「両方」です。以下は、イーサリアム財団の説明です。
自動化されたテストは効率的で、少ないリソースを使用し、手動分析よりも高いレベルのカバレッジを約束します。また、自動テストツールはテストデータを設定することができ、予測された動作と実際の結果を比較することができます。記号実行、SMT解決、入力ファジングなどの高度な解析技術により、何があってもコードが正しく動作するという高い信頼性を得ることができます。
スマートコントラクトの手動テストにはかなりのスキルと時間、お金、労力の投資が必要ですが、人間の知性によって、自動テストでは検出されないようなコントラクト・コードの欠陥が見つかることがよくあります。スマートコントラクトを手動でテストすることで、コードの外側に存在しながらも影響を及ぼす可能性のある脆弱性を発見することもできます。例えば、スマートコントラクトの監査では、上述のようにチェーン外のコンポーネントとの相互作用の欠陥に起因する脆弱性を発見することができます。
MythX
いくつかの企業が、無料または少額のサブスクリプションで使用できるプロフェッショナルなスマートコントラクト・テストツールを作成しています。ConsenSysは現在、Remix用のMythXプラグインを提供しており、サブスクリプションが必要ですが、Remix IDEと直接統合され、コードのどこでエラーが見つかったかを正確に表示します。
Firefly
Runtime VerificationのFireflyを使ったテスト・カバレッジ解析は、現在サブスクリプションを必要とせず、不足しているテストケースやシナリオを明らかにすることができます。
以下の「percentFeeGov == 0」のケースをカバーする既存のテストはありません：
また、以下の「block.timestamp >= expiration」のケースをカバーする既存のテストはありません：
FireFlyはまた、ジャンプ・オペコード（すべてのジャンプ・オペコードで分岐の両方が実行される）、無効なオペコード（コードベース内の無効なオペコードはテストによって到達しなかった）、および復帰オペコード（コードベース内のすべての復帰オペコードはいくつかのテストによって到達した）をチェックします。
Echidna
もう一つの強力なツールは、Trail of BitsのEchidnaです。Echidnaはスマートコントラクトのファザーで、悪意のあるカバレッジ・ガイドによるテストケース生成により、セキュリティ特性を迅速にテストすることができます。例えば、「The expireTsFrom function always returns the encoded expireTs value」というプロパティは、Echidnaのテストパスで検証することができます。
Trail of Bitsは、スマートコントラクトの監査やツールの元祖の1つで、スマートコントラクトを検証するためのシンボリック実行のパイオニアでした。しかし、前述したように、依頼するには長い待ち時間があります。
Foundry
Runtime Verificationは、需要があるもう一つの一流企業で、Foundry 2.0とKEVM（EVMの形式仕様に基づく構築による正しいEthereum Virtual Machine）との創造的で強力な統合を行いました。これらは、シンボリック・プロパティ・テストカバレッジを行うために一緒に使用することができ、カバレッジテストの100％が合格した場合、自動化された形式検証を達成するための方法です。
Foundryツールは、パラメータのランダム入力を生成し、その結果のテストを実行します。
K-Foundryは、K EVMのセマンティクスを使用して、パラメトリック・テストをシンボリックに実行します。
パラメトリック・テストは正式な仕様となり、K-Foundryはそれを正式に検証します。
監査＆承認
監査
コードが100％固まったら、Trail of Bits、BlocTrax、Quantstamp、ConsenSys Diligence、Runtime Verificationなどの信頼できる会社を使って、プロのセキュリティ監査を完全に行ってください。これは、新しいプロジェクトを立ち上げる際に最も重要な部分の1つであり、あなたのコードを保護するための最も重要なステップかもしれません。
こちらはAlchemyが発表した2023年のセキュリティ監査会社のリストです。また、過去の監査実績やREKTニュースを見て、監査対象プロジェクトがハッキングされたことがないかどうかを時間をかけて確認する必要があります。
セキュリティ監査ガイドライン
設計やモデリングの段階でプロジェクトが具体化し始めたら、すぐにセキュリティ監査会社の調査を開始しましょう。目標や予算に合致すると思われる会社に連絡を取り、その会社のカレンダーに載りましょう。特定の専門分野（例：侵入テスト vs スマートコントラクト検証）を持つ複数の会社に依頼することも検討してください。
監査会社が見積りを作成するために、仕様書、コード、テストケースへのアクセスを提供する準備をします。見積もりが提供されない場合は、初回ミーティングの直後に送信する2社間NDAの準備をしましょう。
コードを凍結し、テストネットにデプロイする。これは、私的および公的なバグ・バウンティにも有効です。
スマートコントラクト開発者と監査チームの間で、SlackやDiscordチャンネルなどのオープンなコミュニケーション・ラインを確保し、毎日チェックして質問に答えてください。Slackを通じて監査人と頻繁にQ&Aセッションを行い、問題が見つかれば修正しましょう。
デプロイする予定の新バージョンごとに再監査を行う。これをしないことが、2023年初頭の多くのプロジェクトの破滅につながりました。変更されデプロイされた一行のコードに、悪用された脆弱性が含まれていたのです（SafeMoonを参照）。 監査法人とリテイナー型の関係を構築し、ライブで展開するすべての新しい変更を監査法人にチェックしてもらうことを検討してください。
上級者向け：コードを仕様に照らして正式に検証する。
監査には何が必要なのでしょうか？
セキュリティ監査の実施には、アートとサイエンスが存在します。また、より完全なカバレッジを得るために使用できる手動および自動化されたプロセスも存在します。したがって、スマートコントラクト言語、プロトコルの種類、または使用しているVMについて経験があり、業界内で高い評価を得ているセキュリティ会社を選ぶことが非常に重要です。
セキュリティ・エンジニアはどのように監査に臨むのでしょうか？ 何が行われるのでしょうか？
Runtime VerificationによるBlockswap Stakehouse監査報告書より：
システムの意図する動作を捉える抽象的な高レベルモデルを作成し、このモデルに基づいてプロトコルの望ましい特性や不変性を特定しました。
プロトコルのビジネス・ロジックを手作業で厳密に推論し、セキュリティ上重要なプロパティを検証して、ビジネス・ロジックに抜け穴がないことを確認しました。
ロジックと実装の間に矛盾がないか、既知のセキュリティ問題や攻撃ベクトルに対する脆弱性がないか、コードをレビューしました。
最も致命的な結果についてチームと話し合い、コード内のその場所から逆算して、意図しない方法で到達できないことを確認しました。
開発チームとのミーティングに定期的に参加し、調査結果について話し合い、緩和策や合理的なトレードオフを一緒に考え ました。
また、以下のようなツールの利用が報告されたケースもありました：
EVMの癖やSolidityコンパイラのバグに起因するバイトコード・レベルでの予期せぬ悪用可能な動作を体系的に検索するために、コンパイルされたバイトコードの一部をシンボリックに実行しました。
バイトコード・レベルのテストカバレッジを測定するためにFirefly（上記参照）を採用し、不足しているテスト・シナリオを特定し、テストの品質を向上させました。"
推奨事項/軽減事項
最高の監査チームは、問題を発見した際に推奨事項を提示し、修正内容が適切に実施されているかどうかも検証します。例えば、次のようなことです：
問題点：以下のコードは、「decrease」が「remainingCollateral」より大きくなることがないようにするものです：
しかし、これは間違っています。例えば、「decrease = 1」で「remainingCollateral = 2」の場合、「decrease」は1のままであるべきなのに、2まで増加してしまいます。
推奨：上記のコードは以下のように修正することができます：
ステータス：PR #12で対処しました。
かなりクールでしょう？これは、稼働前にスマートコントラクトの問題を発見して修正する方法の素晴らしい例です。
監査の免責事項 ：セキュリティとリスクはプロジェクトが被るものですので、すべてのセキュリティ監査会社は、その報告書にいかなる種類の失われた資金に対しても、いかなる方法でも責任を負わないという、ある種の免責事項を記載することに注意してください。例えば、次のようなものです：「本報告書は、特定のプロジェクトやチームを支持または非難するものではなく、特定のプロジェクトの安全性を保証するものではありません。本レポートは、トークン、トークンセール、その他の製品、サービス、その他の資産の潜在的な経済性を考慮するものではなく、また考慮すると解釈されるべきでもありません。暗号化トークンは新興技術であり、高い技術的リスクと不確実性を伴います。本レポートは、コードのバグがないこと、ビジネスモデルやその所有者、そのようなビジネスの法的コンプライアンスを含め、いかなる点においても第三者に対していかなる保証や表明も提供しません」
モニター＆アラート
24時間365日のモニタリング
セキュリティは監査が終わっても終わりません。モニタリングはブロックチェーンのセキュリティに不可欠な要素であり、導入したプロジェクトが定義されたパラメータ内で運用されているかどうかをチェックするために、すべてのプロジェクトが備えておかなければなりません。これは、ハードウェアだけでなく、ソフトウェアやスマートコントラクトにも当てはまります。仕様策定段階と監査段階の両方で、スマートコントラクトのプロパティと不変条件（常に「true」でなければならない）が定義され、セキュリティ・モニタリングの中心となります。
メインネットで立ち上げるすべてのプロジェクトは、事前に定義された異常を検出し、問題があることを知らせるアラートを送信するために、ある程度のレベルの監視を行う必要があります。
トランザクションの監視は、ライブアクションが起きている場所にセキュリティをもたらします。
ダッシュボードを作成してプロパティを監視し、設定値から外れるたびにアラートを送信します（例：プールXの総流動性がY未満）。
異常な動作や特定の不変条件（例：ブリッジへの送信量＝ラップ化の生成量）のための追加モニターを作成します。
アラートの種類ごとにプロセスや特定のアクションを作成し、準備を整える！
上級者向け：プロのセキュリティ会社と連携して、監視ソリューションを作成し、ホストする。
プロパティのモニタリング：監視すべき特定のスマートコントラクトのプロパティと不変条件は、通常、仕様に定義され、監査中に再チェックされます。これらの不変条件は契約の有効期間中保持されるべきであり、リアルタイムで監視することができます。
一般的に、優れた監視システムは：
正確なリアルタイム・データと、十分に整備された過去のデータを使用して、メトリクスを通知する。
監査中または別の成果物として特定された不変条件およびその他のプロパティを監視する。
不変条件に違反したとき、またはプロパティが定義された閾値を超えたときに、アクションをトリガーする。
ユーザーへの注意喚起や復旧の開始を含む。
Forta NetworkとSpiceAIは、ブロックチェーン・プロジェクト向けに監視ソリューション、カスタムボット、各種アラートを提供する企業の例です。将来的には、より多くのセキュリティが、取引が行われているノードやウォレットに近づいていくことが予想されます。
ここでは、リアルタイムで監視できるもの、また監視すべきものの簡単な例をいくつか紹介します：
ブリッジ：最終トークンは預け入れトークンより大きいか等しいか？
DEX：X * Y = Zか？
流動性プール：トークンの1つがX%上昇または下降しているか？
ステーブルコイン：トークンの価値は希望のペグからX%以内か？
NFT：フロア価格のX%以上の上昇・下降があるか？
シグナル ー Coming Soon
セキュリティ・ミシュラン星
いくつかのスマートコントラクト監査会社は独自の評価システムを持っていますが、監査を認証し、異なるレベルの認証バッジを作成するための包括的な単一のシステムは、今日まで存在しませんでした。しかし、Enterprise Ethereum Allianceは、EEA EthTrust Security Levels Specification v1を公開しましたので、イーサリアム・エコシステム内での統一的なアプローチにつながるはずです。面白い事実：私はこの仕様を作成したETHTrustグループの創設者であり、私の会社5thnode LTDは、いくつかのブロックチェーンでこのようなシステムに取り組んでいます。
私について：私は、イーサリアム以前からのクリプト愛好家であり、現在、開発者とエンドユーザー向けの新しいセキュリティ製品スイートのステルス開発に注力している投資家です。5thnode LTDのCEOであり、Algorand ALDragon、Nahmii、etc の戦略的アドバイザーです。以前は、Runtime Verificationの最高戦略責任者、ConsenSys DiligenceとMythXの共同設立者。20年来のマイクロソフトのベテラン研究者,Windowsセキュリティ製品オーナー、WWデベロッパー・エコシステム・ディレクター。 現在、長野県長野市とワシントン州カークランド市に在住。
元記事：https://tomlindeman.substack.com/p/secure-sdlc-2023?sd=pf