有界網羅的ランダムプログラム生成 ~Solidityコンパイラテストの新手法~
この記事は以下の論文をもとに書かれています。
TL;DR
コンパイラのバグを効率的に発見するための新しい手法「有界網羅的ランダムプログラム生成」について解説します。この手法は、ランダムプログラム生成の柔軟性とテンプレートベースの手法の焦点を組み合わせ、特にSolidityコンパイラとアナライザのテストに効果的です。ERWINというツールとして実装され、既存のテスト手法では見つけられなかった23個の新しいバグを発見することに成功しています。
はじめに
コンパイラのバグは、特にブロックチェーン分野において壊滅的な結果をもたらすことがあります。2023年7月30日、分散型取引所（DEX）のCurve Financeがハッキング被害を受け、約4700万ドル（約60億円）相当の暗号資産が流出しました。この攻撃の原因は、Curveの主要システムで使用されていたプログラミング言語Vyperのコンパイラに存在したバグによるものでした。
Vyperは、Ethereumのスマートコントラクト開発に用いられるPython風のプログラミング言語で、Solidityの代替として開発されました。攻撃者は、Vyperのバージョン0.2.15、0.2.16、0.3.0に存在したリエントランシー（再入可能性）の脆弱性を悪用しました。この脆弱性により、攻撃者はプールコントラクトの初期化関数を再度呼び出し、自身のアドレスをプールの所有者として設定することが可能となりました。その結果、攻撃者はプール内の資金を自由に引き出すことができました。
この事件は、DeFiエコシステム全体に影響を及ぼし、CurveのユーティリティトークンであるCRVの価格も下落しました。一度デプロイされたスマートコントラクトは変更が難しく、コンパイラのバグがこのような経済的損失に直結するという現実を突きつけられたわけです。
今回は、そんなコンパイラのバグを効率的に発見するための新しい手法「有界網羅的ランダムプログラム生成（Bounded Exhaustive Random Program Generation）」について紹介します。この手法は特にSolidityコンパイラのテストに焦点を当てていますが、考え方自体は他の言語にも応用できる汎用的なものです。
コンパイラテストの課題：機会主義
従来のランダムプログラム生成によるコンパイラテストには「機会主義（opportunism）」という問題があります。これは、プログラミング言語が定義する広大な探索空間の中で、特定の焦点を持たずにプログラムを生成してしまうという問題です。
例えば、こんな感じです：
ランダムプログラム生成器「よーし、次はどんなプログラムを生成しようかな？関数を作ろうか、変数宣言にしようか、それともループにしようか...とりあえず何か作ってみよう！」
この機会主義的なアプローチでは、コンパイラのバグを引き起こす特定のパターンを持つプログラムを生成する確率が低くなります。バグを引き起こすプログラムが、以前に生成された（バグを引き起こさない）プログラムの「近く」に存在する場合でも、ランダム性によってそれを見つけるのが難しくなるんですね。
有界網羅的ランダムプログラム生成とは？
この問題を解決するために提案されたのが「有界網羅的ランダムプログラム生成」です。この手法は、ランダムプログラム生成の柔軟性とテンプレートベースの手法の焦点を組み合わせたものです。
具体的には、以下の2段階のプロセスで構成されています：
- ランダムプログラムテンプレートの生成: バグ関連のプレースホルダーを含む不完全なテストプログラムを生成します
- 有界網羅的列挙の実施: テンプレート内の各プレースホルダーに対して、有効な値の境界付き網羅的列挙を行います
これを図で表すとこんな感じです：
1. テンプレート生成:
function foo(TYPE param) VISIBILITY {
return EXPRESSION;
}
2. 網羅的列挙:
- TYPE = {uint, int, bool, ...}
- VISIBILITY = {public, private, internal, external}
- EXPRESSION = {param, param + 1, ...}
このアプローチの優れている点は、テンプレート生成フェーズで可解な制約セットを維持し、網羅的列挙フェーズでこれらの制約内でプレースホルダーのすべての可能な値を系統的に探索できることです。これにより、バグを引き起こす可能性の高いプログラムを効率的に生成できるようになります。
ERWIN: Solidityのための実装
この手法は、Ethereumブロックチェーン用のスマートコントラクト言語であるSolidityのために、ERWINというツールとして実装されました。Solidityを選んだ理由は、ブロックチェーンエコシステムで最も広く使用されている言語の一つであり、スマートコントラクトの不変性と経済的利害を考えると、コンパイラのバグが深刻な結果をもたらす可能性があるからです。
ERWINの実装は、TypeScriptで約15,000行のコードから成り、以下のような特徴があります：
- 中間表現（IR）プログラムを生成し、それをテストプログラムに変換
- 属性変数（データ型、ストレージの場所、可視性、可変性など）と制約を管理
- 階層的な生成アプローチ（コントラクト宣言→メンバ変数・関数→式→ステートメント）
ERWINの動作フローを簡単に説明すると：
- コンテキスト初期化：スコープや宣言情報を格納
- 式生成と制約構築：トップダウン方式で式を生成し、制約を収集
- テストプログラムへの変換：属性変数に適切な値を割り当て
評価結果：驚異的なバグ発見能力
ERWINの評価結果は非常に印象的です。6ヶ月間の断続的な運用後、ERWINは以下のような成果を上げました：
- solc、solang、slitherで合計26個のバグを特定
- そのうち16個は開発者によってバグとして確認され、9個はすでに修正済み
- 最先端のSolidityファザー（ACFとFuzzol）と比較して、ERWINは合計15個のバグを検出し、そのうち13個は他のツールでは検出されなかった
特に興味深いのは、ERWINがsolcのユニットテストではカバーされていない4,582のエッジと14,737のラインをカバーできたことです。これは、開発者が書いたテストスイートを補完する形で、ERWINが効果的に機能していることを示しています。
検出されたバグの種類も多様で、セグメンテーション違反、不正な出力、ハング、内部コンパイラエラー（ICE）など、さまざまな症状を持つバグが見つかりました。
実践的な意義：より安全なスマートコントラクト開発へ
この研究の実践的な意義は大きいと思います。冒頭で触れたCurve Financeのハッキング事件のように、コンパイラのバグは実際に巨額の経済的損失をもたらす可能性があります。ERWINのようなツールによってSolidityコンパイラのバグを事前に発見できれば、より安全なスマートコントラクト開発が可能になります。
また、ERWINの生成したテストプログラムは、変異ベースのファザーのシードプールを強化するためにも利用できます。これにより、さらに多くのバグを発見できる可能性があります。
個人的には、この手法が他のプログラミング言語やコンパイラにも適用されることを期待しています。特に型システムが複雑な言語（例えばRustやHaskellなど）では、この手法が効果的に機能する可能性があると思います。
まとめ
有界網羅的ランダムプログラム生成は、コンパイラテストにおける機会主義の問題を解決する新しいアプローチです。ERWINというツールとしてSolidityに実装され、既存のテスト手法では見つけられなかった多くのバグを発見することに成功しています。
この手法の強みは、ランダム性と体系的な探索を組み合わせることで、効率的にバグを発見できる点にあります。今後は、Solidityの追加機能（インラインアセンブリ、インターフェース、ライブラリなど）をサポートすることで、さらに多様なプログラムを生成し、より多くのバグを発見することが期待されています。
コンパイラのバグは見つけるのが難しく、発見されないまま本番環境で問題を引き起こすことがあります。ERWINのようなツールが普及することで、より信頼性の高いコンパイラが実現し、結果としてより安全なソフトウェア開発が可能になるのではないでしょうか。
以上。
Discussion