テストスイートのカバレッジは94%で、失敗はゼロだ。symbolic executionエンジンは3秒未満でコードのクラッシュを発見する。

テストは壊れていない。カバレッジメトリックが嘘をついているわけでもない。問題は、テストが特定の地点での振る舞いを検証するのに対し、symbolic executionは入力空間の領域全体にわたって振る舞いを検証するということだ。バグが2つのテストケースの間の隙間に潜んでいるなら、どれだけ例を書いても関係ない。

Symbolic Execution が実際に何をするのか

symbolic executionは、コードを具体的な値ではなくsymbolic変数で実行するプログラム解析手法だ。通常のテストは x = 5 を関数に渡す。symbolic executionエンジンは x = α を渡す。ここで α はあらゆる可能な整数を表す。

コードが実行されると、エンジンは制約を追跡する。if (x > 0) のような分岐に到達したとき、エンジンは方向を選ばない。実行を分岐させる。一方のパスは制約 α > 0 を持ち、もう一方は α ≤ 0 を持つ。両方のパスが独立に続行する。

パスがアサーション、メモリアクセス、または潜在的なクラッシュ地点に到達すると、エンジンはSMTソルバーに単純な質問をする。「このパス上のすべての制約を満たし、この安全性プロパティに違反するような α の値は存在するか？」ソルバーがイエスと答えれば、具体的な反例を返す。これで、テストを書いたことのないバグを引き起こす特定の入力が手に入る。

ユニットテストでは捉えられないバグ

配列の境界を検証してからコピーする関数を考えてみよう。

int copy_slice(const char *src, size_t src_len,
               size_t offset, size_t count) {
    if (offset > src_len) return -1;
    if (count > 1024) return -1;

    size_t end = offset + count;
    if (end > src_len) return -1;

    char dst[1024];
    memcpy(dst, src + offset, count);
    return 0;
}

テストスイートは妥当に見える。

void test_copy_slice_normal() {
    assert(copy_slice("hello", 5, 1, 3) == 0);
}

void test_copy_slice_too_long() {
    assert(copy_slice("hi", 2, 0, 1025) == -1);
}

void test_copy_slice_bad_offset() {
    assert(copy_slice("hi", 2, 5, 1) == -1);
}

すべてグリーンだ。しかし offset と count は size_t、符号なし整数だ。64ビットシステムでは、offset + count は両方が大きい場合に小さな数にラップアラウンドする可能性がある。offset = 0xFFFFFFFFFFFFFFFF で count = 1 の場合、end = 0 となり、src_len より大きくはない。境界チェックを通過する。memcpy は無効なアドレスから読み込む。

合理的な開発者が offset = 2^64 - 1 のテストケースを書くことはない。入力空間は計り知れないほど広い。symbolic executionは悪い入力を推測する必要がない。ラップアラウンドが起こるパスを探索し、ソルバーに対して制約 end ≤ src_len を満たしつつ offset + count がオーバーフローする値を見つけるよう依頼する。ソルバーはミリ秒単位で反例を返す。

エンジンがパスを探索する仕組み

核心メカニズムは制約の収集とパスの分岐だ。コード内のすべての条件文が分岐点になる。エンジンはパス制約を維持する。これは、実行が現在の地点に到達するために真でなければならないすべての条件を表す論理式だ。

各分岐で、エンジンはソルバーにクエリする。

  1. 現在のパス制約にtrue分岐の条件を加えたものは充足可能か？
  2. 現在のパス制約にfalse分岐の条件を加えたものは充足可能か？

両方が充足可能な場合、エンジンは分岐する。両方のパスを探索キューに入れる。これが、symbolic executionが制限付きプログラムに対して網羅的なパスカバレッジを達成する仕組みだ。

パスがクラッシュ、境界外アクセス、または失敗したアサーションに到達すると、エンジンはソルバーに、現在のパス制約の下でsymbolic入力に対する充足する割り当てを求める。その割り当てがバグを引き起こす入力だ。

制約解決ステップは、多くのsymbolic executionエンジンの原動力であるZ3 SMTソルバーを使って直接確認できる。

from z3 import Solver, BitVec, UGT, ULT, ULE, simplify

solver = Solver()

# 32ビット符号なしsize_t値をモデル化
offset = BitVec('offset', 32)
count = BitVec('count', 32)
src_len = BitVec('src_len', 32)

# パス制約: offset <= src_len, count <= 1024
solver.add(ULE(offset, src_len))
solver.add(ULE(count, 1024))

# endがラップアラウンドし、境界チェックが誤って通過するケースを探す
solver2 = Solver()
solver2.add(ULE(offset, src_len))
solver2.add(ULE(count, 1024))
solver2.add(ULT(offset + count, offset))  # 符号なしオーバーフロー
solver2.add(ULE(offset + count, src_len))  # 誤ったチェックが通過

if solver2.check() == solver2.sat:
    model = solver2.model()
    print(f"offset={model[offset]}, count={model[count]}")
    # 32ビットモデルでは offset=4294967295, count=1

ソルバーはオーバーフロー制約を満たす具体的な値を返す。これがsymbolic executionの数学的な核心だ。エンジンはプログラム内のすべての分岐を自動的にこの処理を行う。

テストスイートを置き換えられないトレードオフ

symbolic executionはタダではない。実用的な範囲を制限する3つのコストがある。

パス爆発。 if 文ごとにパスの数が2倍になる。20個の独立した分岐を持つ関数は、100万を超えるパスを持つ。ほとんどのエンジンはタイムアウトまたはパス予算の後に諦める。ループは状況を悪化させる。境界が定まらない範囲をsymbolicに反復するループは、無限に多くのパスを作る。エンジンは通常、ループを固定回数だけアンロールして次に進む。

外部状態とシステムコール。 symbolic executionは純粋関数で最も機能する。コードがファイルを読み込んだり、ネットワークリクエストを行ったり、データベースにクエリしたりすると、エンジンはどのような値が返されるかわからない。いくつかのツールは一般的なライブラリ呼び出しを発見的にモデル化する。他はモックモデルを書くことを要求する。これは面倒でエラーが起きやすい。

ソルバータイムアウト。 実際のコードの制約式は複雑だ。配列、ビットベクトル、浮動小数点演算、非線形数学は、SMTソルバーを指数時間に押し込むことができる。具体的に実行するとマイクロ秒で終わるパスが、symbolicに解くと数分かかることもある。エンジンはこれらのパスを破棄し、未解決として報告する。

これらの制限のため、symbolic executionはテストの代替ではなく補完だ。深いコーナーケースを見つける。テストは一般的なケースと統合の振る舞いを検証する。

実際のコードで試す3つの方法

symbolic executionを実行するのにPhDは必要ない。現代のツールはほとんどの複雑性を隠蔽する。

C/C++向け: KLEE。 KLEEはLLVM上に構築された古典的なオープンソースsymbolic executionエンジンだ。clang -emit-llvm でコードをLLVMビットコードにコンパイルし、その結果に klee を実行する。KLEEはGNU coreutils、SQLite、その他広く使われているCのcodebaseで重大なバグを発見してきた。

clang -emit-llvm -c -g copy_slice.c -o copy_slice.bc
klee --max-time=60 copy_slice.bc

KLEEは発見した各バグに対して .ktest ファイルを出力する。小さなランタイムで再生すれば、正確な入力を確認できる。

Pythonとバイナリ向け: angr。 angrは、symbolic execution、バイナリ解析、リバースエンジニアリングのためのPythonフレームワークだ。コンパイル済みバイナリで動作するため、ソースコードは不要だ。Pythonスクリプトを書いてsymbolicレジスタとメモリを設定し、angrに探索させる。

import angr

proj = angr.Project("./copy_slice")
state = proj.factory.entry_state()
sm = proj.factory.simulation_manager(state)
sm.explore(find=lambda s: b"crash" in s.posix.dumps(1))

angrはKLEEより遅いが、乱雑な呼び出し規約とライブラリ依存関係を持つ実世界のバイナリを扱える。

Rust向け: Kani。 KaniはCBMC上に構築されたRust特有の検証ツールだ。関数に #[kani::proof] をアノテートし、cargo kani を実行する。内部でsymbolic executionを使って、算術オーバーフロー、境界外アクセス、アサーション失敗をチェックする。

#[kani::proof]
fn check_copy_slice() {
    let src = kani::any_slice::<u8, 1024>();
    let offset: usize = kani::any();
    let count: usize = kani::any();
    kani::assume(count <= 1024);
    let _ = copy_slice(src, src.len(), offset, count);
}

Kaniは、すでにRustのエコシステムにいる場合、最も簡単な入り口だ。cargo と統合され、慣れ親しんだ形式のエラートレースを提供する。

よくある質問

symbolic execution は fuzzing を置き換えますか？

いいえ。fuzzingはランダムな入力を生成し、クラッシュを観察する。symbolic executionはパスについて推論し、特定の制約を満たす入力を見つける。fuzzingは大規模なプログラムや長時間の実行にスケールする。symbolic executionは、より小さな領域でより深いバグを見つける。両者はうまく連携する。DrillerやQSYMのようなツールは両方を組み合わせ、カバレッジにはfuzzingを、到達が難しい分岐にはsymbolic executionを使う。

symbolic execution はコードにバグがないことを証明できますか？

制限付きのプログラム、つまり境界のないループもなく外部依存関係もない場合にのみ可能だ。ほとんどの本番コードに対して、symbolic executionはパス深度の制限まで、特定のバグクラスが存在しないことを証明できる。全体の正しさを証明することはできない。

実行にはどれくらい時間がかかりますか？

小さな関数で数分から数時間。symbolic executionはCIのスピードデーモンではない。重要なセキュリティ関数、パーサー、境界チェックコードで実行する。Webフレームワーク全体をsymbolic executionしようとしない。

1つの関数から始めよう

codebase全体をsymbolic executionする必要はない。バグが発生すると痛い1つの関数を選ぶ。パーサー。認可チェック。バッファコピー。

KLEEのハーネス、angrスクリプト、またはKaniの証明を書く。実行する。自分がテストを書かなかった入力を見つけるのを見る。バグを修正する。より安心して眠る。

目標はテストを置き換えることではない。テストカバレッジ94%が安全性94%を意味するふりをやめることだ。symbolic executionが隙間を見つける。テストでは決して見つけられない。