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

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

1（國(guó)防科技大學(xué)計(jì)算機(jī)學(xué)院 長(zhǎng)沙 410073）

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

3（高性能計(jì)算國(guó)家重點(diǎn)實(shí)驗(yàn)室（國(guó)防科技大學(xué)）長(zhǎng)沙 410073）

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

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

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

1 抽象解釋理論

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

1.1 基本概念

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

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

1.2 理論進(jìn)展

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

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

另外，在抽象解釋的完備性相關(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ù)之間可以進(jìn)行技術(shù)遷移.Bruni 等人[12]將程序的外延（功能）等價(jià)性一般化為抽象等價(jià)性.2 個(gè)程序是外延等價(jià)的，當(dāng)且僅當(dāng)2 者在具體語(yǔ)義下是等價(jià)的.2 個(gè)外延等價(jià)的程序，可能具有不同的抽象語(yǔ)義（如，因?yàn)槌绦虼a進(jìn)行了變換，導(dǎo)致抽象語(yǔ)義產(chǎn)生了差異）.文獻(xiàn)[12]工作引入了完備團(tuán)（completeness cliques）和不完備團(tuán)（incompleteness cliques）的概念來(lái)對(duì)程序進(jìn)行分類(lèi).完備團(tuán)C(P，A)表示所有與程序P語(yǔ)義等價(jià)，且抽象域A對(duì)其而言是完備的那些程序構(gòu)成的集合；不完備團(tuán)(P，A)表示所有與程序P語(yǔ)義等價(jià)、且抽象域A對(duì)其而言不是完備的那些程序構(gòu)成的集合.換言之，C(P，A)表示所有應(yīng)用抽象域A分析得到的結(jié)果是足夠精確（無(wú)誤報(bào)）的程序P的變種構(gòu)成的集合；而(P，A)表示所有應(yīng)用抽象域A分析得到的結(jié)果是不夠精確的（存在誤報(bào)）的程序P的變種構(gòu)成的集合.應(yīng)用抽象等價(jià)性的概念，可以幫助理解代碼迷惑技術(shù)和程序分析精度之間的關(guān)聯(lián)關(guān)系.

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

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

1.3 抽象域進(jìn)展

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

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

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

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

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

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

2.1 技術(shù)進(jìn)展

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

1）提高精度

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

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

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

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

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

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

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

2）提高可擴(kuò)展性

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

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

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

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

3）提高可用性

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

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

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

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

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

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

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

2.2 工具進(jìn)展

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.1.2 基于Zonotope 抽象域的驗(yàn)證

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

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

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

3.1.3 基于多面體抽象域的驗(yàn)證

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4.1 智能合約可信保證

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

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

4.2 信息安全保證

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

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

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

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

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

4.3 量子計(jì)算可信保證

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

5 未來(lái)研究方向展望

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

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

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

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

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

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

6 結(jié)論

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

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