軟件已經無處不在，軟件質量問題也越來越普遍，其造成的系統崩潰、安全漏洞等可能帶來經濟上的損失，甚至威脅我們的生命。程序分析是保障軟件質量的基礎技術和重要手段，已被廣泛應用于提高軟件的可靠性、安全性、性能等多個維度的質量。

今天，我們探討一類特殊的程序分析方法，基于符號抽象的程序分析。首先我會簡單回顧一下 抽象解釋 —— 靜態分析的核心理論。抽象解釋的核心問題之一是，計算程序狀態在給定抽象域內的最佳抽象。針對這個問題，我會介紹符號抽象框架以及幾個和符號抽象有關的其他話題。

# 抽象解釋 #

抽象解釋是靜態分析的核心理論 [1]，其關鍵想法是對程序的可達狀態做一個上近似。

如下圖，假設左邊的黃色橢圓代表程序的可達狀態 Reachable States，右邊的黃色橢圓代表有缺陷的狀態 Bad States。我們想驗證這個程序是否有缺陷，即 Reachable States 是否可能和 Bad States 相交。

靜態分析可以對程序的可達狀態做推理，比如算出一個紅色區域。最終紅色區域可以完全覆蓋左邊的黃色區域，因此我們得到了一個上近似。而且我們看到左邊紅色區域和 Bad States 并不相交，因此我們成功地驗證了這個程序是安全的。

# 1.1 抽象解釋的應用

過去 20 多年來，抽象解釋在工業界得到了很多應用，以下三個可能是比較有代表性的。

第一個是 Astrée，基于數值域抽象解釋，已經成功用于驗證航空航天等安全攸關場景的軟件。

第二個是 TVLA，主要做形態分析，比如驗證垃圾回收算法是否真的回收了內存垃圾。TVLA 把形態分析這個概念給發揚光大了，啟發了很多后續工作，比如基于分離邏輯的形態分析。

第三個是 CodeSurfer/x86，它提出的 Value Set Analysis (VSA) 已經成為了二進制靜態分析框架的標配。

此外，抽象解釋在學術領域也獲得多個榮譽，包括 2013 年 SIGPLAN 的程序語言成就獎， 2018 年的約翰·馮諾依曼獎等。

# 1.2 抽象域及其要素

抽象解釋會通過抽象域來對程序的狀態做數學近似，比如數值域、堆域、字符串域等。其中，數值域可以用來捕捉程序的數值信息，用于查找不同的程序缺陷，包括除零錯誤、整數溢出等。

由于抽象解釋是對程序的可達狀態做上近似，它往往伴隨著一些精度問題。比如我們再次看這個圖，右邊的黃色區 Bad States 和紅色區域 (靜態分析的結果) 是相交的，但事實上 Bad States 和左邊的黃色區域 Reachable States 并不相交，因此我們的靜態分析存在誤報。

# 1.3 最佳抽象

給定一個抽象域比如區間域，怎么計算程序在該抽象域上的、最精確的上近似呢？事實上，這也是抽象解釋理論的一個核心問題：給定一個具體遷移函數 以及抽象域 ，如何得到 在 上的最佳抽象 (最精確的抽象遷移函數)？

抽象解釋理論對 有一個聲明式的定義，但是這個定義是“非構造性”的。通常我們沒有自動化的算法，去應用最佳抽象遷移函數 ，或者去得到 的一個表示。

最佳抽象的形式化定義：

# 符號抽象框架 #

為了解決以上問題，研究人員提出了符號抽象框架。

# 2.1 框架定義和實例

假設我們用邏輯約束φ來編碼一個程序的具體狀態，并且把抽象域看作一個比較受限的邏輯片段 (比如“區間邏輯”)。符號抽象的目標就是找到約束φ 在抽象域上的、最精確的上近似[2]。

我們也可以從邏輯的角度來理解 [3]。給定一個約束φ和一個邏輯片段(對應于抽象域), 找到約束φ在中的最強邏輯后承 (strongest logical consequence)。

下面是一個具體的例子：

考慮約束 φ，其中是整數變量。這個約束有四個可行解。我們可以一眼看出，約束φ在區間域的最佳近似是。但是，在一般情況下，我們應如何計算出一個約束的最佳區間近似呢？這就是符號抽象需要解決的問題。

# 2.2 框架意義和應用

通常，為了實現一個靜態分析器，我們需要建模不同的程序指令 (比如加減乘除)，為其設計不同的抽象遷移函數、并將這些遷移函數組合起來。而使用符號抽象框架后，我們就可以用一個約束來精確編碼一整塊代碼，并且自動得到對于該代碼的最精確近似。

符號抽象的理論和實際意義

然而，由于符號抽象的性能問題，目前在真實的靜態分析器中很少得到應用。當前的少量應用主要包括兩塊。

一是上層源代碼的驗證分析，包括數值屬性、堆屬性等的驗證。對于數值驗證，國防科大的陳立前教授就有相關工作 [4]。目前這些工作主要面向一些相對小規模的程序驗證。

其次是二進制分析，比如做控制流恢復 control flow recovery 等。在歐洲有幾個團隊一直有做相關的工作，GrammaTech 甚至已經將符號抽象用到二進制分析產品中。

但即便有工業級應用，符號抽象在形式化、編程語言、甚至抽象解釋社區也都還不夠普及。

# 延伸思考 #

下面分享一些引申思考。回到符號抽象的定義： 是表達力豐富的邏輯，抽象域 對應于 一個子集 。給定 ，找到它在 的最強邏輯后承。

其實計算機科學中的很多問題都跟這個問題相關，下面我們舉幾個例子。

第一個是謂詞抽象 predicate abstraction [5]，它可以看作符號抽象的一個特殊實例。假設我們有一些謂詞集合

，

謂詞抽象的抽象域 就是 中命題的任意布爾組合，比如 。在用于程序驗證時，結合一些不動點迭代方式，我們還能算出 能表達的最強循環不變式。

第二個是量詞消去 quantifier elimination。給定，假設抽象域是只使用特定約束變量集合的約束。那么，存在量詞消去existential quantifier elimination 的目標就是計算在中的最強邏輯后承。

第三個是人工智能里面的 Forgetting 問題 [6]，和量詞消去問題類似。這是港科大 Fangzhen Lin 教授發明的概念，在邏輯 AI 領域很有名。

第四個是 線性規劃 問題，它也可以看作符號抽象問題的一個實例。 即線性約束集合， (其中， 是線性目標函數)。

個人認為符號抽象問題有超越靜態分析、編程語言，甚至超越計算機科學領域的意義，具有深遠的理論蘊含。而且針對相關問題的算法也有一些共通性，比如基于模型的泛化等。

# 總結與展望 #

最后，我們一起從 程序合成 的視角來理解符號抽象 (程序合成是指如何自動從規約中生成程序)。那么，回顧今天的主題，我們的規約是什么？我們應如何從這個規約中生成靜態分析器呢？

審核編輯：劉清