軟件已經(jīng)無(wú)處不在，軟件質(zhì)量問(wèn)題也越來(lái)越普遍，其造成的系統(tǒng)崩潰、安全漏洞等可能帶來(lái)經(jīng)濟(jì)上的損失，甚至威脅我們的生命。程序分析是保障軟件質(zhì)量的基礎(chǔ)技術(shù)和重要手段，已被廣泛應(yīng)用于提高軟件的可靠性、安全性、性能等多個(gè)維度的質(zhì)量。

今天，我們探討一類(lèi)特殊的程序分析方法，基于符號(hào)抽象的程序分析。首先我會(huì)簡(jiǎn)單回顧一下 抽象解釋 —— 靜態(tài)分析的核心理論。抽象解釋的核心問(wèn)題之一是，計(jì)算程序狀態(tài)在給定抽象域內(nèi)的最佳抽象。針對(duì)這個(gè)問(wèn)題，我會(huì)介紹符號(hào)抽象框架以及幾個(gè)和符號(hào)抽象有關(guān)的其他話題。

# 抽象解釋 #

抽象解釋是靜態(tài)分析的核心理論 [1]，其關(guān)鍵想法是對(duì)程序的可達(dá)狀態(tài)做一個(gè)上近似。

如下圖，假設(shè)左邊的黃色橢圓代表程序的可達(dá)狀態(tài) Reachable States，右邊的黃色橢圓代表有缺陷的狀態(tài) Bad States。我們想驗(yàn)證這個(gè)程序是否有缺陷，即 Reachable States 是否可能和 Bad States 相交。

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

# 1.1 抽象解釋的應(yīng)用

過(guò)去 20 多年來(lái)，抽象解釋在工業(yè)界得到了很多應(yīng)用，以下三個(gè)可能是比較有代表性的。

第一個(gè)是 Astrée，基于數(shù)值域抽象解釋?zhuān)呀?jīng)成功用于驗(yàn)證航空航天等安全攸關(guān)場(chǎng)景的軟件。

第二個(gè)是 TVLA，主要做形態(tài)分析，比如驗(yàn)證垃圾回收算法是否真的回收了內(nèi)存垃圾。TVLA 把形態(tài)分析這個(gè)概念給發(fā)揚(yáng)光大了，啟發(fā)了很多后續(xù)工作，比如基于分離邏輯的形態(tài)分析。

第三個(gè)是 CodeSurfer/x86，它提出的 Value Set Analysis (VSA) 已經(jīng)成為了二進(jìn)制靜態(tài)分析框架的標(biāo)配。

此外，抽象解釋在學(xué)術(shù)領(lǐng)域也獲得多個(gè)榮譽(yù)，包括 2013 年 SIGPLAN 的程序語(yǔ)言成就獎(jiǎng)， 2018 年的約翰·馮諾依曼獎(jiǎng)等。

# 1.2 抽象域及其要素

抽象解釋會(huì)通過(guò)抽象域來(lái)對(duì)程序的狀態(tài)做數(shù)學(xué)近似，比如數(shù)值域、堆域、字符串域等。其中，數(shù)值域可以用來(lái)捕捉程序的數(shù)值信息，用于查找不同的程序缺陷，包括除零錯(cuò)誤、整數(shù)溢出等。

由于抽象解釋是對(duì)程序的可達(dá)狀態(tài)做上近似，它往往伴隨著一些精度問(wèn)題。比如我們?cè)俅慰催@個(gè)圖，右邊的黃色區(qū) Bad States 和紅色區(qū)域 (靜態(tài)分析的結(jié)果) 是相交的，但事實(shí)上 Bad States 和左邊的黃色區(qū)域 Reachable States 并不相交，因此我們的靜態(tài)分析存在誤報(bào)。

# 1.3 最佳抽象

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

抽象解釋理論對(duì) 有一個(gè)聲明式的定義，但是這個(gè)定義是“非構(gòu)造性”的。通常我們沒(méi)有自動(dòng)化的算法，去應(yīng)用最佳抽象遷移函數(shù) ，或者去得到 的一個(gè)表示。

最佳抽象的形式化定義：

# 符號(hào)抽象框架 #

為了解決以上問(wèn)題，研究人員提出了符號(hào)抽象框架。

# 2.1 框架定義和實(shí)例

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

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

下面是一個(gè)具體的例子：

考慮約束 φ，其中是整數(shù)變量。這個(gè)約束有四個(gè)可行解。我們可以一眼看出，約束φ在區(qū)間域的最佳近似是。但是，在一般情況下，我們應(yīng)如何計(jì)算出一個(gè)約束的最佳區(qū)間近似呢？這就是符號(hào)抽象需要解決的問(wèn)題。

# 2.2 框架意義和應(yīng)用

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

符號(hào)抽象的理論和實(shí)際意義

然而，由于符號(hào)抽象的性能問(wèn)題，目前在真實(shí)的靜態(tài)分析器中很少得到應(yīng)用。當(dāng)前的少量應(yīng)用主要包括兩塊。

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

其次是二進(jìn)制分析，比如做控制流恢復(fù) control flow recovery 等。在歐洲有幾個(gè)團(tuán)隊(duì)一直有做相關(guān)的工作，GrammaTech 甚至已經(jīng)將符號(hào)抽象用到二進(jìn)制分析產(chǎn)品中。

但即便有工業(yè)級(jí)應(yīng)用，符號(hào)抽象在形式化、編程語(yǔ)言、甚至抽象解釋社區(qū)也都還不夠普及。

# 延伸思考 #

下面分享一些引申思考。回到符號(hào)抽象的定義： 是表達(dá)力豐富的邏輯，抽象域 對(duì)應(yīng)于 一個(gè)子集 。給定 ，找到它在 的最強(qiáng)邏輯后承。

其實(shí)計(jì)算機(jī)科學(xué)中的很多問(wèn)題都跟這個(gè)問(wèn)題相關(guān)，下面我們舉幾個(gè)例子。

第一個(gè)是謂詞抽象 predicate abstraction [5]，它可以看作符號(hào)抽象的一個(gè)特殊實(shí)例。假設(shè)我們有一些謂詞集合

，

謂詞抽象的抽象域 就是 中命題的任意布爾組合，比如 。在用于程序驗(yàn)證時(shí)，結(jié)合一些不動(dòng)點(diǎn)迭代方式，我們還能算出 能表達(dá)的最強(qiáng)循環(huán)不變式。

第二個(gè)是量詞消去 quantifier elimination。給定，假設(shè)抽象域是只使用特定約束變量集合的約束。那么，存在量詞消去existential quantifier elimination 的目標(biāo)就是計(jì)算在中的最強(qiáng)邏輯后承。

第三個(gè)是人工智能里面的 Forgetting 問(wèn)題 [6]，和量詞消去問(wèn)題類(lèi)似。這是港科大 Fangzhen Lin 教授發(fā)明的概念，在邏輯 AI 領(lǐng)域很有名。

第四個(gè)是 線性規(guī)劃 問(wèn)題，它也可以看作符號(hào)抽象問(wèn)題的一個(gè)實(shí)例。 即線性約束集合， (其中， 是線性目標(biāo)函數(shù))。

個(gè)人認(rèn)為符號(hào)抽象問(wèn)題有超越靜態(tài)分析、編程語(yǔ)言，甚至超越計(jì)算機(jī)科學(xué)領(lǐng)域的意義，具有深遠(yuǎn)的理論蘊(yùn)含。而且針對(duì)相關(guān)問(wèn)題的算法也有一些共通性，比如基于模型的泛化等。

# 總結(jié)與展望 #

最后，我們一起從 程序合成 的視角來(lái)理解符號(hào)抽象 (程序合成是指如何自動(dòng)從規(guī)約中生成程序)。那么，回顧今天的主題，我們的規(guī)約是什么？我們應(yīng)如何從這個(gè)規(guī)約中生成靜態(tài)分析器呢？

審核編輯：劉清