スマートコントラクトの脆弱性対策に向けた形式検証手法の新たなアプローチ

目次

• はじめに
• 脆弱性防止のための別の手法
• 仕様駆動型アプローチ
• 結論

はじめに

スマートコントラクトおよびその周辺のブロックチェーンインフラにおける脆弱性問題に対して、形式的アルゴリズム検証手法を用いる試みは、ここ数年にわたって行われてきた。この分野で初期の研究の一つである Bhargavan et al. (2016): “Formal Verification of Smart Contracts: Short Paper.” PLAS 2016¹ では、Solidityで記述された契約のソースコードと、そこからコンパイルされたEVMバイトコードの双方を、F*言語の部分集合へ並行して翻訳し、その意味論的同値性を形式的に証明することを試みた。

理論上、これにより、意図しないコンパイルエラーと、ブロックチェーン上での契約展開時におけるEVMバイトコードの悪意ある差し替えの両方が排除されるはずである。その後、Mavridou & Laszka (2018): “Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach (FSolidM).” Financial Cryptography (FC) 2018² では、スマートコントラクトの設計に対する別のアプローチが提案された。これは、有限オートマトンという形式によって計算モデルを制約するもので、その概念的な単純さは多くのセキュリティ上重要な特性の「ワンクリック」検証に適している。

また、Tsankov et al. (2018): “Securify: Practical Security Analysis of Smart Contracts.” ACM CCS 2018³ による、より古典的な解決策も存在し、静的解析ツールによって、セキュリティ上の問題に関連する典型的なアルゴリズムパターンの自動検出が実証されている。さらに、“ZEUS: Analyzing Safety of Smart Contracts.” NDSS 2018⁴ では、特別にコンパイルされたLLVM版のSolidityソースのシンボリック解釈を通じて、典型的な脆弱性パターンが認識される手法が提案されている。

そして、Sergey et al. (2019): “Scilla: a Smart Contract Intermediate-Level Language.” ACM PLDI 2019⁵ による解決策も忘れてはならない。これは、ブロックチェーンインフラに対して、インタラクティブ定理証明で使用される論理形式化ツールに親和性の高い、契約の中間表現のためのドメイン固有言語を組み込むものである。本分野における最新の技術水準は、Tolmach et al. (2021): “A Survey of Smart Contract Formal Specification and Verification.” arXiv e-print 2008.02712⁶ などのメタサーベイによりより詳細に評価されているが、残念ながら、産業界で実際に応用されることは稀な多様な方法論が存在する現状を示している。

脆弱性防止のための別の手法

本研究では、スマートコントラクトの脆弱性対策という問題に対し、従来の枠組みを超えて、Leslie Lamport がかつて指摘した、複雑なソフトウェアシステムに必然的に存在する膨大なエラーという課題に一般化した視点を提供することを目指す。厳密な設計という彼の哲学に基づき、私たちは、従来のソフトウェア開発手法（従来のソフトウェアとスマートコントラクトが現在この手法に基づいて作成される）の最も潜在的に危険な重大エラーの根本原因は、実装すべきアルゴリズムに対する形式仕様のフェーズが欠如している点にあると主張する。この形式仕様のフェーズは、実際の実装に先立つべきものである。

従来の手法では、仕様が開発者の意図を非形式的に文書化することで代用され、せいぜい主要な使用パターンを示すテストスイートが付随するに留まっている。しかし、我々は、ゼロデイ脆弱性（特に暗号金融の文脈においては極めて危険なもの）との戦いは、周囲の実行環境における影響を正確に反映した形式仕様によるカバーがなされる前に、一行目のコードが記述された瞬間に実質的に敗北すると考える。この視点は、上述の方法論的前提に基づき、以下の点を浮き彫りにする。

1. コンパイラの形式検証や、ソースコードと実行可能バイナリ間の意味論的同値性検証に関する研究が極めて重要であるにもかかわらず、その実際の影響は限定的であり、プログラムのソースコード段階で既に生じる多くの脆弱性を網羅できていない。
2. プログラマのツールキットを大幅に狭めるようなソフトウェア信頼性向上の解決策は、普遍的なものとは言えない。すべての金融取引ロジックが有限オートマトンで容易に表現できるわけではなく、その適用範囲を超えた場合、問題の深刻さは依然として残る。
3. 典型的な脆弱性を対象とした静的コード解析ツールは実用的には有用であるが、既に記述されたコードにのみ適用可能であるため、完全な形式仕様を代替することはできない。さらに、それらは既知のパターンに還元されない新たな論理エラーの防止にも寄与しない。
4. 現在のソフトウェア開発業界の状況を鑑みると、コードの形式仕様化のために高い敷居を要求するツール（例：Rocq（Coq）、Lean、Agda など）を用いるパラダイムが広く採用されるとは想像し難い。形式的なプログラム特性の記述が、数学的論理の専門知識を要求しなくなるまでは、適切な形式仕様を伴って開発を開始できるのはごく一部の者に限られるだろう。

仕様駆動型アプローチ

以上を踏まえると、仕様駆動型開発パラダイムへの移行は、アルゴリズムの特性を記述するための手法の抜本的な見直しを必要とする。このような変革の結果として、一般的なプログラマのツールキットは、以下の要件を満たすように適応されなければならない。

1. 開発者は、自ら実装するアルゴリズムに対して、任意の論理的特性を記述可能な十分な表現力を持つ形式で仕様を定式化できなければならない。
2. 仕様記述の手段は直感的かつ利用しやすいものであり、参入障壁を最小限に抑えることで、開発者間での広範な採用を促進する必要がある。
3. 開発プロセス中に、コードがその形式仕様に準拠しているかを自動的に検証する仕組みを構築し、不一致を早期に検出・修正できる体制が求められる。さらに、ツールチェーンは一般的な開発環境やバージョン管理システムとシームレスに統合され、仕様および検証のプロセスが従来のワークフローを妨げないようにする必要がある。
4. また、このアプローチは後方互換性を保持し、従来の開発手法から仕様駆動型パラダイムへの段階的な移行を可能にすることで、既存プロジェクトへの形式手法の導入を円滑にするものでなければならない。

結論

結論として、これらの課題に取り組むことは、暗号金融製品のセキュリティおよび信頼性の向上のみならず、ソフトウェア開発における新たな標準の確立にも寄与する。形式検証を開発ライフサイクルの根幹に据えることで、ゼロデイ脆弱性に伴うリスクを効果的に軽減し、より堅牢で安全、かつ信頼性の高いソフトウェアエコシステムの実現が期待できる。

この種の実質的な技術革新の展望には、依然として明確なユートピア的色彩が否定できないものの、我々は、比較的少ない労力であっても、仕様駆動型開発の輝かしい未来が実現可能であることを示す研究の方向性を提案する。もし我々の仮説が正しければ、新たな方法論の基盤は以下の公理に置かれることになる。

任意のチューリング完全なプログラミング言語において、プログラムは基本的に、数少ない追加の非決定的意味論を伴う構成要素を補完することで、同一の言語内で仕様化できる。

プログラムが記述されるのと同じ言語の特殊な非決定的拡張を用いて、そのプログラム自体の仕様を定式化することは、これらの考えが広く受け入れられるための決定的な突破口となり得る。もし、任意の命令型プログラミング言語に対し、新たな構成要素を拡張してアルゴリズムの任意の論理的特性を定式化するための十分に一般的な原則が確立できるならば、コードの仕様化は、一部の学識ある研究者の秘儀的な芸術に留まらず、かつて数学のアンダーグラウンドから登場したサブストラクチャル型システムのように、プログラマの通常の技量の一部となるであろう。

これらの新たなアイデアの初期の実証実験として、形式化された意味論、暗号金融業界における広範な採用、そしてインタラクティブ定理証明器 Rocq⁷（WasmCert-Coq⁸）による成熟した機械化を兼ね備えた WebAssembly 計算モデル⁹の利用を提案する。

このブログ記事の議論に参加してください: