A Unifying View on SMT-Based Software Verification — 投影片

原文：JAR 2018 · doi:10.1007/s10817-017-9432-6 · 開啟原文 PDF ↗

0 你需要先會的東西

0.1 一個關於數字的尷尬問題

假設論文 A 說他們的方法在 benchmark 上贏過方法 B 三倍。你該信嗎？

這篇論文有一半的價值在這裡：把四個演算法放進同一份實作、用同一個 solver 跑，這時候的比較才有意義。

這也是為什麼「統一框架」不只是理論上漂亮——它是做出可信實驗的前提。

0.2 先回顧：SSA 與 path formula

SV 1 教過的東西這裡整篇都在用。快速複習：

一條執行路徑翻成公式時，每個變數的每個版本要有自己的名字：

i = 0;
i = i + 1;

0.3 BMC：把迴圈攤平

Bounded model checking 的想法非常直接：迴圈就展開它。

i = 0;
while (i < 3) { i = i + 1; }
assert(i == 3);

展開兩圈的路徑翻成公式：

沒有迴圈了，就是一條長長的公式，丟給 SMT solver。

• 有解 → 這條路走得通，如果它通往 ERROR 就是真的 bug
• 無解 → $k$ 步之內沒有 bug

注意 BMC 的先天限制：它只能說「$k$ 步之內沒事」，不能說「永遠沒事」。要證明程式完全正確，BMC 不夠。

0.4 k-induction：把歸納法用在程式上

你在大一數學學過歸納法：證 $P(0)$，再證 $P(n) \Rightarrow P(n+1)$，就得到所有 $n$ 都成立。

套到程式上：

1. base case：初始狀態是安全的
2. inductive step：安全的狀態走一步之後還是安全的

如果兩者都成立，程式就永遠安全——而且不需要展開迴圈。

k-induction 的解法是把假設加強：不只假設「上一步安全」，而是假設「連續 $k$ 步都安全」，再證第 $k+1$ 步安全。假設越強，能證的東西越多。

0.5 ARG：記住誰是誰的後繼

ARG（abstract reachability graph）就是把探索過程記下來的圖：節點是 abstract state，邊表示「這個是那個的後繼」。

為什麼需要它？ 因為找到誤報時，你得知道「這條錯誤路徑是怎麼走過來的」才能修。ARG 就是那份路徑紀錄。SV 1 的 refinement 也需要這個，只是那時沒給它名字。

0.6 precision：每個位置各自的精細度

$\pi$ 是一個從程式位置映到predicate 集合的函數。$\pi(l_4) = \{x = y\}$ 的意思是「在位置 $l_4$，追蹤 $x = y$ 這個 predicate」。

這就是 SV 1 那張「每個位置一份清單」的表，被寫成了框架的一等公民。

以上是前置。接下來是論文本身。

1 這篇要解決的問題

兩個問題，一個理論一個實務：

1. BMC、k-induction、predicate abstraction、IMPACT 之間的關係到底是什麼？
2. 它們的效能數據能不能公平比較？

第二個問題其實依賴第一個——只有先證明它們是同一個框架的不同設定，「其他變因都相同」的比較才做得出來。

2 在這之前，卡在哪裡

3 關鍵洞察

3.1 先把框架撐大：CPA+ 與 CPA++

SV 2 的 CPA 是四元組。這篇用的是六元組（定義在 §2.2, p.302）：

多出來的兩個：

• $\Pi$ —— 所有可能 precision 的集合
• $\mathsf{prec}$ —— precision-adjustment operator，可以在執行途中調整精度

3.2 blk：什麼時候做 abstraction

這是最能說明問題的一個旋鈕。

Adjustable-Block Encoding（ABE） 把「多久做一次」變成參數，由 block-adjustment operator blk 控制：

$\mathsf{prec}$ 就是照著 blk 的指示動作（論文 §3.1, p.308）：

看起來嚇人，但意思很簡單：blk 說「該做了」就做 abstraction，否則原封不動放行。

3.3 BMC 的完整配方：blk 不是唯一的旋鈕

這裡要很小心，因為一個常見的說法是錯的。

不能說「調一個 blk 就從 predicate abstraction 變成 BMC」。論文 §4.1（p.315）列的 BMC 配方是四個零件一起：

1. $\mathsf{blk}^{never}$ —— whole-program encoding
2. $\mathsf{fcover}^{id}$ —— 不做 forced covering
3. Loop-Bound CPA $\mathbb{LB}$ —— 每個 loop head 配一個計數器，precision 就是 loop bound $k$。它的 transfer relation 刻意是 unsound 的：計數器到達 $k$ 時不產生後繼狀態，用這個方式擋掉超過 $k$ 圈的路徑
4. 外層再包一個演算法 —— 在 CPA++ 跑完後檢查每個 abstract error state 的 path formula 是否 satisfiable。另可做 forward-condition check，判斷 $k$ 夠不夠大

而 predicate abstraction 走的是 CEGAR + refinement，是完全不同的外層流程。

為什麼這件事值得計較？ 因為論文最重要的立論是「公平比較」，而公平比較的前提正是其他變因都相同、只有一個變因不同。把差別過度簡化成「一個運算子」，反而讓這個立論站不住。

3.4 refine 的四個步驟

論文 §3.2（p.309）把 refinement 拆成四步，這個結構值得原樣記住：

1. Abstract-Counterexample Construction —— 從 ARG 回溯出抽象反例 $\langle e_0, \dots, e_n \rangle$
2. Feasibility Check —— 把每段的 block formula 串成一條 counterexample formula，丟一次 SMT query。有解就是真 bug，無解就是誤報
3. Interpolation —— 求 interpolant 序列（見下）
4. Refinement Strategies —— 兩種選擇：

3.5 從一個 interpolant 到一整個序列

1. $\tau_0 = \mathit{true}$ 且 $\tau_n = \mathit{false}$
2. $\tau_{i-1} \wedge \varphi_i \Rightarrow \tau_i$
3. $\tau_i$ 只用同時出現在 $\bigwedge_{j \le i} \varphi_j$ 與 $\bigwedge_{j > i} \varphi_j$ 的變數

第 2 條是關鍵。 它要求整串前後扣得起來：每一個 $\tau_i$ 都能從前一個加上這一段的公式推出來。

3.6 四個演算法的對照

這是論文 Table 1（p.324）的內容，四個欄位照原樣列出：

表格讀不出來的兩件事，補在這裡。

4 手算一遍

blk 的效果用算的比用讀的清楚。

5 對後續的影響

這篇是 CPAchecker 現在的理論骨架。 上面講的每個零件都對應到實作裡的一個 configuration 選項——四個演算法共用同一份程式碼，差別只在設定檔。

方法論上的影響可能更大。 這篇示範了一件事：要比較演算法，先把它們放進同一份實作、用同一個 solver。帶著這個標準，你之後讀任何驗證工具的論文都可以問一句：這個比較控制了哪些變因？

回頭看三篇的關係：

SV 1 (POPL'04)         SV 2 (CAV'07)              SV 3 (JAR'18)
predicate 從哪來   →   怎麼統一所有分析      →   統一後能公平比較什麼
Craig interpolation    CPA 四元組                 CPA+ / CPA++ 與一組旋鈕
       └──────── 是這個框架的一種設定 ────────┘

6 讀原文時的導覽

37 頁，是三篇裡最長的。不必一次讀完。

建議路徑：§1 → §2 → §3.1 → §3.2 → §4.1，其餘按需要再回頭。

取得原文：台大校內網路可直接下載，見頁首 DOI。