探討一下基于符號抽象的程序分析

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

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

# 抽象解釋 #

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

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

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

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

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

第一個是 Astrée，基于數(shù)值域抽象解釋，已經(jīng)成功用于驗證航空航天等安全攸關(guān)場景的軟件。

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

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

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

# 1.2 抽象域及其要素

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

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

# 1.3 最佳抽象

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

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

最佳抽象的形式化定義：

# 符號抽象框架 #

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

# 2.1 框架定義和實例

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

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

下面是一個具體的例子：

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

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

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

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

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

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

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

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

# 延伸思考 #

下面分享一些引申思考?；氐椒柍橄蟮亩x： 是表達力豐富的邏輯，抽象域 對應(yīng)于 一個子集 。給定 ，找到它在 的最強邏輯后承。

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

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

，

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

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

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

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

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

# 總結(jié)與展望 #

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

審核編輯：劉清