抽象解釋及其應(yīng)用研究進展

陳立前 范廣生,3 尹幫虎 王 戟,3

1（國防科技大學(xué)計算機學(xué)院 長沙 410073）

2（國防科技大學(xué)系統(tǒng)工程學(xué)院 長沙 410073）

3（高性能計算國家重點實驗室（國防科技大學(xué)）長沙 410073）

抽象解釋是一種對用于形式描述復(fù)雜系統(tǒng)行為的數(shù)學(xué)結(jié)構(gòu)進行抽象和近似并推導(dǎo)或驗證其性質(zhì)的理 論，由Patrick Cousot[1-2]和Radhia Cousot[1]于20 世紀70 年代提出.抽象解釋提供了一個通用的理論框架，使得人們能夠在該框架下討論不同形式化方法各自能提供的理論保證，如可靠性、完備性、不完備性等.例如，基于抽象解釋，人們能夠解釋調(diào)試、演繹證明、模型檢驗、靜態(tài)分析等方法的優(yōu)勢和局限性.

目前，抽象解釋在語義模型、不變式生成、程序分析驗證、混成系統(tǒng)驗證、程序轉(zhuǎn)換、系統(tǒng)生物學(xué)模型分析等領(lǐng)域取得了廣泛應(yīng)用.在抽象解釋的發(fā)展過程中，除了理論本身的發(fā)展完善，也涌現(xiàn)出了一批優(yōu)秀的抽象解釋工具.20 世紀90 年代，研究人員開發(fā)了基于抽象解釋的靜態(tài)分析工具Polyspace，并成功商業(yè)化[3].2003 年左右，Blanchet 等人[4]基于抽象解釋開發(fā)了靜態(tài)分析工具Astrée[4]，并商業(yè)化[5]，它主要用于檢測C 語言編寫的運算密集型安全攸關(guān)嵌入式實時軟件系統(tǒng)中運行時的錯誤（包括算術(shù)溢出、除零錯、數(shù)組越界等），并成功對空客A340（約13.2 萬行C 代碼）、A380（約35 萬行C 代碼）等系列飛機的飛行控制軟件進行了分析，實現(xiàn)了“零誤報”，這是當時驗證工具在驗證規(guī)模上的重大突破.2015 年，Miné等人[6]進一步開發(fā)了面向多線程并發(fā)程序的靜態(tài)分析工具AstréeA，它作為Astrée 的并發(fā)版本，已實際應(yīng)用于空客飛行系統(tǒng)軟件，所分析程序的最大規(guī)模達百萬行.

近年來，抽象解釋在理論與應(yīng)用方面都取得了進一步發(fā)展.本文重點介紹最近5 年抽象解釋在理論、基于抽象解釋的程序分析、基于抽象解釋的可信人工智能和其他典型應(yīng)用等方面的進展，并討論抽象解釋領(lǐng)域未來的發(fā)展方向.

1 抽象解釋理論

本節(jié)主要介紹抽象解釋的基本概念、理論及抽象域方面的進展.

1.1 基本概念

抽象解釋為建立具體空間與抽象空間之間的聯(lián)系提供了形式化的理論方法.我們將具體空間中推理對象的集合及其上的操作所構(gòu)成的數(shù)學(xué)結(jié)構(gòu)稱為“具體域”，而將抽象空間推理對象的集合及其上的操作所構(gòu)成的數(shù)學(xué)結(jié)構(gòu)稱為“抽象域”.抽象解釋理論利用Galois 連接來形式化地描述具體域與抽象域之間的關(guān)系.對于給定的2 個偏序集 和 ，其中稱為具體域，稱為抽象域，函數(shù) α:D→D#與函數(shù) γ:D#→D構(gòu)成的函數(shù)對(α，γ)稱為D與D#之間的Galois 連接，當且僅當 ?x∈D，x#∈D#，α(x) ?#x#?x? γ(x#)，α 稱為抽象化函數(shù)，γ 稱為具體化函數(shù).對于具體域D中的元素x和抽象域D#中的元素x#，若 α(x) ?#x#(亦即x? γ(x#))，則稱x#是x的可靠抽象（也稱上近似抽象）；對于具體域D上的函數(shù)f和抽象域D#上的函數(shù)f#，若 ?x#∈D#，(f?γ) (x#) ?(γ?f#) (x#)，則稱f#是f的可靠抽象.

抽象解釋通過在抽象域上計算抽象函數(shù)的不動點來獲得抽象語義，并基于此進行推理.抽象解釋提供了嚴格的理論來保證基于上近似抽象的推理的可靠性，即所有基于上近似抽象推理得出的抽象空間中的性質(zhì)在具體空間中也必然成立.但是，由于上近似抽象引入了精度損失，抽象解釋不保證所有在具體空間中成立的性質(zhì)都能基于上近似抽象推理得到.

1.2 理論進展

在理論框架方面，Cousot 等人[7]提出了一種稱為A2I（abstract2interpretation），也稱元抽象解釋的技術(shù)，它用于對基于抽象解釋的程序分析作進一步的抽象解釋，即應(yīng)用抽象解釋對程序分析工具的性質(zhì)開展分析.A2I 既可離線應(yīng)用也可在線應(yīng)用.離線A2I既可在分析程序之前開展（如變量打包技術(shù)），也可在分析程序之后開展（如警告診斷）；在線A2I 則既可在分析程序過程中開展（如面向數(shù)值抽象域的動態(tài)變量劃分技術(shù)），也可用于優(yōu)化底層程序分析的精度和效率，如應(yīng)用A2I，可以在原有程序分析基礎(chǔ)上構(gòu)建更加高效、更加精確的程序分析算法.換言之，A2I提供了一種通用的方法，使得不僅能應(yīng)用抽象解釋分析程序的性質(zhì)還能應(yīng)用抽象解釋分析程序分析工具的性質(zhì).

Bruni 等人[8]在抽象解釋框架下提出了局部完備性（local completeness）概念，它只考慮特定的而非所有的輸入，并定義了一種支持局部完備抽象解釋推理的邏輯LCLA，通過結(jié)合上近似和下近似，可支持某些程序規(guī)約的正確性（程序不存在錯誤）和不正確性表示，斷言Q是post[c](P)的最強后置條件的下近似，(程序存在錯誤)證明.該邏輯LCLA通過 ?A[P]c[Q]來且使得Q在抽象域A上的抽象和post[c](P)一致.?A[P]c[Q] 不僅保證了Q中的所有報警都是正報，還保證了若Q中沒有報警則c是正確的.因為LCLA邏輯對于非局部完備抽象域不適用，需要修復(fù)這些抽象域以滿足局部完備性.為此，Bruni 等人[9]進一步提出了一種稱為抽象解釋修復(fù)（abstract interpretation repair）的方法，展示了如何利用局部完備性的概念以一種最優(yōu)的方式來精化抽象域，以增強程序驗證的精度.應(yīng)用這種方法，并不要求在分析之前選擇合適的抽象域，而是可以從任意抽象域開始，對其需達到的局部完備性逐步進行修復(fù).抽象解釋修復(fù)技術(shù)之于抽象解釋，類似于反例制導(dǎo)抽象精化技術(shù)之于抽象模型檢驗.該工作給出了最優(yōu)局部完備精化存在的充要條件.基于此，提出了2 種修復(fù)策略，使得能夠在一個給定的抽象計算上消除所有的誤報：一種策略是隨著具體計算進行前向修復(fù)；另一種是在抽象計算過程中進行后向修復(fù).換而言之，抽象解釋修復(fù)的目標是找到最為抽象的，但又能消除不完備抽象計算中所有誤報的抽象域.不過，到目前為止，如何找到充分條件保證抽象解釋修復(fù)的終止性依然是開放的研究問題.最近，Campion 等人[10]提出了一種理論來對抽象解釋中分析的不精確性帶來的誤差的傳播進行估計.其主要思想是在抽象域上增加了一個度量距離的操作，用于度量不同抽象域元素之間的相對不精確程度.該工作引入了部分完備性（partial completeness）的概念.部分完備性允許產(chǎn)生一些誤報，但是誤報數(shù)量是有界的.部分完備性使得能夠通過調(diào)整在分析中允許的噪聲的量，來對不完備分析進行精化.該工作設(shè)計了一個證明系統(tǒng)來估計抽象解釋器在程序分析過程中累積誤差的上界.在該證明系統(tǒng)中，用 ?A[Pre]P[Post，ε]來表示后置條件Post在抽象域A上的抽象和程序P在輸入Pre上具體語義下結(jié)果的抽象之間的距離不超過ε.ε可理解為抽象解釋器在分析輸入滿足Pre的程序P的過程中累積的不精確度的上界.ε部分完備性表示抽象解釋的不精確的程度不超過ε，即，具體語義下結(jié)果的抽象和抽象解釋在給定輸入下的分析結(jié)果之間的距離不超過ε.

另外，在抽象解釋的完備性相關(guān)研究方面，Bonchi 等人[11]展示了共歸納up-to 技術(shù)（最初用于并發(fā)系統(tǒng)互模擬證明）與抽象解釋存在關(guān)聯(lián)關(guān)系.具體而言，在一定假設(shè)下，共歸納可靠up-to 技術(shù)與完備抽象技術(shù)之間存在理論上的聯(lián)系，這樣2 種技術(shù)之間可以進行技術(shù)遷移.Bruni 等人[12]將程序的外延（功能）等價性一般化為抽象等價性.2 個程序是外延等價的，當且僅當2 者在具體語義下是等價的.2 個外延等價的程序，可能具有不同的抽象語義（如，因為程序代碼進行了變換，導(dǎo)致抽象語義產(chǎn)生了差異）.文獻[12]工作引入了完備團（completeness cliques）和不完備團（incompleteness cliques）的概念來對程序進行分類.完備團C(P，A)表示所有與程序P語義等價，且抽象域A對其而言是完備的那些程序構(gòu)成的集合；不完備團(P，A)表示所有與程序P語義等價、且抽象域A對其而言不是完備的那些程序構(gòu)成的集合.換言之，C(P，A)表示所有應(yīng)用抽象域A分析得到的結(jié)果是足夠精確（無誤報）的程序P的變種構(gòu)成的集合；而(P，A)表示所有應(yīng)用抽象域A分析得到的結(jié)果是不夠精確的（存在誤報）的程序P的變種構(gòu)成的集合.應(yīng)用抽象等價性的概念，可以幫助理解代碼迷惑技術(shù)和程序分析精度之間的關(guān)聯(lián)關(guān)系.

在抽象解釋效率優(yōu)化方面，Stein 等人[13]提出了一種結(jié)合了增量式和按需驅(qū)動的抽象解釋技術(shù)，其核心是定義了一種動態(tài)演進的按需抽象解釋圖表示，它能夠顯式地表示程序語句、抽象狀態(tài)和分析過程中計算之間的依賴關(guān)系.基于這種圖表示，程序編輯、用戶產(chǎn)生的查詢、抽象語義計值能夠統(tǒng)一處理，不同于已有的增量式或按需驅(qū)動的技術(shù)，該技術(shù)適用于任意抽象域（包括帶加寬操作的抽象域）.Wei 等人[14]提出了分階段抽象解釋器（staged abstract interpreter）的概念.在編譯技術(shù)中，分階段解釋器是一個編譯器，它針對一個給定程序，將解釋器定制化得到一個等價的但是運行效率更高的可執(zhí)行程序.抽象解釋器是一個程序分析器，如果將定制化技術(shù)應(yīng)用于抽象解釋器將得到一個分階段抽象解釋器.文獻[14]的工作將部分求值技術(shù)中的第一Futamura 投影定理[15]從應(yīng)用于具體解釋器擴展到應(yīng)用于抽象解釋器，從而能夠得到一個分階段抽象解釋器.分階段抽象解釋器可用于對靜態(tài)分析進行優(yōu)化，且使得實現(xiàn)優(yōu)化僅需要較小的工程量且又不損害可靠性.

抽象解釋為設(shè)計不變式推導(dǎo)方法提供了一個通用框架，而性質(zhì)制導(dǎo)可達性（property-directed reachability,PDR），也稱IC3，則是近年來不變式推導(dǎo)領(lǐng)域的重要突破之一.最近，F(xiàn)eldman 等人[16]展示了PDR 與抽象解釋之間在理論上的關(guān)聯(lián)關(guān)系，即命題PDR 可以轉(zhuǎn)換為邏輯抽象域上的一個抽象解釋算法.具體而言，該工作設(shè)計了PDR 的一個變種版本，稱為∧-PDR，其中反例的所有一般化都被用來增強（用于構(gòu)造歸納不變式的）公式序列，以阻止反例.該工作展示了∧-PDR 推導(dǎo)不變式過程對應(yīng)于抽象域上最佳轉(zhuǎn)換子上的Kleene 迭代.

1.3 抽象域進展

抽象域是抽象解釋框架的核心要素，也是抽象解釋在實踐中取得成功應(yīng)用的一個關(guān)鍵因素.抽象域包括抽象語義的選擇、數(shù)據(jù)結(jié)構(gòu)和算法的設(shè)計、實現(xiàn)的決策等方面.抽象解釋框架提供了構(gòu)造性的和系統(tǒng)性的方法來設(shè)計、組合、比較、研究、證明和應(yīng)用抽象域.到目前為止，已經(jīng)涌現(xiàn)出數(shù)十種抽象域.大致可以分為2 類：數(shù)值抽象域（區(qū)間、同余、八邊形、多面體、多項式等）和符號抽象域（如形態(tài)、樹）.抽象解釋為抽象域提供了各種通用的算子（乘積、冪集、補全等）.抽象域已經(jīng)廣泛應(yīng)用于各種系統(tǒng)（硬件、軟件、神經(jīng)網(wǎng)絡(luò)等）的多種性質(zhì)（安全性、終止性、概率性質(zhì)等）的分析驗證中.目前，也出現(xiàn)了多個開源抽象域庫，如APRON[17]，ELINA[18]，PPL[19]，PPLite[20]，VPL[21]等.

近年來，在提升抽象域的計算效率方面，Singh等人[22-23]提出了一種降低數(shù)值抽象域時空開銷但又不影響分析精度的分解（decomposition）技術(shù).其主要思想是：根據(jù)變量之間以及變量與程序語句之間的依賴關(guān)系，將一個抽象域元素分解為程序變量集的不相交子集上抽象域元素的笛卡爾乘積.這樣，抽象域算子不需要應(yīng)用于整個抽象域元素上，而只需要應(yīng)用于其中相關(guān)的部分上，從而減少時空開銷.這種技術(shù)適用于任意基于線性約束表示的數(shù)值抽象域，如八邊形、多面體.從實現(xiàn)角度，對變量集應(yīng)用分解技術(shù)之后，可以通過手工方式實現(xiàn)域操作的分解（即需要人工重新實現(xiàn)抽象域的域操作），以使得域操作能適用于變量集的劃分.進一步，Singh 等人[18]提出了一種通用的在線分解技術(shù)，在分析過程中自動動態(tài)調(diào)整變量集劃分，能夠在不改變原抽象域操作的基礎(chǔ)上自動實現(xiàn)基于在線分解的抽象域優(yōu)化.實驗結(jié)果表明，在不損失分析精度的前提下，分解技術(shù)能獲得極大的性能提升.比如，基于分解技術(shù)優(yōu)化后的八邊形抽象分析的性能提升超過百倍[22].Singh等人基于分解技術(shù)實現(xiàn)了開源的抽象域庫ELINA[18].最近，Gange 等人[24]基于加權(quán)有向圖的切分規(guī)范型（split normal form），給出了Zone 抽象域和八邊形抽象域的高效實現(xiàn)方法.圖表示上的閉包算法是這2 個抽象域的核心算法.這2 個抽象域的傳統(tǒng)實現(xiàn)方法在圖表示上基于Dijkstra 最短路徑閉包算法計算閉包時，會根據(jù)變量界{x≥c1，y≤c2}引入差分界約束y?x≤c2?c1，使得x和y建立了關(guān)聯(lián)關(guān)系，從而使得圖表示更稠密，進而影響了效率.引入切分規(guī)范型的主要目的是盡量保持內(nèi)部圖表示的稀疏性，同時使得閉包更高效.比如，重新計算圖的閉包時，避免加入因變量界信息引入的約束關(guān)系.此外，考慮抽象域操作對抽象狀態(tài)的增量式更新，Chawdhary 等人[25]最近針對八邊形抽象域設(shè)計了平方復(fù)雜度的增量式算法來計算閉包，提升了八邊形抽象域的計算效率.

在提升抽象域表達能力方面，Chen 等人[26]基于二叉決策樹設(shè)計了一個抽象域函子，其中樹的分支節(jié)點為路徑布爾條件，葉節(jié)點為數(shù)值或符號抽象域，以提升抽象域在依賴路徑的靜態(tài)分析中的精度.最近，Chen 等人[1,27-28]在抽象域域表示中加入了對程序變量的值與絕對值間關(guān)系的刻畫，設(shè)計實現(xiàn)了線性絕對值等式抽象域，能夠推斷程序中一部分分段線性行為（如條件分支、絕對值函數(shù)調(diào)用和最大或最小值函數(shù)調(diào)用等）所蘊含的非凸析取性質(zhì).在析取區(qū)間分析方面，Gange 等人[29]使用范圍決策圖（range decision diagrams）代替二叉決策圖，重新設(shè)計實現(xiàn)了Gurfinkel 等人[30]提出的Boxes 抽象域（該抽象域能夠表達多個Box 的析取并刻畫部分路徑條件信息），使得Boxes 抽象域的實現(xiàn)更高效、對于非線性表達式的精度也更高.

在多面體抽象域?qū)崿F(xiàn)方面，Maréchal 等 人[31]提出了基于參數(shù)線性規(guī)劃的最小化算子（用于消除域表示中的冗余約束），使得僅基于約束表示的多面體抽象域庫VPL 相比原來提升了幾個數(shù)量級的性能，并與已有基于傳統(tǒng)雙重描述法的多面體抽象域?qū)崿F(xiàn)性能相當.Becchi 等人[32]針對支持嚴格不等式約束的未必封閉多面體域[33]，提出了一種多面體域雙重描述法的新表示方法及其相應(yīng)的類Chernikova 轉(zhuǎn)換算法，這種表示方法完全沒有使用松弛變量，極大提升了分析效率.進一步，Becchi 等人基于該工作開發(fā)了相應(yīng)的開源抽象域庫PPLite[19].

2 基于抽象解釋的程序分析

抽象解釋理論為靜態(tài)程序分析的設(shè)計和構(gòu)建提供了一個通用的框架，并從理論上保證了所構(gòu)建的程序分析的終止性和可靠性.程序分析是抽象解釋最主要的應(yīng)用之一.本節(jié)主要介紹抽象解釋在程序分析中的應(yīng)用及其進展.

2.1 技術(shù)進展

本節(jié)介紹基于抽象解釋的程序分析的最新技術(shù)進展，主要包括如何提高分析的精度、可擴展性和可用性等3 個方面.

1）提高精度

抽象解釋通過迭代計算求解程序語義方程系統(tǒng)的解，即抽象不動點，從而得到程序不變式.當前學(xué)術(shù)界和工業(yè)界的抽象解釋工具基本都采用傳統(tǒng)的不動點迭代算法，即包含加寬和變窄算子的混沌迭代（chaotic iteration）算法.最近，Amato 等人[34]提出在分析過程中交織使用加寬和變窄算子的迭代策略，打破混沌迭代算法中先應(yīng)用加寬算子再應(yīng)用變窄算子的固定順序，使得不動點迭代計算結(jié)果更加精確.Boutonnet 等人[35]提出利用初次迭代計算得到的基本解與加寬點處后向收集的信息來確定一個啟動點，然后重復(fù)應(yīng)用加寬和變窄操作以得到更精確的結(jié)果.

抽象解釋通過加寬算子來加快收斂速度并保證終止性，從而實現(xiàn)高效分析.然而，加寬操作引入的精度損失極大影響了迭代計算的精度.為此，已有工作[4,34]提出了多種方法來減少加寬帶來的精度損失.設(shè)置加寬閾值是彌補加寬精度損失的常用技術(shù).不同于固定的加寬閾值設(shè)定，Cha 等人[36]基于對加寬精度有影響的程序特征，利用機器學(xué)習(xí)的方法對大量代碼的分析結(jié)果進行學(xué)習(xí)，從而得到適應(yīng)不同程序的加寬閾值的最優(yōu)設(shè)定策略.

抽象域作為抽象解釋的重要組成部分，其表達能力直接決定了抽象解釋分析能力.現(xiàn)有抽象域大多數(shù)為線性的數(shù)值抽象域，且不能表達非凸性質(zhì).為彌補抽象域自身表達的局限性，除了設(shè)計新的能夠刻畫析取、非線性的抽象域，將現(xiàn)有抽象域與其他方法結(jié)合是另一種解決方案，這方面近期研究主要可分為2 類：

①通過符號化抽象[37]（symbolic abstraction）求解抽象域的最佳抽象遷移.隨著近年來最優(yōu)化模理論（optimization modulo theories,OMT）的發(fā)展[38-39]，符號化抽象得到進一步發(fā)展.Jiang 等人[40]提出了結(jié)合抽象域與可滿足性模理論（satisfiability modulo theories,SMT）塊級抽象解釋技術(shù)，其主要思想是：把整個程序劃分為一個個程序塊；程序塊的遷移語義采用SMT 公式來精確編碼，塊間信息的傳遞使用抽象域表示；在出程序塊時，應(yīng)用OMT 技術(shù)把SMT 公式抽象為抽象域表示；在循環(huán)頭，采用抽象域上的加寬操作，來保證分析的終止性.這種技術(shù)實現(xiàn)了抽象域與SMT 的優(yōu)勢互補，提升了抽象解釋分析的精度.Yao等人[41]提出了針對無量詞位向量公式的符號化抽象算法，并將其應(yīng)用于符號化區(qū)間抽象和符號化多面體抽象.該工作在設(shè)計符號化抽象時，主要基于2 項觀察：程序變量之間往往具有關(guān)聯(lián)關(guān)系；區(qū)間抽象域和多面體抽象域在位向量算術(shù)下是有界的.該工作利用這2 項觀察來減少冗余計算和縮減符號化抽象的搜索空間，從而提升了基于OMT 的符號化抽象的效率.

②提高抽象域的非線性表達能力.基于組合遞推分析（compositional recurrence analysis）[42]將符號化分析與抽象解釋結(jié)合起來可以生成多項式、指數(shù)、對數(shù)等形式的非線性不變式，并且能取得與抽象精化同樣精確的結(jié)果.Kincaid 等人[43]最近還將組合遞推分析進一步應(yīng)用于遞歸程序分析與資源界分析中，并在結(jié)合多種數(shù)值推導(dǎo)方法后提升了多種非線性數(shù)值不變式生成的精度與效率[44].此外，Allamigeon 等人[45]提出基于橢圓冪集的方法來生成析取二次不變式.

通過抽象解釋與動態(tài)分析的結(jié)合，同樣可以提升程序分析的精度.針對目前基于抽象解釋的程序驗證技術(shù)存在的不變式精度不夠、沒有利用目標性質(zhì)以及不擅長產(chǎn)生反例等問題，Yin 等人[46]提出了一種待驗證性質(zhì)制導(dǎo)的、結(jié)合迭代抽象解釋和有界枚舉測試的程序驗證框架，通過前/后向抽象解釋分析的迭代精化以及與測試技術(shù)的結(jié)合，提升基于抽象解釋的程序驗證的能力.Toman 等人[47]最近提出了結(jié)合具體測試和抽象解釋技術(shù)的框架Concerto，用以分析基于框架的應(yīng)用程序，其中，利用具體測試來分析框架實現(xiàn)部分，使用抽象解釋來分析應(yīng)用代碼部分.Chen 等人[48]提出了一種貝葉斯框架DynaBoost，使用從動態(tài)測試執(zhí)行過程中獲得的信息來對基于抽象解釋的靜態(tài)分析的報警進行優(yōu)先級排序，以減少靜態(tài)分析的誤報.

最近，O'Hearn[49]提出了不正確性邏輯（incorrectness logic），作為霍爾邏輯(用于證明程序不存在錯誤)對偶的版本，用于證明程序存在錯誤.不正確性邏輯三元組 [presumption]f[?:result] 表示，任何滿足結(jié)果 條件result的最終狀態(tài)可由滿足前提條件presumption的初始狀態(tài)執(zhí)行f后得到，其中，?為ok（表示正常結(jié)束）或er（表示錯誤結(jié)束）.基于不正確性邏輯，目前衍生了不正確性分離邏輯[50]和不正確性并發(fā)分離邏輯[51]，在此基礎(chǔ)上設(shè)計實現(xiàn)的工具Pulse-X[52]已經(jīng)可以實現(xiàn)對OpenSSL 內(nèi)存漏洞的檢測.不正確性邏輯采用下近似推理.在文獻[49]中，O'Hearn 討論了如何使用抽象解釋理論指導(dǎo)和解釋不正確性邏輯問題，即如何利用基于抽象解釋的程序分析查找真實的錯誤.沿著這一思路，Ascari 等人[53]討論了設(shè)計下近似抽象域所面臨的困難.

2）提高可擴展性

提升抽象解釋可擴展性，使其支持更大規(guī)模程序的高效分析，是抽象解釋在實際中成功應(yīng)用的關(guān)鍵.近期相關(guān)研究進展主要包括3 個方面.

①改進抽象解釋框架下不動點迭代算法.基于程序依賴圖弱拓撲序（weak topological order）的混沌迭代過程為串行執(zhí)行，具有三次方的最壞時間復(fù)雜度，并且可能會因為過深層次的程序依賴而導(dǎo)致棧溢出.為此，研究人員考慮通過不動點迭代的并行執(zhí)行來提升分析的可擴展性.最近，Kim 等人[54]在抽象解釋工具IKOS[55]中將混沌迭代的弱拓撲序擴展為弱偏序（weak partial order），并基于計算循環(huán)嵌套森林的算法[56]，提出了一種最壞線性時間復(fù)雜度的確定性并行不動點迭代算法，并在16 核上開展了實驗，在保證與串行分析結(jié)果一致的同時，性能最大提升10.97倍.不同于利用CPU 并行處理能力，內(nèi)存優(yōu)化同樣可以提升不動點迭代性能.Kim 等人[57]提出了一種近似線性時間復(fù)雜度的不動點迭代算法，通過在混沌迭代過程中及時釋放存儲抽象值的內(nèi)存，并在不動點計算期間而非計算結(jié)束后執(zhí)行斷言檢查，使得IKOS 在緩沖區(qū)溢出過程間分析時的內(nèi)存使用峰值平均降低到43.7%.

②基于抽象解釋的參數(shù)化程序分析[58].參數(shù)化程序分析將程序分析視為黑盒，尋找程序分析在性能表現(xiàn)、精確性和可靠性間的權(quán)衡.在這方面研究中，機器學(xué)習(xí)的方法發(fā)揮了重要作用.Heo 等人[59]利用支持向量機學(xué)習(xí)在哪些可能的程序構(gòu)件中允許采用非可靠的分析方法，并保留正確報警，以提升抽象解釋工具的缺陷檢測能力.Heo 等人[60]還提出了一種資源敏感的分析方法，通過強化學(xué)習(xí)一個控制器來控制程序抽象的粗化程度，以在不動點迭代期間跟蹤分析過程消耗內(nèi)存等資源的情況，并動態(tài)調(diào)整其行為，使得在滿足資源約束的條件下取得高精度的分析結(jié)果.

③提升抽象域分析效率.更高精度的抽象域，往往伴隨著更高的時空開銷.在當前的主要程序分析工具中，八邊形抽象域和多面體抽象域表現(xiàn)仍然難以適應(yīng)大規(guī)模分析，因而針對這2 種抽象域可擴展性的研究一直是熱點話題.除了針對抽象域?qū)崿F(xiàn)本身的優(yōu)化[22-24]之外，有研究開始關(guān)注利用機器學(xué)習(xí)來加速抽象域分析.Singh 等人[61]提出了一種基于強化學(xué)習(xí)來加速靜態(tài)程序分析的方法，在每次迭代過程中，利用強化學(xué)習(xí)來決策選擇使用抽象域操作多種實現(xiàn)中的某一種，以實現(xiàn)分析精度和效率的均衡.He等人[62]提出了一種數(shù)據(jù)驅(qū)動的自適應(yīng)學(xué)習(xí)方法，通過迭代學(xué)習(xí)算法來識別和刪除分析過程中產(chǎn)生的抽象狀態(tài)序列中的冗余狀態(tài)約束，能夠在提高現(xiàn)有數(shù)值程序分析效率的同時不會造成顯著的精度損失.

3）提高可用性

實際中，待分析程序可能由不同程序語言實現(xiàn)，包含復(fù)雜數(shù)據(jù)結(jié)構(gòu)，涉及各種不同程序特征.如何使抽象解釋能夠在實際中支持各種復(fù)雜數(shù)據(jù)結(jié)構(gòu)與程序特征并取得較好效果一直是研究人員關(guān)注的話題.最近，應(yīng)用抽象解釋對特定類型程序或特定性質(zhì)的分析驗證方面的研究也取得了不少進展.主要包含4 個方面:復(fù)雜數(shù)據(jù)結(jié)構(gòu)自動分析、不同譜系目標程序的分析、程序多種類型性質(zhì)分析、編譯場景下的應(yīng)用.

在復(fù)雜數(shù)據(jù)結(jié)構(gòu)的自動分析方面，在嵌入式代碼中，動態(tài)數(shù)據(jù)結(jié)構(gòu)（如列表、樹）依賴于靜態(tài)連續(xù)存儲區(qū)域（數(shù)組）來實現(xiàn)，為此Liu 等人[63]提出了一種結(jié)合數(shù)組抽象和形態(tài)抽象的靜態(tài)區(qū)域存儲動態(tài)數(shù)據(jù)結(jié)構(gòu)編程模式代碼自動驗證方法.其主要思想是基于對描述數(shù)組數(shù)值性質(zhì)的謂詞和描述動態(tài)結(jié)構(gòu)形態(tài)性質(zhì)的謂詞這2 種謂詞的元級合取，使得可以重用已有的對數(shù)組和動態(tài)結(jié)構(gòu)單獨分析的方法.該工作對嵌入式操作系統(tǒng)內(nèi)核服務(wù)和驅(qū)動程序等包含復(fù)雜數(shù)據(jù)結(jié)構(gòu)的實際程序的安全性質(zhì)和功能性質(zhì)進行了驗證.此外，Journault 等人[64]提出了一種基于抽象解釋的C 程序中字符串類型訪問越界檢測方法.

為提升抽象解釋對形態(tài)相關(guān)程序的分析驗證能力，Illous 等人[65-66]設(shè)計實現(xiàn)了關(guān)系型形態(tài)抽象域，并利用抽象形態(tài)遷移與基于分離邏輯的遷移摘要信息，設(shè)計了一種使用形態(tài)轉(zhuǎn)換關(guān)系作為過程摘要的自頂向下的過程間分析方法.Li 等人[67]提出了一種基于狀態(tài)剪影（silhouette）的抽象內(nèi)存狀態(tài)析取的合并策略，顯著提升了形態(tài)分析的精度，并在形態(tài)分析工具MenCAD 中進行了實現(xiàn).

隨著概率編程的興起，基于抽象解釋的概率程序分析開始進入人們視野[68-69].相比確定性的靜態(tài)程序分析，概率程序靜態(tài)分析因遞歸、非結(jié)構(gòu)化控制流、發(fā)散、不確定性和連續(xù)分布這些特征而更具挑戰(zhàn)性.2018 年Wang 等人[68]提出了一個概率程序分析框架PMAF，用于設(shè)計實現(xiàn)概率程序的靜態(tài)分析，并證明分析的正確性.在PMAF 框架中，Wang 等人[68]引入前馬爾可夫代數(shù)（pre-Markov algebras）以分解出概率程序不同分析中的共同部分，并通過將傳統(tǒng)（非概率）程序的過程間數(shù)據(jù)流分析思想擴展到概率程序分析中，以實現(xiàn)過程間分析和函數(shù)摘要生成.相比概率抽象解釋[70-71]（probabilistic abstract interpretation），PMAF具有2 大優(yōu)勢：一是其基于代數(shù)，為實現(xiàn)新的抽象提供了簡單的聲明式接口；二是其基于不同的語義基礎(chǔ)，這些語義遵循域理論中對非確定概率程序的標準解釋.

在操作系統(tǒng)代碼的安全和功能性分析方面，抽象解釋最近也得到了應(yīng)用[63,72-73].2019 年Gershuni 等人[72]針對Linux 子系統(tǒng)eBPF(其允許在Linux 內(nèi)核中運行用戶編寫的程序)，通過使用Zone 抽象域跟蹤寄存器和偏移間的差異，在抽象解釋的框架下設(shè)計實現(xiàn)了一個針對eBPF 的靜態(tài)分析器.該分析器相比現(xiàn)有的eBPF 靜態(tài)分析工具擁有更低的誤報率和更好的可擴展性，并支持對循環(huán)的分析.

在資源使用量上界分析方面，Carbonneaux 等人[74]提出了一種結(jié)合平攤分析與抽象解釋的精確資源界分析方法，并設(shè)計實現(xiàn)了工具C4B.Fan 等人[75]提出了一種基于抽象解釋的命令式C 程序中動態(tài)分配類型資源（如堆內(nèi)存）使用量上界分析方法，通過對資源分配相關(guān)API 的資源使用建模，引入輔助變量刻畫程序資源使用情況，然后結(jié)合數(shù)值抽象與指向分析，得到任意程序點處的資源使用量不變式.Facebook公司也在推進大規(guī)模程序的資源使用界分析[76]，主要依托于程序分析工具Infer 中WCET 相關(guān)插件與數(shù)值抽象解釋相關(guān)插件.

在編譯相關(guān)技術(shù)方面，Rivera 等人面向浮點程序，設(shè)計并實現(xiàn)了浮點代碼到基于區(qū)間算術(shù)代碼的編譯器IGen[77]和SafeGen[78].IGen 將基于浮點實現(xiàn)的C 函數(shù)轉(zhuǎn)換為等效的使用區(qū)間算術(shù)的可靠C 函數(shù)，在保持較高精度的同時保證運行效率，提高了性能.在IGen 的基礎(chǔ)上，SafeGen 將給定的浮點程序重寫為相應(yīng)的使用仿射算術(shù)的可靠程序，在保持變量之間線性相關(guān)性的同時，與區(qū)間算術(shù)相比實現(xiàn)了更高的精度.在ARM 指令集反匯編場景下，Ye 等人[79]設(shè)計實現(xiàn)了反匯編工具D-ARM，在解釋指令的時候?qū)χ噶顖?zhí)行過程中的具體值和執(zhí)行過程的關(guān)鍵寄存器進行了符號化處理，并映射到抽象域上，為后續(xù)構(gòu)建指令超集圖提供語義信息.

2.2 工具進展

目前，抽象解釋理論在程序分析與驗證領(lǐng)域獲得了廣泛的研究和應(yīng)用.表1 列出了目前主要的基于抽象解釋的程序分析工具.

Astrée[5]作為抽象解釋工具最典型的成功案例已經(jīng)被廣泛應(yīng)用于空客公司的飛控軟件的安全驗證中[4].Astrée 能夠支持對大規(guī)?，F(xiàn)實程序的分析，并且誤報率極低.這主要是因為Astrée 中集成了多種抽象解釋分析優(yōu)化技術(shù)，包括眾多類型的抽象域、多種抽象域間的協(xié)同技術(shù)、跡劃分技術(shù)、模塊化分析技術(shù)等[4,95-96].

CGS（C Global Surveyor）[80]為NASA 內(nèi)部使用的C 程序靜態(tài)分析工具，它主要用于數(shù)組邊界安全性檢查；能夠在幾個小時內(nèi)，以80%的精確度分析28 萬行的火星任務(wù)飛行控制軟件，并成功應(yīng)用于Mars Path-Finder，Deep Space One 和Mars Exploration Rover等航天器的軟件上.CGS 在一個增量式的框架內(nèi)結(jié)合指針分析與數(shù)組下標的數(shù)值分析，分布部署到集群內(nèi)多臺機器上進行協(xié)同分析.

Table 1 Program Analyzers Based on Abstract Interpretation表1 基于抽象解釋的程序分析工具

Polyspace[3]目前為Mathworks 公司旗下的商業(yè)化靜態(tài)程序分析工具.Polyspace 可用于證明程序在所有的控制流和數(shù)據(jù)流下均沒有關(guān)鍵的運行時錯誤.Polyspace 已被成功運用于M-346 教練機自動駕駛儀軟件和沃爾沃汽車部分軟件的安全驗證中.

Sparrow[81]為韓國首爾國立大學(xué)開發(fā)的商業(yè)化C程序抽象解釋工具，其同時存在開源版本.Sparrow采用了許多優(yōu)秀的靜態(tài)分析技術(shù)，以實現(xiàn)可擴展性、精確性和用戶便捷性的統(tǒng)一.在可擴展性方面，Sparrow 使用了稀疏分析框架[97-98]等技術(shù)；在精確性方面，Sparrow實現(xiàn)了可選擇的上下文敏感分析和可選擇的關(guān)系型分析[99]等技術(shù)；而在用戶便捷性方面，Sparrow 支持警報聚類[100]等技術(shù).Sparrow 能實現(xiàn)對Linux 內(nèi)核代碼的高效分析驗證.研究人員還利用機器學(xué)習(xí)技術(shù)，進一步提升Sparrow 的性能[59-60]，并通過動靜態(tài)結(jié)合的方法減少分析的誤報[48].

IKOS[82]是最初由NASA 研究員發(fā)起的一款開源C/C++程序抽象解釋工具.IKOS 已成功支持開源四軸飛行器軟件AeroQuad 和開源無人機控制軟件DIY AutoPilot 的分析驗證.其主要特點包括其自主設(shè)計實現(xiàn)的Gauge 抽象域[101]，以及最近基于并行計算和內(nèi)存優(yōu)化設(shè)計的高效不動點迭代算法[54,57].

Frama-C[83,102-103]為開源C 程序分析平臺，包括多個實現(xiàn)不同功能的插件，其中包含了基于數(shù)值抽象解釋的值分析插件EVA，且不同功能的插件可以互相配合以使得分析驗證更加精確.Frama-C 已成功運用于巴西衛(wèi)星運載火箭VLS-V03 控制軟件、NASA空中交通管理系統(tǒng)的分析驗證中.

Infer[84,104-108]是Facebook 公司開發(fā)的開源程序分析工具，并被用于日常的軟件開發(fā)流程，以提升代碼安全性.Infer 采用組合分析和增量式分析方法.Infer還集成了分離邏輯的實現(xiàn)，以達到更好的內(nèi)存安全檢測效果.此外，Infer 采用基于函數(shù)摘要的過程間分析方法以提升分析的效率.

Goblint[85]主要用于分析多線程程序，特別是用于檢測中斷并發(fā)錯誤.其支持數(shù)據(jù)競爭檢測、斷言檢測、整數(shù)溢出等類型缺陷的檢查.Goblint 結(jié)合指針分析與數(shù)值分析來處理動態(tài)分配和數(shù)組中的鎖[109].Goblint 還將線程模塊非關(guān)系值分析作為局部跡語義的抽象，并基于副作用約束系統(tǒng)以實現(xiàn)更通用、更精確的線程模塊化分析[110].此外，Goblint 最近還對不動點求解算法進行了優(yōu)化，以適應(yīng)更大規(guī)模和更復(fù)雜程序的分析[111-112].值得注意的是，Goblint 是路徑敏感的[113]，并增加了對增量式分析[114]和交互式分析[115]的支持.

Dai[86]為開源C 程序抽象解釋工具，其最大的特點是實現(xiàn)了需求驅(qū)動的抽象解釋分析[13]，使得程序分析能夠交互式進行.

Clam[87]是開源的抽象解釋靜態(tài)分析工具，能分析LLVM 字節(jié)碼并得到歸納不變式.其主要依托于Crab[88]構(gòu)建.Crab 是一個服務(wù)于構(gòu)建基于抽象解釋的靜態(tài)程序分析的開源基礎(chǔ)庫，采用C++實現(xiàn).Crab提供了豐富的抽象域類型、不動點迭代算法的實現(xiàn)，并支持數(shù)據(jù)流分析、過程間分析和后向分析等類型的分析.

SPARTA[89]是Facebook 開源的一個軟件組件庫，用于構(gòu)建基于抽象解釋的高性能靜態(tài)分析器.SPARTA 旨在提供擁有簡單API、性能高、易于集成的軟件組件，以簡化抽象解釋工具構(gòu)建的工程量.由于SPARTA 對抽象解釋復(fù)雜細節(jié)進行了封裝，用戶基于SPARTA 設(shè)計抽象解釋工具時只需要關(guān)注于程序分析的3 個基本方面：1）語義，指待分析的性質(zhì)，如數(shù)值型變量值范圍、別名關(guān)系等；2）劃分，指被分析性質(zhì)的粒度，如過程內(nèi)/過程間分析、上下文敏感/不敏感分析等；3）抽象，指程序性質(zhì)的表示方法，如區(qū)間、別名圖等.SPARTA 的成功應(yīng)用是為Facebook開發(fā)的Android 字節(jié)碼優(yōu)化工具ReDex 中大多數(shù)的優(yōu)化環(huán)節(jié)提供了分析引擎.

Mopsa[90]是一個基于抽象解釋的靜態(tài)分析通用框架.Mopsa 致力于通過模塊化抽象，能夠一次只對軟件中的某個組件進行分析，從而在不降低精度的同時提升軟件分析的效率.Mopsa 支持不同的迭代器和抽象，并能夠支持不同類型語言的分析，尤其是支持動態(tài)類型語言Python 的分析，這也是其近期研究的主要關(guān)注點[116-118].

MemCAD[91]是開源的形態(tài)分析工具，主要用于分析、驗證程序的內(nèi)存使用相關(guān)性質(zhì)，特別是鏈表和樹等動態(tài)結(jié)構(gòu)相關(guān)斷言的驗證.用戶可以針對數(shù)據(jù)結(jié)構(gòu)的描述來參數(shù)化選擇工具使用的抽象域.

Interproc[92]是一個開源的抽象解釋工具，可分析得到一種自定義的簡單命令式語言SPL 編寫的程序并得到數(shù)值變量的數(shù)值不變式.Interproc 支持包含遞歸在內(nèi)的過程間分析[119].Interproc 由前端、開源的不動點求解庫、開源抽象域庫Apron 3 部分組成.

CodeHawk[92]是一個基于抽象解釋的靜態(tài)分析工具，由Kestrel Technology 公司開發(fā)并開源[94].其基于一種自 定義的 中間語言CHIF（CodeHawk internal form）實現(xiàn)了一個與目標程序語言相獨立的抽象解釋引擎，能夠支持C、Java 字節(jié)碼和二進制程序等3 種不同語言程序的分析.該抽象解釋引擎包含了高效的迭代分析器，以及值集合、污點、多面體和區(qū)間等多種抽象域.CodeHawk 還通過分而治之的方法實現(xiàn)對大規(guī)模程序的分析[94].

總體而言，基于抽象解釋的程序分析工具在最近幾年的進展體現(xiàn)了3 個趨勢：1）關(guān)注分析規(guī)模和效率的提升.利用并行計算、內(nèi)存優(yōu)化、機器學(xué)習(xí)等技術(shù)，提升程序分析工具的性能.2）多語言支持.大部分傳統(tǒng)的分析工具只支持C 程序分析，而最近抽象解釋工具增加了對并發(fā)程序，以及Java、Python 和二進制等程序分析的支持.3）與軟件開發(fā)過程聯(lián)系更加緊密.不同于傳統(tǒng)的全程序分析，通過增量式分析、交互式分析和需求驅(qū)動分析，抽象解釋分析工具能更好地適應(yīng)軟件迭代式開發(fā)、增量式演化等特點，以更好融入軟件生產(chǎn)開發(fā)的全過程.此外，程序分析誤報的消除也能進一步提升軟件開發(fā)人員的使用友好度.

3 基于抽象解釋的可信人工智能

本節(jié)主要介紹抽象解釋在人工智能可信保證中的應(yīng)用及其進展.

3.1 神經(jīng)網(wǎng)絡(luò)模型驗證

近年來，深度神經(jīng)網(wǎng)絡(luò)（deep neural network,DNN）被廣泛應(yīng)用于安全攸關(guān)領(lǐng)域，包括自動駕駛系統(tǒng)、醫(yī)療診斷系統(tǒng)、飛行器防碰撞系統(tǒng)等.在此類系統(tǒng)中，可信性質(zhì)被違背可能帶來嚴重后果.如何確保神經(jīng)網(wǎng)絡(luò)系統(tǒng)的高可信性已成為人工智能技術(shù)在安全攸關(guān)領(lǐng)域廣泛應(yīng)用所面臨的問題.神經(jīng)網(wǎng)絡(luò)驗證是檢驗和提高神經(jīng)網(wǎng)絡(luò)可信性的重要手段.

神經(jīng)網(wǎng)絡(luò)可以看作是一類程序，因此可基于面向程序的形式化分析與驗證技術(shù)研究其可信性.但神經(jīng)網(wǎng)絡(luò)又有其特殊性.例如，輸入一般是高維的，且激活函數(shù)是非線性的，實際應(yīng)用中神經(jīng)網(wǎng)絡(luò)包含的神經(jīng)元數(shù)量往往非常龐大，故對神經(jīng)網(wǎng)絡(luò)進行精確推理代價很大.抽象解釋技術(shù)通過對神經(jīng)網(wǎng)絡(luò)的具體語義進行抽象，使其能夠在抽象語義上實現(xiàn)更加高效的推理.2018 年，Gehr 等人[120]提出了基于抽象解釋的神經(jīng)網(wǎng)絡(luò)驗證框架AI2，首次將抽象解釋技術(shù)應(yīng)用于神經(jīng)網(wǎng)絡(luò)的安全性和魯棒性驗證；使用帶條件的仿射函數(shù)實現(xiàn)對ReLU 激活函數(shù)的抽象建模，在此基礎(chǔ)上實現(xiàn)了面向神經(jīng)網(wǎng)絡(luò)驗證的區(qū)間和Zonotope 及其冪集抽象域.此后，基于抽象解釋的神經(jīng)網(wǎng)絡(luò)驗證技術(shù)不斷涌現(xiàn).也有不少綜述[121-123]介紹了基于抽象解釋的神經(jīng)網(wǎng)絡(luò)驗證方面的工作.2021年，Albarghouthi[124]詳細介紹了基于抽象解釋技術(shù)開展神經(jīng)網(wǎng)絡(luò)驗證的典型算法和前沿工作.在神經(jīng)網(wǎng)絡(luò)驗證領(lǐng)域，抽象域設(shè)計尤為重要，目前廣泛使用的抽象域包括區(qū)間抽象域、Zonotope 抽象域和多面體抽象域等，它們有效實現(xiàn)了精度和效率的合理折衷.

3.1.1 基于區(qū)間抽象域的驗證

在神經(jīng)網(wǎng)絡(luò)驗證領(lǐng)域，區(qū)間抽象域技術(shù)在很多文獻中被稱為區(qū)間界傳播（interval bound propagation,IBP）[125]或區(qū)間分析（interval analysis）.Mirman 等人[126]將區(qū)間抽象域、區(qū)間界傳播、區(qū)間分析等概念視為等價的，它們本質(zhì)上都是抽象解釋框架下的一種基于區(qū)間算術(shù)的抽象推導(dǎo)方式.為此，本文在描述上也不對這些概念進行刻意區(qū)分.此外需要說明的是，在程序分析領(lǐng)域，區(qū)間抽象域中的區(qū)間上界和下界一般是具體的實數(shù)，而在神經(jīng)網(wǎng)絡(luò)分析中，上界和下界可能是符號表達式(即符號區(qū)間)，此時的符號區(qū)間實質(zhì)上表示的是一個多面體抽象域，但當它基于輸入值范圍進行具體化后又會得到一個值區(qū)間，故又可稱為區(qū)間抽象域.

區(qū)間分析最早在AI2中被用于神經(jīng)網(wǎng)絡(luò)驗證[120].隨后，Wang 等人[127]針對ReLU 神經(jīng)網(wǎng)絡(luò)提出了基于符號化區(qū)間的神經(jīng)網(wǎng)絡(luò)形式化驗證技術(shù)，其主要思想是為每個神經(jīng)元維持一個關(guān)于輸入變量的符號區(qū)間，并逐層向后傳播，當利用符號區(qū)間計算得到的神經(jīng)元（執(zhí)行激活函數(shù)前）取值范圍包含0 時（即無法確定神經(jīng)元激活狀態(tài)），則用值區(qū)間替換符號區(qū)間繼續(xù)向后傳播，直至得到輸出層的符號區(qū)間和值區(qū)間信息，并據(jù)此判斷待驗證性質(zhì)是否成立.在逐層向后傳播過程中，用具體值區(qū)間替換符號區(qū)間時會丟失神經(jīng)元之間的依賴關(guān)系，從而造成輸出層神經(jīng)元的計算精度大量損失，可能導(dǎo)致性質(zhì)無法得到有效驗證.Wang 等人[128]對這一方法進行了改進，提出了基于線性松弛的符號化區(qū)間分析技術(shù)，其主要思想是為每個神經(jīng)元維護2 個符號區(qū)間，一個記錄激活函數(shù)處理之前的符號界信息，另一個記錄激活函數(shù)處理之后的符號界信息.當神經(jīng)元激活狀態(tài)確定為激活或非激活狀態(tài)時，激活函數(shù)之后的符號界信息可以精確得到；否則需要利用線性松弛技術(shù)（基于激活函數(shù)之前的神經(jīng)元符號界和值范圍信息）近似計算激活函數(shù)之后的符號界信息.這種傳播方式既能夠有效維護神經(jīng)元之間的部分依賴關(guān)系，又能避免精確傳播帶來的組合爆炸問題，取得了更好的驗證效果.Yin 等人[129]提出一個更精細的抽象域，在抽象表示上為每個神經(jīng)元維護2 個符號區(qū)間、1 個值區(qū)間和1 個激活狀態(tài)變量（可能取值是激活、非激活或不確定），在此基礎(chǔ)上還在每遍抽象分析過程中顯式記錄一組輸入變量必須滿足的線性約束；在抽象遷移上，針對神經(jīng)元激活函數(shù)狀態(tài)非確定情形，提出了一種新的線性松弛技術(shù)，它能保證該神經(jīng)元抽象傳播過程中精度損失的面積達到最小，實驗表明該抽象域在單遍分析精度以及基于分支限界（B&B）的迭代驗證框架中均表現(xiàn)出了明顯優(yōu)勢.

盡管抽象解釋技術(shù)由于抽象帶來的精度損失可能導(dǎo)致很多性質(zhì)無法驗證，但在神經(jīng)網(wǎng)絡(luò)驗證實踐中依然 取得了 很好的效果.Baader 等 人[130]、Wang 等人[131]從理論層面分析了其中的原因，他們一般化描述了神經(jīng)網(wǎng)絡(luò)的通用近似（universal approximation）性質(zhì)，并將其應(yīng)用于基于區(qū)間抽象域或者其他更精確抽象域的神經(jīng)網(wǎng)絡(luò)驗證.具體而言，假定某個神經(jīng)網(wǎng)絡(luò)在給定輸入?yún)^(qū)域內(nèi)是魯棒的，但基于區(qū)間抽象域卻無法驗證其魯棒性時，Wang 等人[131]證明總能基于現(xiàn)有激活函數(shù)（ReLU，Sigmoid 等）構(gòu)造一個新的神經(jīng)網(wǎng)絡(luò)，該網(wǎng)絡(luò)可以在語義上按照需要無限接近于原來的神經(jīng)網(wǎng)絡(luò)，同時可以基于抽象解釋技術(shù)驗證這一新構(gòu)建的神經(jīng)網(wǎng)絡(luò)在給定區(qū)域內(nèi)是魯棒的，從而在理論上證明了抽象解釋技術(shù)可以驗證任何神經(jīng)網(wǎng)絡(luò)的性質(zhì).但文獻[131]中同時也指出構(gòu)建新神經(jīng)網(wǎng)絡(luò)的復(fù)雜度在最壞情況下可能是NP 難的.Mirman 等人[126]也進行了理論分析，指出區(qū)間分析在驗證分類神經(jīng)網(wǎng)絡(luò)的魯棒性上是存在局限性的，并通過定理證明了并不是所有的神經(jīng)網(wǎng)絡(luò)都能夠通過構(gòu)造不可逆函數(shù)實現(xiàn)精確的區(qū)間分析.鑒于此，文獻[126]中進一步推導(dǎo)出一個悖論：即使所有數(shù)據(jù)集都可以進行魯棒分類，但仍然存在一些簡單的數(shù)據(jù)集不能用區(qū)間分析來證明其分類的魯棒性.這些研究從理論層面分析了抽象解釋框架（特別是區(qū)間分析）的可用性和存在的一些局限性，對深入研究可信神經(jīng)網(wǎng)絡(luò)具有重要意義.

3.1.2 基于Zonotope 抽象域的驗證

Gehr 等人[120]在AI2中將Zonotope 抽象域引入到神經(jīng)網(wǎng)絡(luò)驗證領(lǐng)域.而后，Singh 等人[132]專門針對ReLU，Tanh，Sigmoid 激活函數(shù)重新設(shè)計了基于逐點傳播的Zonotope 抽象遷移操作，有效減小了Zonotope投影到二維平面上的面積，從而提高了分析精度.基于重新設(shè)計的Zonotope 抽象域，開發(fā)了既支持串行遷移計算又支持并行遷移計算的神經(jīng)網(wǎng)絡(luò)驗證系統(tǒng)DeepZ，并在MNIST 和CIFAR10 等數(shù)據(jù)集上開展實驗，驗證包含8 萬多個神經(jīng)元的神經(jīng)網(wǎng)絡(luò)的魯棒性.實驗結(jié)果表明DeepZ 相比之前的工作取得了更精確且更高效的驗證效果.

為了進一步提高驗證精度，Singh 等人[133]提出了一種基于精化的神經(jīng)網(wǎng)絡(luò)魯棒性驗證方法，其主要思想是充分利用抽象解釋方法的高效性，以及混合整數(shù)線性規(guī)劃和整數(shù)規(guī)劃松弛技術(shù)的高精度，并采用啟發(fā)式策略選取在抽象解釋的上近似分析（如基于Zonotope 抽象域）過程中精度損失較大的神經(jīng)元，對于這些神經(jīng)元再利用整數(shù)線性規(guī)劃和松弛技術(shù)計算更加精確的符號和值范圍.基于該方法，實現(xiàn)了一個支持完備神經(jīng)網(wǎng)絡(luò)驗證的工具RefineZono.實驗結(jié)果表明，對于大規(guī)模神經(jīng)網(wǎng)絡(luò)，RefineZone 相比其他不完備驗證工具擁有更高的精度；而對于小規(guī)模神經(jīng)網(wǎng)絡(luò)，在保證驗證完備性的情況下，RefineZone 相比其他完備驗證工具表現(xiàn)得更加高效.

最近，Jordan 等人[134]基于Zonotope 抽象域設(shè)計了一種新穎的算法ZonoDual.ZonoDual 有效結(jié)合了基于抽象域和基于最優(yōu)化技術(shù)2 種方法來計算界信息，具有的特點為：具有高度可擴展性并且適合GPU加速；結(jié)合后的方法比單一使用某種方法能夠獲得更精確的界信息；方法具有高度可調(diào)節(jié)性，可以有效實現(xiàn)精度和計算效率的折衷；可作為一個附加組件加入到已有的對偶驗證框架中來進一步提高其性能.在MNIST 和CIFAR10 等數(shù)據(jù)集上的實驗表明，ZonoDual 算法在精度和效率方面都優(yōu)于線性松弛技術(shù)，并且產(chǎn)生了比以前的對偶方法更精確的界信息.

3.1.3 基于多面體抽象域的驗證

Singh 等人[135]將多面體抽象域應(yīng)用于神經(jīng)網(wǎng)絡(luò)驗證，設(shè)計了一種新的抽象域表示，即針對每個神經(jīng)元分別維護1 個符號區(qū)間和1 個值區(qū)間，提出了新的抽象遷移函數(shù)處理仿射轉(zhuǎn)換、ReLU、Sigmoid、Tanh、Maxpool 等神經(jīng)網(wǎng)絡(luò)中的常見算子.此外，還基于多面體抽象域?qū)崿F(xiàn)了一個驗證工具DeepPoly，并在MNIST和CIFAR10 數(shù)據(jù)集上開展實驗，結(jié)果表明DeepPoly能夠有效驗證卷積神經(jīng)網(wǎng)絡(luò)在無窮范數(shù)和旋轉(zhuǎn)擾動下的魯棒性.Tran 等人[136]提出了一種稱之為ImageStars的卷積神經(jīng)網(wǎng)絡(luò)集合表示方法，其實質(zhì)上是多面體抽象域的另外一種刻畫方式，文獻[136]將ImageStars應(yīng)用于基于集合的分析框架中，并分別設(shè)計算法實現(xiàn)卷積層、全連接層、最大池化層、平均池化層可達狀態(tài)的精確和上近似計算.進一步基于該可達性分析算法實現(xiàn)了神經(jīng)網(wǎng)絡(luò)驗證工具NNV，并在實際中廣泛使用的卷積神經(jīng)網(wǎng)絡(luò)VCG 上開展實驗.結(jié)果表明NNV 工具相比DeepPoly 能夠更好驗證VCG 在對抗攻擊（如DeepFool 攻擊）下的魯棒性.Goubault 等人[137]結(jié)合基于集合的方法和抽象解釋技術(shù)，提出了一種使用Tropical 多面體抽象ReLU 前饋神經(jīng)網(wǎng)絡(luò)的方法.文獻[137]中闡述了Tropical 多面體可以有效地抽象ReLU 激活函數(shù)，同時又能夠較好控制由于線性計算而導(dǎo)致的精度損失.

為了實現(xiàn)更大規(guī)模神經(jīng)網(wǎng)絡(luò)的驗證，Müller 等人[138]在GPU 上設(shè)計了面向神經(jīng)網(wǎng)絡(luò)驗證的通用、可靠的多面體抽象域的算法.該算法充分利用了GPU 的并行處理能力以及神經(jīng)網(wǎng)絡(luò)驗證問題固有的稀疏性，并在此基礎(chǔ)上實現(xiàn)了一個可擴展性高的基于多面體抽象域的并行驗證工具GPUPoly.實驗表明GPUPoly能夠在34.5ms 時間內(nèi)驗證包含30 多個隱含層、上百萬個神經(jīng)元的深度殘差網(wǎng)絡(luò)的魯棒性，使得抽象解釋技術(shù)朝驗證現(xiàn)實世界超大規(guī)模人工智能系統(tǒng)邁出關(guān)鍵的一步.

大部分非完備的驗證技術(shù)都是基于單個神經(jīng)元的凸抽象，即對隱含層的每個神經(jīng)元的抽象都是單獨進行的，對該隱含層的抽象則是每個神經(jīng)元抽象結(jié)果的并，在幾何上即每個神經(jīng)元的凸閉包的笛卡爾乘積.從單個神經(jīng)網(wǎng)絡(luò)隱含層抽象角度來看，這種抽象方式精度顯然會低于該隱含層的最優(yōu)凸閉包，更重要的是它忽略了同層神經(jīng)元之間的依賴關(guān)系，且這種抽象方式的精度損失會在神經(jīng)網(wǎng)絡(luò)逐層推導(dǎo)過程中被不斷放大，從而導(dǎo)致輸出層的分析精度十分受限.Salman 等人[139]闡明了單個神經(jīng)元凸抽象的固有局限.為了消除該局限，有工作[140]針對ReLU 網(wǎng)絡(luò)提出了多神經(jīng)元抽象技術(shù)，相比單個神經(jīng)元的凸抽象，其精度更高；而相比最優(yōu)凸閉包，它又具有更好的可擴展性，因此可看作最優(yōu)凸閉包和單個神經(jīng)元凸抽象的一個折衷方案.

Singh 等人[137,140]提出了k-Poly 的方法，其要思想是將隱含層的神經(jīng)元劃分為若干個（集合元素數(shù)目小于等于5）小集合，再將每個小集合的神經(jīng)元分為若干個組，每組神經(jīng)元數(shù)量不超過k個（k≤3），對于每組神經(jīng)元通過八面體[141]（octahedra）抽象域來對其輸入進行刻畫，在此基礎(chǔ)上聯(lián)合計算該組k個神經(jīng)元的最優(yōu)凸閉包輸出.最優(yōu)凸閉包的計算代價非常高，并且會產(chǎn)生復(fù)雜的輸出約束，因此只會應(yīng)用在少數(shù)幾個互不相交的神經(jīng)元組上，這就限制了該方法能夠維持的同層神經(jīng)元之間的依賴關(guān)系數(shù)量.

Tjandraatmadja 等人[142]和Palma 等人[143]在考慮隱含層的輸入時，將激活函數(shù)與激活函數(shù)之前的仿射層合并得到一個多維激活層，并計算多維激活層的凸近似，以得到該隱含層的一個超盒（hyperbox）近似.這種粗略的輸入抽象一定程度上緩解了只在單個仿射層上進行近似的缺陷.實驗表明，文獻[142-143]的方法都取得了較好的精度提升，但它們僅限于ReLU 激活并且缺乏可擴展性，原因是需要精確計算少量神經(jīng)元的最優(yōu)凸閉包或者大量神經(jīng)元的較優(yōu)凸閉包.此外，它們也沒有解決如何在層內(nèi)獲取足夠的神經(jīng)元相互依賴關(guān)系以盡可能接近最優(yōu)凸抽象的問題.針對這些問題，Müller 等人[144]提出了PRIMA驗證框架，它能處理包含ReLU，Sigmoid，Tanh，MaxPool等多種激活函數(shù)的神經(jīng)網(wǎng)絡(luò).PRIMA 是建立在k-Poly基礎(chǔ)上的，它通過考慮大量相對較小的重疊神經(jīng)元組，獲得神經(jīng)元之間的大多數(shù)相互依賴關(guān)系.雖然它沒有達到最優(yōu)凸閉包的精確程度，但相比以往的抽象技術(shù)，PRIMA 在逐層推導(dǎo)過程中獲得了顯著的精度提升.實驗表明，PRIMA 在自動駕駛領(lǐng)域的真實神經(jīng)網(wǎng)絡(luò)上實現(xiàn)了精確驗證，而且時間開銷控制在幾分鐘以內(nèi).

3.1.4 結(jié)合抽象解釋的驗證精化

抽象解釋在上近似過程中會引入精度損失，從而可能導(dǎo)致分析結(jié)果精度不足以支撐神經(jīng)網(wǎng)絡(luò)性質(zhì)的驗證.Li 等人[145]和Yang 等人[146]研究提出了一種基于符號傳播的方法來提高基于抽象解釋的神經(jīng)網(wǎng)絡(luò)驗證的精確性，并將精化后的神經(jīng)元的邊界值信息用于提高基于SMT 的神經(jīng)網(wǎng)絡(luò)驗證方法（如Reluplex）的性能.Elboher 等人[147]提出類似反例制導(dǎo)抽象精化（CEGAR）的神經(jīng)網(wǎng)絡(luò)迭代驗證技術(shù)，其主要思想是將神經(jīng)網(wǎng)絡(luò)進行可靠抽象得到一個較小規(guī)模的網(wǎng)絡(luò)，并在該網(wǎng)絡(luò)上進行性質(zhì)驗證，如果性質(zhì)成立則終止驗證；否則生成一個反例，用于指導(dǎo)神經(jīng)網(wǎng)絡(luò)抽象，從而得到一個更大的、更接近于原始網(wǎng)絡(luò)的新網(wǎng)絡(luò)，并在新網(wǎng)絡(luò)上重新展開驗證.

另一個主流的精化方式是將抽象解釋分析技術(shù)與基于搜索或最優(yōu)化的技術(shù)相結(jié)合[148-151]，從而實現(xiàn)更加精確的驗證，更多相關(guān)工作請參見綜述文獻[121].本文重點介紹基于分支限界（branch and bound,B&B）方法，它也是一種結(jié)合搜索和抽象分析的通用迭代驗證框架[152-153].該框架包括2 個關(guān)鍵過程，即Branch 過程 和Bound 過程.Bound 過程是 指通過分析獲取神經(jīng)網(wǎng)絡(luò)各個隱含層和輸出層神經(jīng)元的界信息，快速判斷待驗證性質(zhì)是否成立.為了保證整個驗證框架能夠高效工作，界信息的獲取通常在抽象語義下（如基于抽象解釋、區(qū)間傳播、線性松弛等技術(shù)構(gòu)建神經(jīng)網(wǎng)絡(luò)的上近似抽象）進行，以盡量提高每遍Bound 過程的效率.Branch 過程是指當Bound 過程產(chǎn)生的界信息尚不足以驗證其性質(zhì)時，通過劃分技術(shù)，將原來較難驗證的問題分解為若干更易于驗證的子問題，針對每個子問題再通過Bound 過程判斷性質(zhì)是否成立.如果所有子問題都得到成功驗證，則說明待驗證性質(zhì)成立；否則如果在某個子問題中找到反例，則說明待驗證性質(zhì)不成立.B&B 框架提供了一個思路，使得原本不完備的抽象解釋技術(shù)能夠?qū)崿F(xiàn)完備的神經(jīng)網(wǎng)絡(luò)驗證.事實上，當前不少工作[154-156]都可以歸結(jié)為B&B 框架的一個應(yīng)用，只是設(shè)計了不同Bound 算法和Branch 算法.Wang 在文獻[157]中系統(tǒng)介紹了B&B 技術(shù)在神經(jīng)網(wǎng)絡(luò)驗證領(lǐng)域取得的主要進展.

這里重點介紹3 個工具，即ReluVal[127]，Neurify[128]和LayerSAR[129].這3 個工具都在B&B 框架下實現(xiàn)更加完備的驗證，其主要思想都是利用了抽象解釋技術(shù)計算抽象可達狀態(tài)集合（即Bound 過程），并同時采用基于輸入域劃分的迭代技術(shù)（即Branch 過程）不斷精化抽象可達狀態(tài)集合，從而最終達到驗證性質(zhì)的目的.具體而言，ReluVal[127]采用了基于二分法的輸入域劃分技術(shù)，即直接在輸入空間上啟發(fā)式選取1 個輸入變量，再對該變量的區(qū)間值范圍進行均勻二分，從而得到2 個子輸入空間，再針對每個子空間開展迭代抽象驗證，文獻[127]基于利普希茨連續(xù)性定理證明了二分法在理論上是完備.基于二分法對輸入域劃分的優(yōu)點是操作簡單、易于實現(xiàn)，但缺點也十分明顯，即劃分的目的不清晰、具有盲目性，從而導(dǎo)致提升驗證效率的效果不佳.為了克服這些不足，Neurify[128]結(jié)合了符號化線性松弛技術(shù)和基于中間層神經(jīng)元的輸入域劃分技術(shù).其劃分神經(jīng)元的選取策略是在預(yù)分析階段基于梯度分析技術(shù)反向推導(dǎo)每個隱含層神經(jīng)元對性質(zhì)驗證的影響程度，在迭代階段則根據(jù)分析結(jié)果依次選取影響程度更大神經(jīng)元作為劃分對象.Neurify 在一定程度上提高了驗證效率，但由于劃分神經(jīng)元可能來自任意隱含層，故在前向抽象分析得到的符號上下界可能不相等.由此帶來的問題是當每個神經(jīng)元最多被劃分1 次時（Neurify 工具在實現(xiàn)上基于如此假設(shè)），它的劃分技術(shù)不能保證該驗證方法能夠經(jīng)過有窮迭代后得出完備的驗證結(jié)論.針對Neurify 可能不完備的問題，LayerSAR[129]提出了基于非確定首層（FUL）的劃分策略.FUL 是指從（輸入層到輸出層）逐層抽象分析過程中首個包含神經(jīng)元激活函數(shù)狀態(tài)非確定的隱含層.FUL 層神經(jīng)元具有的性質(zhì)為符號上界和符號下界總是相等的.故在劃分后得到的2 個子驗證問題中劃分神經(jīng)元的激活狀態(tài)都會變得確定化，從而能夠證明每個神經(jīng)元至多劃分1 次即能驗證性質(zhì)成立.此外，LayerSAR 進一步利用劃分謂詞對輸入域進行精化，從而進一步提升單遍抽象解釋分析精度.

3.1.5 在RNN 驗證上的應(yīng)用

3.1.1～3.1.4 節(jié)所述的基于抽象解釋的神經(jīng)網(wǎng)絡(luò)驗證工作大多聚焦于檢驗全連接前饋神經(jīng)網(wǎng)絡(luò)（FFNN）和卷積神經(jīng)網(wǎng)絡(luò)（CNN）的安全性和魯棒性等可信性質(zhì).近年來，隨著形式化方法逐步應(yīng)用于循環(huán)神經(jīng)網(wǎng)絡(luò)（RNN）的驗證[158-164]，抽象解釋技術(shù)也發(fā)揮了越來越重要的作用[158,160,162].

Zhang 等人[158]在深入分析并定義認知領(lǐng)域RNN需要驗證的重要性質(zhì)的基礎(chǔ)上，提出了一種新的RNN 性質(zhì)驗證方法.該方法主要包括2 個階段：一是改進“易于驗證的網(wǎng)絡(luò)”范式，并用于訓(xùn)練循環(huán)網(wǎng)絡(luò)；二是結(jié)合混合多面體傳播、多面體不變式生成和反例制導(dǎo)的抽象精化等技術(shù)進行RNN 性質(zhì)驗證.在上述驗證過程中，應(yīng)用了抽象解釋框架下凸多面體有窮冪集抽象域，并設(shè)計了專門處理多面體的凸閉包的抽象函數(shù)和降低凸閉包精度損失的精化函數(shù)，以解決具體語義下可達性分析中多面體數(shù)量呈指數(shù)增長的問題，以及如何獲得足夠的抽象分析精度來證明所需驗證的性質(zhì)等.實驗結(jié)果表明，該工作中采用的技術(shù)為應(yīng)對這些挑戰(zhàn)提供了可行的解決方案.

Akintunde 等人[159]和Jacoby[160]等人分別采用不同的方法將RNN 驗證問題轉(zhuǎn)化為FFNN 驗證問題，再借助已有的包括基于抽象解釋技術(shù)在內(nèi)的任意形式化驗證工具對轉(zhuǎn)換之后的FFNN 開展驗證.這些方法不同之處在于文獻[159]采用的轉(zhuǎn)換過程是對RNN 進行有窮次復(fù)制（類似于程序分析中的循環(huán)展開技術(shù)），故最終實現(xiàn)的是一種不可靠（unsound）的部分驗證；而文獻[160]的轉(zhuǎn)換過程采用了一種基于不變式的上近似技術(shù)（類似于抽象解釋技術(shù)處理程序中的循環(huán)），其核心思想是把RNN 傳播過程中上一時刻的記憶單元值使用含時間變量t的線性歸納不變式（實質(zhì)是一個符號區(qū)間約束）進行可靠抽象，從而避免了RNN 展開技術(shù)導(dǎo)致的網(wǎng)絡(luò)規(guī)模急劇增大的問題.當經(jīng)過抽象的FFNN 不足以驗證原來性質(zhì)時，可通過精化關(guān)于t的線性歸納不變式進行不斷迭代，最終實現(xiàn)高效可靠的RNN 神經(jīng)網(wǎng)絡(luò)驗證.

Ryou 等人[162]實現(xiàn)了一個可擴展的、高精度的遞歸神經(jīng)網(wǎng)絡(luò)驗證工具Prover，其主要思想為：結(jié)合采樣技術(shù)、優(yōu)化技術(shù)和費馬定理，設(shè)計一系列多面體抽象方法，以計算非凸和非線性的遞歸更新函數(shù)；提出了一種基于梯度下降的抽象精化算法，該算法針對待驗證的性質(zhì)，結(jié)合了每個神經(jīng)元的多種抽象方式.基于Prover，文獻[162]中研究了語音識別領(lǐng)域RNN非平凡應(yīng)用實例的驗證問題，并設(shè)計實現(xiàn)了非線性語音預(yù)處理管道的自定義抽象方法.實驗表明，Prover 能夠成功驗證計算機視覺、語音和運動傳感器數(shù)據(jù)分類和識別中若干個極具挑戰(zhàn)性的，且在此之前的工作都未能處理的RNN 網(wǎng)絡(luò)模型.

3.2 神經(jīng)網(wǎng)絡(luò)模型魯棒訓(xùn)練

神經(jīng)網(wǎng)絡(luò)可信性驗證總是假定待驗證的神經(jīng)網(wǎng)絡(luò)是已經(jīng)訓(xùn)練好的，而神經(jīng)網(wǎng)絡(luò)的可信訓(xùn)練則是研究如何在神經(jīng)網(wǎng)絡(luò)訓(xùn)練過程中針對特定屬性提高其可信性.目前，有不少研究工作都使用抽象解釋技術(shù)訓(xùn)練更魯棒的神經(jīng)網(wǎng)絡(luò).實踐證明，基于抽象解釋訓(xùn)練得到的神經(jīng)網(wǎng)絡(luò)在對抗擾動攻擊上表現(xiàn)出了更好的魯棒性，反過來這種魯棒性也更易于通過抽象解釋技術(shù)得到驗證.

Mirman 等人[165]和Gowal 等人[166]最早于2018 年將抽象解釋應(yīng)用于神經(jīng)網(wǎng)絡(luò)訓(xùn)練過程.文獻[165]提出了可微抽象解釋（differentiable abstract interpretation）技術(shù)用于訓(xùn)練大規(guī)模神經(jīng)網(wǎng)絡(luò)，從而保證訓(xùn)練出來的神經(jīng)網(wǎng)絡(luò)總是滿足某些魯棒性質(zhì).在此基礎(chǔ)上，F(xiàn)ischer 等人[167]提出了一種面向深度學(xué)習(xí)的可微邏輯（differentiable logic），開發(fā)了系統(tǒng)DL2，并在無監(jiān)督學(xué)習(xí)、半監(jiān)督學(xué)習(xí)、有監(jiān)督學(xué)習(xí)等場景下的神經(jīng)網(wǎng)絡(luò)可信訓(xùn)練上取得了較好效果.

此外，還有很多研究使用抽象解釋技術(shù)訓(xùn)練更加魯棒的圖形識別和自然語言處理神經(jīng)網(wǎng)絡(luò)模型[168-172].文獻[168]提出了一種通用語言，用于刻畫與自然語言處理相關(guān)的可編程字符串操作（例如插入、刪除、替換、交換等）.在此基礎(chǔ)上，提出了一種對抗訓(xùn)練神經(jīng)網(wǎng)絡(luò)模型的方法A3T，使得訓(xùn)練得到的模型關(guān)于用戶指定的字符串操作是魯棒的.A3T 充分結(jié)合了基于搜索的對抗性訓(xùn)練技術(shù)和基于上近似的抽象技術(shù)各自的優(yōu)勢.具體而言，文獻[168]中介紹了如何將一組用戶自定義的字符串操作分解為2 個組件規(guī)約，一個能夠受益于搜索技術(shù)，另一個能夠受益于抽象技術(shù).使用A3T 在AG 和SST2 數(shù)據(jù)集上訓(xùn)練模型的實驗結(jié)果表明，A3T 生成的模型對于用戶自定義的模仿拼寫錯誤和其他保留含義的操作都是魯棒的.

文獻[169]提出了一種用于訓(xùn)練魯棒RNN 的方法ARC，并在LSTMs，BiLSTMs 和TreeLSTMs 等模型上展示了ARC 的有效性.ARC 是抽象解釋技術(shù)的一個新的應(yīng)用，以符號化方式刻畫以編程方式定義的字符串集合，并通過RNN 進行傳播.實驗結(jié)果表明，相較于此前技術(shù)，ARC 訓(xùn)練出的模型對于任意空間擾動表現(xiàn)出更好魯棒性.此外，ARC 能夠證明給定神經(jīng)網(wǎng)絡(luò)模型關(guān)于某些攻擊操作是魯棒的，而此前技術(shù)很難做到這一點.

3.3 深度學(xué)習(xí)程序的分析

深度學(xué)習(xí)程序中含有大量的數(shù)值操作，因此難以通過測試的方法遍歷所有的程序狀態(tài)以檢測出所有的程序缺陷.而靜態(tài)分析能夠考慮程序所有可能的狀態(tài)空間，從而可以分析驗證深度學(xué)習(xí)程序的可靠安全性.

不同于模型層面的神經(jīng)網(wǎng)絡(luò)驗證方法，面向神經(jīng)網(wǎng)絡(luò)框架（如TensorFlow 編寫的程序）的分析方法能夠在模型訓(xùn)練前分析檢測程序可能存在的缺陷.Zhang 等人[173]提出了一種神經(jīng)網(wǎng)絡(luò)框架層面的基于抽象解釋的數(shù)值缺陷檢測分析方法.該方法對神經(jīng)網(wǎng)絡(luò)架構(gòu)分析時基于2 種抽象：一是張量抽象，二是數(shù)值變量的區(qū)間范圍抽象.同時，其還通過張量劃分和仿射等式關(guān)系抽象技術(shù)，在保證分析效率的同時提升分析精度.

4 抽象解釋的其他典型應(yīng)用

本節(jié)主要介紹抽象解釋在其他方面的典型應(yīng)用及其進展.

4.1 智能合約可信保證

以太坊智能合約的執(zhí)行需要消耗gas.在智能合約部署運行前，通過靜態(tài)分析的方法提前預(yù)估合約可能的gas 資源使用量峰值，有助于避免經(jīng)濟損失.為此，Pérez 等人[174]提出了一種基于抽象解釋的參數(shù)化資源分析方法.此外，Grech 等人[175]提出了一種gas 泄漏檢測方法，結(jié)合基于控制流分析的反匯編和聲明式程序結(jié)構(gòu)查詢技術(shù)，在EVM 字節(jié)碼上使用抽象解釋進行分析，并設(shè)計實現(xiàn)了工具MadMax.

由于智能合約一旦部署便難以修補漏洞，因而對智能合約的安全性進行驗證具有重要意義.Kalra等人[176]利用抽象解釋、符號模型檢驗和帶約束霍恩子句（constrained Horn clauses,CHC）的結(jié)合來快速驗證合約的安全性，并構(gòu)建了ZEUS 驗證平臺.文獻[176]提出了Solidity 智能合約執(zhí)行語義的形式化抽象，計算數(shù)據(jù)域上的循環(huán)和函數(shù)摘要，從而減少模型檢驗階段的狀態(tài)空間.ZEUS 對超過22.4 萬個智能合約進行了評估，其誤報率較低且沒有漏報.

4.2 信息安全保證

在信息流安全無干擾性分析方面，Giacobazzi 等人[177-179]基于抽象解釋引入了抽象無干擾性（abstract non-interference）的概念作為無干擾性概念的一般化.文獻[177-179]指出抽象無干擾性是參數(shù)化的，以人們要保護哪些隱私信息、外部觀察者可觀察信息為參數(shù)，并指出可在標準的抽象解釋框架內(nèi)對抽象無干擾性進行刻畫，使得程序的安全程度成為程序語義的屬性.最近，Mastroeni 等人[179]設(shè)計了一個基于抽象解釋的靜態(tài)分析器，以可靠地檢查無干擾性.文獻[179]定義了一個超抽象域用于分析超性質(zhì)（hyperproperty），它能夠?qū)Ρ环治龀绦蛑谐霈F(xiàn)的信息流進行近似.

針對Cache 側(cè)信道泄漏問題，K?pf 等人[180]提出了一種基于抽象解釋的量化方法，它通過靜態(tài)Cache分析技術(shù)實現(xiàn)對抽象Cache 狀態(tài)具體化后具體狀態(tài)的計數(shù)，將靜態(tài)Cache 分析與定量信息流分析結(jié)合，從而自動推導(dǎo)出攻擊者通過觀察CPU Cache 性能的方式從程序中提取關(guān)于輸入信息量的上界.Doychev、K?pf 等人[181]還進一步開發(fā)了針對Cache 側(cè)信道攻擊的具有形式化且量化安全保證的開源靜態(tài)分析工具CacheAudit，通過抽象計算攻擊者可能的側(cè)信道觀測信息的精確上近似.Barthe、K?pf 等人[182]在此基礎(chǔ)上將CacheAudit 應(yīng)用于并發(fā)環(huán)境下的內(nèi)存?zhèn)刃诺腊踩ＷC中.Doychev 和K?pf[183]進一步支持了動態(tài)內(nèi)存分配環(huán)境下內(nèi)存訪問的位級推理和算術(shù)推理，使得能夠針對可執(zhí)行代碼側(cè)信道攻擊軟件防御措施開展嚴格分析.此外，Wang 等人[184]設(shè)計實現(xiàn)了一個秘密增強符號抽象域，并在此基礎(chǔ)上提出了一種新的二進制靜態(tài)分析方法來檢測基于緩存的側(cè)信道.Touzeau 等人[185]則通過結(jié)合抽象解釋與模型檢驗，實現(xiàn)高效精確的緩存分析.

針對時間側(cè)信道問題，Wu 等人[186]提出了一種基于程序分析和轉(zhuǎn)換的方法，用于消除安全關(guān)鍵應(yīng)用程序中的時間側(cè)信道，這一方法借助了抽象解釋實現(xiàn)的靜態(tài)Cache 分析.Blazy 等人[187]實現(xiàn)了一種靜態(tài)分析技術(shù)，它能夠基于抽象解釋技術(shù)，在源代碼級別保證軟件的實現(xiàn)是常數(shù)時間的.

對于在支持預(yù)測執(zhí)行的處理器上運行的程序，分析它們的行為對于執(zhí)行時間估計、側(cè)信道檢測等應(yīng)用至關(guān)重要.然而，現(xiàn)有的基于抽象解釋的靜態(tài)分析技術(shù)沒有對預(yù)測執(zhí)行進行建模，因為它們關(guān)注的主要是程序的功能屬性，而預(yù)測執(zhí)行并不改變其功能.為此，Wu 等人[188]引入了虛擬控制流的概念，以及處理合并與循環(huán)的優(yōu)化方法，并安全地限制預(yù)測執(zhí)行深度，使得能夠提升現(xiàn)有的抽象解釋技術(shù)以支持分析預(yù)測執(zhí)行下的程序.在靜態(tài)緩存分析工具中使用該技術(shù)后，能夠檢測出許多被現(xiàn)有不支持預(yù)測分析技術(shù)所忽略的緩存泄漏和側(cè)信道泄漏缺陷.

2021 年，F(xiàn)ang 等人[189]提出了一種零知識靜態(tài)分析方法，它允許不受信任的一方在不暴露程序的情況下證明程序具有某種特性，并在抽象解釋程序分析的基礎(chǔ)上應(yīng)用該技術(shù).該工作提供了一種技術(shù)手段，能夠打破分析工具難以接觸受保密程序的現(xiàn)狀.

4.3 量子計算可信保證

由于量子計算難以模擬，為理解更大規(guī)模的量子程序并檢測斷言，Yu 等人[190]將抽象狀態(tài)視為一組投影構(gòu)成的元組（通過投影來對密度矩陣進行近似），在此之基礎(chǔ)上提出了構(gòu)成伽羅瓦連接的抽象化函數(shù)和具體化函數(shù)，并使用它們來定義抽象操作.該工作提出了一種量子程序的抽象方法，并基于該方法實現(xiàn)了在多項式時間內(nèi)支持300 個量子位的斷言檢測，這超出了當前超級計算機能夠模擬的量子位數(shù)量.

5 未來研究方向展望

作為程序語言與形式化方法領(lǐng)域中的一個傳統(tǒng)方向，抽象解釋持續(xù)受到學(xué)術(shù)界和工業(yè)界的關(guān)注.目前來看，抽象解釋在未來研究中的潛在方向包括:

1）結(jié)合上近似與下近似抽象的抽象解釋.目前，絕大部分抽象解釋技術(shù)采用的是上近似抽象，以保證分析驗證的可靠性.然而，單純采用上近似抽象可能導(dǎo)致精度不夠，從而可能產(chǎn)生誤報.研究下近似抽象，以及上近似與下近似抽象的結(jié)合，對于消除靜態(tài)分析誤報具有重要意義.結(jié)合O'Hearn 最近提出的不正確性邏輯[49]，在抽象解釋框架下研究下近似及其與上近似抽象的結(jié)合，是未來值得關(guān)注的研究方向.

2）機器學(xué)習(xí)輔助的抽象解釋.抽象解釋本身是基于形式化的，但是有效的啟發(fā)式信息對于提高基于抽象解釋的分析驗證的精度、效率具有重要幫助.比如，約束模版的設(shè)置、加寬閾值的選擇、抽象域的選擇、變量打包的策略、控制流匯合操作的精度控制等，都依賴于啟發(fā)式規(guī)則或者人工設(shè)定.而利用機器學(xué)習(xí)得到有效的啟發(fā)式信息，對于更有效地面向具體應(yīng)用來權(quán)衡抽象解釋的精度和效率具有重要意義.

3）抽象域的析取表達能力提升.抽象域是抽象解釋框架下的核心要素.但是，目前數(shù)值抽象域在表達析取信息方面存在局限性，導(dǎo)致分析精度不夠.而實際程序中天然存在很多析取行為，設(shè)計能夠表達析取的抽象域或者通用的析取表達能力提升算子，可以有效緩解傳統(tǒng)數(shù)值抽象域的凸性局限性、提高程序分析的精度、減少誤報.比如，將數(shù)值抽象域與SMT 約束求解器、決策圖或決策樹結(jié)合，可提升析取表達能力.

4）面向人工智能實際應(yīng)用可信保證的抽象解釋.目前抽象解釋技術(shù)已經(jīng)在深度神經(jīng)網(wǎng)絡(luò)模型和架構(gòu)的分析與驗證中有初步應(yīng)用.但是目前實驗對象的神經(jīng)元規(guī)模離大部分實際場景下神經(jīng)元規(guī)模有較大距離，支持的網(wǎng)絡(luò)模型的類型也不夠豐富；同時，如何應(yīng)用抽象解釋對實際場景中符號神經(jīng)混合系統(tǒng)開展建模、抽象與分析驗證也是值得關(guān)注的方向；另外，利用抽象解釋進行實際應(yīng)用中神經(jīng)網(wǎng)絡(luò)的魯棒訓(xùn)練也值得更多的關(guān)注.

5）面向代碼演化的抽象解釋.持續(xù)集成、持續(xù)交付、持續(xù)部署已成為現(xiàn)代軟件開發(fā)的“最佳實踐”，被廣泛應(yīng)用于實際軟件項目開發(fā)中.目前，抽象解釋方法主要應(yīng)用于完整程序代碼的分析，而針對完整版本的分析過程往往需要較多的時間和資源開銷，使其難以在快速迭代、持續(xù)集成等現(xiàn)代軟件開發(fā)實踐中快速響應(yīng).以快速迭代、持續(xù)集成等現(xiàn)代軟件開發(fā)實踐背景下所形成的系列代碼版本、代碼提交片段、版本合并等作為分析對象，形成具有支持代碼演化的增量式抽象解釋方法具有重要的現(xiàn)實意義.

6 結(jié)論

抽象解釋是程序語言與形式化方法領(lǐng)域的一個重要的研究方向.本文系統(tǒng)地對近5 年來抽象解釋的理論及其應(yīng)用研究進展進行綜述.首先介紹了抽象解釋的基本概念并綜述了其在理論框架、抽象域方面的最新進展；然后，重點概述了基于抽象解釋的程序分析、基于抽象解釋的神經(jīng)網(wǎng)絡(luò)模型驗證與魯棒訓(xùn)練及深度學(xué)習(xí)程序的分析等方面的研究進展；還對抽象解釋在智能合約可信保證、信息安全保證、量子計算可信保證等方面的應(yīng)用進展進行了介紹；最后對未來的研究方向進行了說明.總之，隨著抽象解釋理論、技術(shù)與工具的不斷發(fā)展，未來抽象解釋將在更多應(yīng)用領(lǐng)域發(fā)揮越來越重要的作用.

作者貢獻聲明：陳立前負責(zé)論文總體設(shè)計、文獻調(diào)研、理論進展與未來研究方向展望相關(guān)內(nèi)容撰寫；范廣生負責(zé)程序分析與其他典型應(yīng)用相關(guān)的文獻調(diào)研與內(nèi)容撰寫；尹幫虎負責(zé)可信人工智能相關(guān)的文獻調(diào)研與內(nèi)容撰寫；王戟提出指導(dǎo)意見并修改論文.