Symbolic Execution 找到了我 94% 測試覆蓋率都漏掉的整數溢位

你的測試套件有 94% 覆蓋率且零失敗。Symbolic execution engine 在三秒內就在你的程式碼中找到了一個 crash。

測試沒壞。覆蓋率指標沒有說謊。問題在於測試只驗證特定點上的行為。Symbolic execution 驗證的是整個輸入空間區域中的行為。如果 bug 存在於兩個測試案例之間的縫隙，你寫再多範例也沒用。

Symbolic Execution 到底在做什麼

Symbolic execution 是一種程式分析技術，它用 symbolic variables 而非具體數值來執行你的程式碼。一般的測試把 x = 5 傳進函式。Symbolic execution engine 傳的是 x = α，其中 α 代表每一個可能的整數。

當程式碼執行時，engine 會追蹤 constraints。當它遇到像 if (x > 0) 這樣的分支時，它不會選擇方向。它會分叉執行。一條路徑帶著 constraint α > 0，另一條帶著 α ≤ 0。兩條路徑獨立繼續。

當某條路徑抵達 assertion、記憶體存取或潛在的 crash site 時，engine 會向 SMT solver 提出一個簡單的問題：「是否存在某個 α 的值，能滿足這條路徑上的所有 constraints，同時又違反這個安全性質？」如果 solver 回答有，它就會回傳一個具體的 counterexample。你現在就有了一個特定的輸入，能觸發一個你從未寫過測試的 bug。

你的單元測試抓不到的 Bug

考慮一個在複製前驗證陣列邊界的函式：

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 不需要你猜壞輸入。它會探索發生繞回的那條路徑，並要求 solver 找出滿足 constraint end ≤ src_len 且 offset + count 溢位的數值。Solver 在毫秒內就回傳了 counterexample。

Engine 如何探索路徑

核心機制是 constraint collection 和 path forking。程式碼中的每個條件敘述都變成一個分支點。Engine 維護一個 path constraint，這是一個布林公式，代表執行要抵達目前位置必須為真的所有條件。

在每個分支點，engine 會查詢 solver：

目前的 path constraint 加上 true-branch condition 是否可滿足？
目前的 path constraint 加上 false-branch condition 是否可滿足？

如果兩者都可滿足，engine 就會分叉。它把兩條路徑都加入queue等待探索。Symbolic execution 就是這樣為有界程式達成窮舉路徑覆蓋的。

當某條路徑抵達 crash、越界存取或失敗的 assertion 時，engine 會要求 solver 在目前的 path constraint 下，為 symbolic inputs 找出一個滿足的賦值。那個賦值就是觸發 bug 的輸入。

你可以直接用 Z3 看到 constraint-solving 的步驟。Z3 是驅動許多 symbolic execution engine 的 SMT solver：

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

solver = Solver()

# Model 32-bit unsigned size_t values
offset = BitVec('offset', 32)
count = BitVec('count', 32)
src_len = BitVec('src_len', 32)

# Path constraints: offset <= src_len, count <= 1024
solver.add(ULE(offset, src_len))
solver.add(ULE(count, 1024))

# We want to find a case where offset + count wraps around
# and the end check passes incorrectly
end = offset + count
solver.add(UGT(end, src_len))  # This should trigger the return -1

# But what if we look for the overflow case where end wraps?
solver2 = Solver()
solver2.add(ULE(offset, src_len))
solver2.add(ULE(count, 1024))
solver2.add(ULT(offset + count, offset))  # unsigned overflow
solver2.add(ULE(offset + count, src_len))  # bogus check passes

if solver2.check() == solver2.sat:
    model = solver2.model()
    print(f"offset={model[offset]}, count={model[count]}")
    # offset=4294967295, count=1 on a 32-bit model

Solver 回傳滿足溢位 constraint 的具體數值。這就是 symbolic execution 的數學核心。Engine 會自動對你程式中的每個分支執行這個過程。

讓它無法取代你測試套件的權衡

Symbolic execution 不是免費的。有三項成本限制了它的實用範圍。

路徑爆炸。 每個 if 敘述都讓路徑數量翻倍。一個有 20 個獨立分支的函式就有超過一百萬條路徑。大多數 engine 在逾時或路徑預算用盡後就會放棄。迴圈會讓情況更糟。一個在無界範圍上進行 symbolic iteration 的迴圈會產生無限多條路徑。Engine 通常會把迴圈展開固定次數後就繼續前進。

外部狀態和系統呼叫。 Symbolic execution 在 pure functions 上效果最好。當你的程式碼從檔案讀取、發出網路請求或查詢資料庫時，engine 根本不知道會回傳什麼值。有些工具會用啟發式方法模擬常見的函式庫呼叫。其他的則需要你撰寫 mock model。這很繁瑣且容易出錯。

Solver 逾時。 真實程式碼的 constraint formula 很複雜。陣列、bitvectors、浮點運算和非線性數學都可能讓 SMT solver 陷入指數時間。一條以具體執行只需微秒的路徑，以 symbolic 方式求解可能需要數分鐘。Engine 會捨棄這些路徑並將它們回報為未解決。

由於這些限制，symbolic execution 是測試的補充，而非替代品。它找到深層的邊界案例。你的測試驗證常見案例和整合行為。

在三種真實程式碼上嘗試的方法

執行 symbolic execution 不需要博士學位。現代工具隱藏了大部分複雜度。

C/C++ 用 KLEE。 KLEE 是經典的開源 symbolic execution engine，建構在 LLVM 之上。你用 clang -emit-llvm 把程式碼編譯成 LLVM bitcode，然後對結果執行 klee。KLEE 曾在 GNU coreutils、SQLite 和其他廣泛使用的 C codebase 中找到嚴重的 bug。

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

KLEE 會為找到的每個 bug 輸出 .ktest 檔案。你可以用一個小型執行時期來重播它們，查看確切的輸入。

Python 和二進位檔用 angr。 angr 是一個用於 symbolic execution、binary analysis 和 reverse engineering 的 Python 框架。它運作在已編譯的二進位檔上，所以不需要原始碼。你寫一個 Python script 來設置 symbolic registers 和記憶體，然後讓 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 慢，但能處理真實世界的二進位檔，包括它們雜亂的 calling conventions 和函式庫相依性。

Rust 用 Kani。 Kani 是建構在 CBMC 之上的 Rust 專屬驗證器。你用 #[kani::proof] 標註函式並執行 cargo kani。它在底層使用 symbolic execution 來檢查算術溢位、越界存取和 assertion failure。

#[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);
}

如果你已經在 Rust 生態系中，Kani 是最簡單的入門選項。它與 cargo 整合，並以你熟悉的格式提供錯誤追蹤。

常見問題

Symbolic execution 會取代 fuzzing 嗎？

不會。Fuzzing 產生隨機輸入並觀察 crash。Symbolic execution 對路徑進行推理，找出滿足特定 constraints 的輸入。Fuzzing 能擴展到大型程式和長時間執行。Symbolic execution 在較小的區域中找到更深的 bug。這兩種技術相輔相成。像 Driller 和 QSYM 這樣的工具結合了兩者：用 fuzzing 來達成覆蓋率，用 symbolic execution 來處理難以觸及的分支。

Symbolic execution 能證明我的程式碼沒有 bug 嗎？

只有對於沒有無界迴圈和沒有外部相依性的有界程式才可以。對於大多數生產程式碼，symbolic execution 可以在路徑深度限制內證明某些 bug 類別不存在。它無法證明完全正確性。

執行需要多久？

小型函式需要數分鐘到數小時。Symbolic execution 不是 CI 的速度王者。把它用在關鍵的安全函式、parser和邊界檢查程式碼上。不要試著對整個 web framework 執行 symbolic execution。

從一個函式開始

你不需要對整個 codebase 執行 symbolic execution。挑一個如果出 bug 會很痛的函式。一個parser。一個授權檢查。一個buffer 複製。

寫一個 KLEE harness、一個 angr script，或一個 Kani proof。執行它。看著它找到一個你永遠不會寫測試的輸入。修掉 bug。睡得更安穩。

目標不是取代你的測試。目標是停止假裝 94% 覆蓋率就代表 94% 的安全性。Symbolic execution 找到縫隙。你的測試永遠做不到。