張 健,張 超,玄躋峰,熊英飛,王千祥,梁 彬,李 煉,竇文生,陳振邦,陳立前,蔡 彥

1(計(jì)算機(jī)科學(xué)國(guó)家重點(diǎn)實(shí)驗(yàn)室(中國(guó)科學(xué)院 軟件研究所),北京 100190)

2(中國(guó)科學(xué)院大學(xué),北京 100049)

3(清華大學(xué) 網(wǎng)絡(luò)科學(xué)與網(wǎng)絡(luò)空間研究院,北京 100084)

4(武漢大學(xué) 計(jì)算機(jī)學(xué)院,湖北 武漢 430072)

5(高可信軟件技術(shù)教育部重點(diǎn)實(shí)驗(yàn)室(北京大學(xué)),北京 100871)

6(華為技術(shù)有限公司,北京 100095)

7(中國(guó)人民大學(xué) 信息學(xué)院,北京 100872)

8(中國(guó)科學(xué)院 計(jì)算技術(shù)研究所,北京 100190)

9(國(guó)防科技大學(xué) 計(jì)算機(jī)學(xué)院,湖南 長(zhǎng)沙 410073)

隨著信息化的不斷發(fā)展,軟件對(duì)人們生活的影響越來(lái)越大,在國(guó)民經(jīng)濟(jì)和國(guó)防建設(shè)中具有越來(lái)越重要的地位.如何提高軟件質(zhì)量,保證其行為的可信性,是學(xué)術(shù)界和工業(yè)界共同關(guān)注的重要問(wèn)題.要解決該問(wèn)題,應(yīng)加強(qiáng)軟件開發(fā)過(guò)程管理,在全生命周期采取各種方法和技術(shù)提升軟件質(zhì)量.由于軟件系統(tǒng)的復(fù)雜性,在編碼實(shí)現(xiàn)完成之后,甚至在軟件產(chǎn)品發(fā)布、被廣泛使用之后,往往還有各種各樣的缺陷和漏洞.各種軟件測(cè)試和分析技術(shù),是發(fā)現(xiàn)這些缺陷、漏洞的有效手段.

不同于很多黑盒測(cè)試方法,軟件分析技術(shù)可深入軟件系統(tǒng)內(nèi)部,細(xì)致地考察其結(jié)構(gòu)及各個(gè)組成部分,進(jìn)而發(fā)現(xiàn)其各種特性,如性能、正確性、安全性等.軟件分析已逐漸發(fā)展成為程序語(yǔ)言和軟件工程領(lǐng)域的一個(gè)重要研究方向,并已影響到信息安全等相關(guān)領(lǐng)域.進(jìn)入 21世紀(jì)以來(lái),該方向進(jìn)展顯著,研究成果不斷涌現(xiàn).軟件分析不僅可用來(lái)發(fā)現(xiàn)軟件中的缺陷、漏洞,還可用于軟件理解、修復(fù)以及測(cè)試用例生成等方面[1].

軟件包含程序和文檔.由于篇幅所限,本文主要介紹程序分析方面的研究,特別是最近 10余年該方向的一些重要工作.本文將介紹程序分析的基本概念(分析對(duì)象、難度、評(píng)價(jià)等)、主要的基礎(chǔ)性分析技術(shù)、針對(duì)不同類型分析對(duì)象的分析方法等.最后,簡(jiǎn)要提及一些挑戰(zhàn)性問(wèn)題以及新興的研究方向.

1 程序分析簡(jiǎn)介

本節(jié)介紹程序分析的基本概念、程序及其性質(zhì)多樣性等,進(jìn)而解釋程序分析的難度及其評(píng)價(jià).

1.1 基本概念

程序分析指的是:對(duì)計(jì)算機(jī)程序進(jìn)行自動(dòng)化的處理,以確認(rèn)或發(fā)現(xiàn)其特性,比如性能、正確性、安全性等[2].程序分析的結(jié)果可用于編譯優(yōu)化、提供警告信息等,比如被分析程序在某處可能出現(xiàn)指針為空、數(shù)組下標(biāo)越界的情形等.

傳統(tǒng)上,程序分析包括各種靜態(tài)分析技術(shù)(類型檢查、數(shù)據(jù)流分析、指向分析等)與動(dòng)態(tài)分析技術(shù):所謂的靜態(tài)分析,是指對(duì)程序代碼進(jìn)行自動(dòng)化的掃描、分析,而不必運(yùn)行程序;與靜態(tài)分析相對(duì)應(yīng)的是動(dòng)態(tài)分析技術(shù),其利用程序運(yùn)行過(guò)程中的動(dòng)態(tài)信息,分析其行為和特性.

與程序分析密切相關(guān)的兩類方法是形式驗(yàn)證及測(cè)試:前者試圖通過(guò)形式化方法,嚴(yán)格證明程序具有某種性質(zhì),目前,其自動(dòng)化程度尚有不足,難于實(shí)用;測(cè)試方法多種多樣,在實(shí)際工程中廣泛使用,這些方法也是以發(fā)現(xiàn)程序中的缺陷為目的,它們一般都需要人們提供輸入數(shù)據(jù),以便運(yùn)行程序,觀察其輸出結(jié)果.

1.2 程序及其性質(zhì)的多樣性

程序分析內(nèi)涵比較豐富,具有多樣性.

1) 被分析對(duì)象的多樣性

程序分析的對(duì)象既可以是源代碼,也可以是二進(jìn)制可執(zhí)行代碼.對(duì)于源程序,根據(jù)其實(shí)現(xiàn)語(yǔ)言不同,可能需要不同的分析技術(shù).比如,C程序和 Java程序的分析,其技術(shù)可能就不一樣:后者需要處理一些面向?qū)ο蟮慕Y(jié)構(gòu).即使是同一種高級(jí)語(yǔ)言編寫的程序,也可能具有不同的特性.比如,程序中是否有比較多的指針?是否使用并發(fā)控制結(jié)構(gòu)、通信機(jī)制?是否有大量的數(shù)值計(jì)算.從規(guī)模看,被分析的程序可以是幾百行的代碼,也可以是幾十萬(wàn)行乃至于上千萬(wàn)行代碼.

2) 程序性質(zhì)的多樣性

對(duì)不同類型的程序,在不同的應(yīng)用環(huán)境下,人們關(guān)注的性質(zhì)也不一樣.以 C程序?yàn)槔?很多 C程序會(huì)用到指針,用于動(dòng)態(tài)分配、釋放內(nèi)存.對(duì)這樣的程序,人們會(huì)關(guān)注空指針、內(nèi)存泄漏等問(wèn)題.但對(duì)某些嵌入式系統(tǒng)來(lái)說(shuō),程序中很少動(dòng)態(tài)分配內(nèi)存空間,卻可能要處理中斷.另外一些 C程序可能有大量的數(shù)值(浮點(diǎn)數(shù))計(jì)算,程序員可能更關(guān)注其中是否存在溢出問(wèn)題.

1.3 程序分析的難度及評(píng)價(jià)

由于程序語(yǔ)言的復(fù)雜性、程序性質(zhì)的多樣性,自動(dòng)化的程序分析往往具有相當(dāng)大的難度.根據(jù)Rice定理:對(duì)于程序行為的任何非平凡屬性,都不存在可以檢查該屬性的通用算法[3].也就是說(shuō),大量的程序分析問(wèn)題都是不可判定的.比如,一般情況下,程序的終止性就是不可判定的.也就是說(shuō),不存在一種算法,它能判斷任何給定的程序是否總能終止.程序路徑的可行性(path feasibility)也是不可判定的[4].如果存在輸入數(shù)據(jù)使得程序沿著一條路徑執(zhí)行,程序中該路徑被稱為是可行的(feasible).沒(méi)有一種算法,它能判斷程序中某條給定路徑是否可行.最近,Cousot等人[5]從抽象解釋的角度形式化地證明了:從可計(jì)算性角度看,相比程序驗(yàn)證(只需要檢查一個(gè)給定的程序不變式是否正確),程序分析(需要綜合出正確的程序不變式)是一個(gè)更難的問(wèn)題.具體而言:對(duì)于證明有窮域上的程序斷言,程序分析與程序驗(yàn)證是等價(jià)的問(wèn)題;但是對(duì)于無(wú)窮域上的斷言,程序分析比程序驗(yàn)證更難.

鑒于程序分析的理論難度以及被分析程序的復(fù)雜度,我們往往不要求對(duì)程序進(jìn)行完全精確的分析.這就可能帶來(lái)誤報(bào)(false positive)、漏報(bào)(false negative)等問(wèn)題:前者指的是報(bào)警信息指出的缺陷實(shí)際上不存在、不可能發(fā)生;后者指的是程序中存在的某個(gè)缺陷,沒(méi)有被程序分析工具所發(fā)現(xiàn).

對(duì)程序分析技術(shù)或工具進(jìn)行評(píng)價(jià),不僅要看其分析對(duì)象的規(guī)模、復(fù)雜度,分析過(guò)程的效率,還要看其對(duì)用戶的要求,發(fā)現(xiàn)缺陷的嚴(yán)重程度,以及誤報(bào)率、漏報(bào)率等.

2 程序分析方法和技術(shù)

本節(jié)主要介紹一些近期有重要進(jìn)展的程序分析方法和技術(shù),包括抽象解釋、數(shù)據(jù)流分析、基于摘要的過(guò)程間分析、符號(hào)執(zhí)行、動(dòng)態(tài)分析、基于機(jī)器學(xué)習(xí)的程序分析等.這6項(xiàng)方法和技術(shù)的關(guān)系如圖1所示.

Fig.1 Main program analysis techniques圖1 主要的程序分析技術(shù)

程序分析總體可以分為靜態(tài)分析和動(dòng)態(tài)分析,涉及的基礎(chǔ)理論包括抽象解釋、約束求解、自動(dòng)推理等.而靜態(tài)分析的關(guān)鍵技術(shù)包括數(shù)據(jù)流分析、過(guò)程間分析、符號(hào)執(zhí)行等.最后,近期機(jī)器學(xué)習(xí)技術(shù)被用于提升各種不同的程序分析技術(shù).

除了這 6種基本程序分析技術(shù)之外,還有一些其他廣泛使用的程序分析技術(shù)也在近期有顯著進(jìn)展,如污點(diǎn)分析、模型檢驗(yàn)、編程規(guī)則檢查[6]等,由于受篇幅所限,本文將不再對(duì)這些技術(shù)進(jìn)行詳述.

2.1 抽象解釋

抽象解釋是一種對(duì)程序語(yǔ)義進(jìn)行可靠抽象(或近似)的通用理論[7].該理論為程序分析的設(shè)計(jì)和構(gòu)建提供了一個(gè)通用的框架[8],并從理論上保證了所構(gòu)建的程序分析的終止性和可靠性(即考慮了所有的程序行為).基于抽象解釋來(lái)設(shè)計(jì)程序分析,本質(zhì)上是通過(guò)對(duì)程序語(yǔ)義進(jìn)行不同程度的抽象,以在分析精度和計(jì)算效率之間取得權(quán)衡.這種由某種語(yǔ)義抽象及其上的操作所構(gòu)成的數(shù)學(xué)結(jié)構(gòu)稱為抽象域.抽象解釋采用 Galois連接來(lái)刻畫具體域與抽象域之間的關(guān)系.設(shè)〈D,?〉和〈D#,?#〉是兩個(gè)給定的偏序集,函數(shù)α:D→D#及γ:D#→D構(gòu)成的函數(shù)對(duì)(α,γ)稱為D與D#之間的 Galois連接,當(dāng)且僅當(dāng)?x∈D,x#∈D#,α(x)?#x#?x?γ(x#),其中,〈D,?〉稱為具體域,〈D#,?#〉稱為抽象域,α稱為抽象化函數(shù),γ稱為具體化函數(shù).由定義中的性質(zhì)α(x)?#x#(亦即x?γ(x#))可知,x#是x的可靠抽象(又稱上近似).給定具體域〈D,?〉和抽象域〈D#,?#〉之間的 Galois 連接(α,γ),對(duì)于具體域D上的函數(shù)f和抽象域D#上的函數(shù)f#,當(dāng)?x#∈D#,(f?γ)(x#)?(γ?f#)(x#)時(shí),我們稱f#是f的可靠抽象.抽象解釋理論的一個(gè)重要思想是,通過(guò)在抽象域上計(jì)算程序的抽象不動(dòng)點(diǎn)來(lái)表達(dá)程序的抽象語(yǔ)義.在程序分析中,程序狀態(tài)集合通過(guò)抽象域中的域元素來(lái)近似,而程序語(yǔ)義動(dòng)作(如賦值、條件測(cè)試等)通過(guò)抽象域中的域操作(如遷移函數(shù))來(lái)可靠建模.此外,為了加速抽象域上不動(dòng)點(diǎn)迭代的收斂速度并保證不動(dòng)點(diǎn)迭代的終止性,抽象解釋框架提供了加寬算子(widening).抽象解釋框架能夠保證抽象域上迭代求得的抽象不動(dòng)點(diǎn)是程序最小不動(dòng)點(diǎn)(對(duì)應(yīng)程序的具體聚集語(yǔ)義)的上近似.換言之,抽象解釋提供了嚴(yán)格的理論來(lái)保證基于上近似抽象的推理的可靠性,即:所有基于上近似抽象推理得出的性質(zhì),在原程序中也必然成立.但是,由于抽象帶來(lái)的精度損失,不保證所有在原程序中成立的性質(zhì)都能基于上近似抽象推理得到.

抽象域是抽象解釋框架下的核心要素,一般是面向某類特定性質(zhì)設(shè)計(jì)的.到目前為止,已出現(xiàn)了數(shù)十種面向不同性質(zhì)的抽象域.其中,具有代表性的抽象域包括區(qū)間抽象域、八邊形抽象域、多面體抽象域等數(shù)值抽象域.此外,還出現(xiàn)了若干開源的抽象域庫(kù),如APRON[9]、ELINA[10]、PPL[11]等.基于抽象解釋的程序分析工具也不斷涌現(xiàn),出現(xiàn)了 PolySpace[12]、Astrée[13]等商業(yè)化工具和 Frama-C Value Analysis[14]、CCCheck(code contract static checker)[15]、Interproc[16]等學(xué)術(shù)界工具.隨著這些工具的日益完善,抽象解釋在工業(yè)界大規(guī)模軟件,尤其是嵌入式軟件的分析與驗(yàn)證中得到了成功應(yīng)用.典型的應(yīng)用案例是,Astrée成功應(yīng)用于空客A340(約13.2萬(wàn)行C代碼)、A380(約35萬(wàn)行C代碼)等系列飛機(jī)飛行控制軟件的自動(dòng)分析并實(shí)現(xiàn)了分析的零誤報(bào)[17].最近,Astrée的擴(kuò)展版本AstréeA支持多線程C程序中運(yùn)行時(shí)錯(cuò)誤、數(shù)據(jù)競(jìng)爭(zhēng)、死鎖等的檢測(cè),并成功應(yīng)用于ARINC 653航空電子應(yīng)用軟件(約220萬(wàn)行代碼)的分析[18].總體而言,基于抽象解釋的程序分析主要面臨提高分析精度、可擴(kuò)展性兩方面的挑戰(zhàn).

在提高分析精度方面,基于加寬的不動(dòng)點(diǎn)迭代過(guò)程所導(dǎo)致的分析精度損失問(wèn)題和抽象域本身表達(dá)能力的局限性是當(dāng)前面臨的主要問(wèn)題.

· 在緩解加寬所導(dǎo)致的精度損失方面,近年來(lái)的研究進(jìn)展大致可以分為兩種思路:(1) 使用基于策略迭代[19]或抽象加速[20]的不動(dòng)點(diǎn)迭代過(guò)程來(lái)取代傳統(tǒng)的基于加寬的不動(dòng)點(diǎn)迭代過(guò)程,以獲得更精確的分析結(jié)果,但是,該方法只適用于一些特殊類別的程序和抽象域;(2) 改進(jìn)加寬/變窄算子及其迭代序列,如結(jié)合加寬變窄算子的交疊迭代策略[21].

· 在彌補(bǔ)抽象域本身表達(dá)能力的局限性方面,最近的研究進(jìn)展可分為3類:(1) 將符號(hào)化方法與抽象方法結(jié)合起來(lái),利用SMT求解器[22,23]、插值[24]等技術(shù)來(lái)計(jì)算程序中語(yǔ)句遷移函數(shù)的最佳抽象,以改進(jìn)抽象域在語(yǔ)句遷移函數(shù)上的精度損失;(2) 提高抽象域的析取表達(dá)能力,如基于區(qū)間線性代數(shù)、絕對(duì)值約束、集合差、非格結(jié)構(gòu)、決策樹等方法構(gòu)造的非凸抽象域[25,26];(3) 提高抽象域的非線性表達(dá)能力,如基于組合遞推分析[27,28]將符號(hào)化分析與抽象解釋結(jié)合起來(lái)以生成多項(xiàng)式、指數(shù)、對(duì)數(shù)等形式非線性不變式,基于橢圓冪集來(lái)生成二次不變式[29]等.

在提高可擴(kuò)展性方面,如何有效降低分析過(guò)程中抽象狀態(tài)表示與計(jì)算的時(shí)空開銷是目前考慮的主要問(wèn)題.在這方面,最近的研究進(jìn)展包括:

· 利用變量訪問(wèn)的局部性原理,降低當(dāng)前抽象環(huán)境中所涉及的變量維數(shù),并根據(jù)數(shù)據(jù)流依賴的稀疏性,降低抽象狀態(tài)的存儲(chǔ)開銷和傳播開銷.基于該思想,最近,Oh等人提出了一種通用的全局稀疏分析框架,在不損失分析精度的前提下能夠顯著降低時(shí)空開銷,并在靜態(tài)分析工具Sparrow上進(jìn)行了應(yīng)用,取得了顯著的可擴(kuò)展性提升效果[30,31];

· 利用矩陣分解等在線分解優(yōu)化策略來(lái)對(duì)抽象域操作的算法進(jìn)行優(yōu)化.基于該思想,最近,Singh等人[32,33]對(duì)常用的八邊形抽象域、多面體抽象域的實(shí)現(xiàn)進(jìn)行了優(yōu)化,優(yōu)化后,分析的性能取得了顯著的提升,性能提升最大的達(dá) 140多倍;在此基礎(chǔ)上,Singh等人還提出了一種通用的基于分解的優(yōu)化策略[34],能夠在不改變基抽象域的基礎(chǔ)上自動(dòng)實(shí)現(xiàn)基于分解的優(yōu)化,從而無(wú)需人工重新實(shí)現(xiàn)基抽象域,并基于這一思想實(shí)現(xiàn)了開源抽象域庫(kù)ELINA.這種基于在線分解的方法不會(huì)造成精度損失.

最近,Singh等人[35]還提出了一種基于強(qiáng)化學(xué)習(xí)來(lái)加速靜態(tài)程序分析的方法,在每次迭代過(guò)程中,利用強(qiáng)化學(xué)習(xí)來(lái)決策選擇哪個(gè)轉(zhuǎn)換子,以在精度和不動(dòng)點(diǎn)迭代收斂速度之間進(jìn)行權(quán)衡.在抽象域編碼實(shí)現(xiàn)上,Becchi等人[36]最近改進(jìn)了未必封閉多面體域(支持嚴(yán)格不等式約束)的雙重描述法,在表示中避免了松弛變量的引入,極大地提高了分析效率,并開發(fā)了多面體域的開源實(shí)現(xiàn)PPLite.

此外,將抽象解釋應(yīng)用到特定類型程序或特定性質(zhì)的分析驗(yàn)證方面的研究也取得了不少進(jìn)展,主要的關(guān)注點(diǎn)包括復(fù)雜數(shù)據(jù)結(jié)構(gòu)自動(dòng)分析的支持、不同譜系目標(biāo)程序的支持、活性性質(zhì)分析的支持.在復(fù)雜數(shù)據(jù)結(jié)構(gòu)的自動(dòng)分析方面,最近的研究重點(diǎn)關(guān)注針對(duì)數(shù)組內(nèi)容的精確分析[37]、混雜數(shù)據(jù)結(jié)構(gòu)的建模[38]、數(shù)值與形態(tài)混合的程序分析[39,40]、關(guān)系型形態(tài)分析[41].在支持不同譜系目標(biāo)程序方面,最近的研究重點(diǎn)關(guān)注多線程程序的自動(dòng)分析[18]、中斷驅(qū)動(dòng)型程序的自動(dòng)分析[42,43]、概率程序的分析[44,45]、操作系統(tǒng)代碼的安全和功能性分析[38,46]、JavaScript等動(dòng)態(tài)語(yǔ)言的分析[47]、二進(jìn)制代碼的分析[48]、Web應(yīng)用程序的安全性分析[49].在目標(biāo)性質(zhì)支持方面,近年來(lái),在抽象解釋領(lǐng)域出現(xiàn)了一些新的用來(lái)分析時(shí)序性質(zhì)和終止性的方法[50-52].

未來(lái),抽象解釋技術(shù)將進(jìn)一步在新的架構(gòu)、語(yǔ)言、應(yīng)用等實(shí)際需求驅(qū)動(dòng)下不斷發(fā)展.值得關(guān)注的方向包括對(duì)弱內(nèi)存模型的分析驗(yàn)證[53,54]、神經(jīng)網(wǎng)絡(luò)的分析與驗(yàn)證[55,56]、大數(shù)據(jù)處理相關(guān)錯(cuò)誤的分析[57]、Python程序的自動(dòng)分析[58]等.與約束求解、自動(dòng)推理、人工智能等基礎(chǔ)支撐技術(shù)的緊密結(jié)合,將是抽象解釋后續(xù)的研究趨勢(shì)之一[59-61].同時(shí),降低誤報(bào)率將依然是基于抽象解釋的程序分析技術(shù)拓展實(shí)際應(yīng)用的研究挑戰(zhàn)和重點(diǎn).

2.2 數(shù)據(jù)流分析

數(shù)據(jù)流分析通過(guò)分析程序狀態(tài)信息在控制流圖中的傳播來(lái)計(jì)算每個(gè)靜態(tài)程序點(diǎn)(語(yǔ)句)在運(yùn)行時(shí)可能出現(xiàn)的狀態(tài).經(jīng)典的數(shù)據(jù)流分析理論[62]用有限高度的格〈L,?〉來(lái)抽象表示所有可能狀態(tài)的集合,并對(duì)每個(gè)程序語(yǔ)句定義一個(gè)單調(diào)的轉(zhuǎn)移函數(shù)(transfer function),以計(jì)算其對(duì)程序狀態(tài)的更新.數(shù)據(jù)流分析可以是前向或后向,對(duì)應(yīng)程序狀態(tài)信息在控制流圖中的前向或后向傳播.在程序控制流圖中,多個(gè)分支交匯的程序點(diǎn)狀態(tài)為其所有前驅(qū)(或后繼,如果是后向傳播)程序點(diǎn)狀態(tài)的?,表示不同執(zhí)行路徑下可能出現(xiàn)的所有程序狀態(tài).

數(shù)據(jù)流分析為抽象解釋的一個(gè)特例,其計(jì)算的狀態(tài)信息(抽象域)局限于有限高度的格〈L,?〉.數(shù)據(jù)流分析已經(jīng)在編譯器實(shí)現(xiàn)中得到廣泛應(yīng)用,常見的應(yīng)用包括常數(shù)傳播分析、部分冗余分析等.相比于通用的抽象解釋理論,經(jīng)典數(shù)據(jù)流分析的實(shí)現(xiàn)可以通過(guò)一個(gè)迭代計(jì)算框架來(lái)計(jì)算所有語(yǔ)句的輸出直至不動(dòng)點(diǎn).單調(diào)性和格的有限高度保證了數(shù)據(jù)流分析迭代計(jì)算框架的收斂性,而無(wú)需引入加寬算子.編譯器中的數(shù)據(jù)流分析多為過(guò)程內(nèi)數(shù)據(jù)流分析,全局過(guò)程間的分析可以使用基于摘要的方法,通過(guò)對(duì)函數(shù)自動(dòng)分析摘要得以實(shí)現(xiàn).近年來(lái),對(duì)數(shù)據(jù)流分析方向的應(yīng)用已不僅僅局限于編譯優(yōu)化,研究者們也提出了多種方法來(lái)高效實(shí)現(xiàn)過(guò)程間的上下文敏感的數(shù)據(jù)流分析,主要包括如下兩種方法.

1) IFDS/IDE數(shù)據(jù)流分析框架

IFDS分析框架由Reps等人[63]于1995年提出.IFDS將抽象域(即數(shù)據(jù)流分析計(jì)算的狀態(tài)信息)為滿足分配性的有限集合的一大類數(shù)據(jù)流分析問(wèn)題轉(zhuǎn)換為一個(gè)圖可達(dá)問(wèn)題,從而能夠有效地進(jìn)行上下文敏感的過(guò)程間分析.IFDS框架基于程序過(guò)程間控制流圖定義了一個(gè)超級(jí)流圖(supergraph),其中,每個(gè)節(jié)點(diǎn)對(duì)應(yīng)在一個(gè)程序點(diǎn)的抽象域中的一個(gè)元素;而節(jié)點(diǎn)間的邊表示該元素在過(guò)程間控制流圖的傳播,對(duì)應(yīng)著數(shù)據(jù)流分析中的轉(zhuǎn)移函數(shù).通過(guò)求解是否存在從程序入口到每個(gè)程序點(diǎn)的一個(gè)可達(dá)路徑,我們可以得到該程序點(diǎn)的狀態(tài)信息.基于該分析方法的框架已經(jīng)實(shí)現(xiàn)于開源分析系統(tǒng),如Soot[64]和Wala[65]中,并廣泛用于包括Android污點(diǎn)分析[66]在內(nèi)的多種應(yīng)用中.

Reps等人[67]后續(xù)進(jìn)一步擴(kuò)展了該框架,通過(guò)已有抽象域?yàn)榄h(huán)境而計(jì)算得到新的屬性,用于過(guò)程間常數(shù)傳播等應(yīng)用中,并形式化定義了上述圖可達(dá)問(wèn)題為上下文無(wú)關(guān)文法圖可達(dá)問(wèn)題.上下文無(wú)關(guān)文法圖可達(dá)問(wèn)題對(duì)圖中的邊進(jìn)行標(biāo)號(hào),圖中任意兩點(diǎn)可達(dá)需要兩點(diǎn)間的一條路徑上的標(biāo)號(hào)串滿足事先定義的上下文無(wú)關(guān)文法.多種不同程序分析問(wèn)題均可表示為對(duì)上下文無(wú)關(guān)文法圖可達(dá)問(wèn)題的求解.近年來(lái),包括指針?lè)治鯷68,69]、并行程序分析[70,71]等多種分析技術(shù)均通過(guò)求解上下文無(wú)關(guān)文法圖可達(dá)問(wèn)題來(lái)有效地加以實(shí)現(xiàn).

2) 基于值流圖的稀疏數(shù)據(jù)流分析方法

傳統(tǒng)的數(shù)據(jù)流分析在程序控制流圖上將所需計(jì)算的狀態(tài)信息在每個(gè)程序點(diǎn)傳播得到最終分析結(jié)果.此過(guò)程通常存在較多冗余操作,對(duì)效率,特別是過(guò)程間數(shù)據(jù)流分析效率會(huì)有很大影響.為了進(jìn)一步提高數(shù)據(jù)流分析的效率,近年來(lái),研究者們提出了多種稀疏的分析方法,從而無(wú)需計(jì)算狀態(tài)信息在每個(gè)程序點(diǎn)的傳播即可得到與數(shù)據(jù)流分析相同的結(jié)果.該類分析技術(shù)[72-76]通過(guò)一個(gè)稀疏的值流圖(value flow graph)直接表示程序變量的依賴關(guān)系,從而使得狀態(tài)信息可以有效地在該稀疏的值流圖上傳播.該值流圖保證了狀態(tài)信息可以有效地傳播到其需要使用該信息的程序點(diǎn),并避免了在無(wú)效程序點(diǎn)的冗余傳播,可大幅度提高效率.

2.3 基于摘要的過(guò)程間分析

摘要(summary)是可復(fù)用的程序模塊分析結(jié)果,能夠簡(jiǎn)要地刻畫模塊的外部行為.創(chuàng)建摘要和利用摘要開展分析的過(guò)程稱為摘要分析.在編寫程序的過(guò)程中,一個(gè)程序模塊往往需要調(diào)用其他程序模塊.對(duì)主調(diào)(caller)模塊的分析必然涉及到對(duì)被調(diào)模塊(callee)的分析.與復(fù)用被調(diào)模塊代碼可提高軟件生產(chǎn)效率類似,摘要分析期望復(fù)用被調(diào)模塊的分析結(jié)果也能提高分析主調(diào)模塊的效率.通過(guò)基于摘要的程序分析技術(shù),我們將被復(fù)用模塊的分析結(jié)果被構(gòu)造成為摘要,并在分析主調(diào)模塊時(shí)對(duì)其實(shí)例化,以加快分析速度.

傳統(tǒng)摘要分析的研究主要關(guān)注模塊化(modular)分析,即:在分析過(guò)程中將軟件劃分為多個(gè)模塊,對(duì)各個(gè)模塊分別分析和創(chuàng)建摘要,然后合并摘要獲得整體的分析結(jié)果.這樣,在分析過(guò)程中創(chuàng)建摘要的技術(shù)也稱為在線摘要技術(shù).摘要分析在最近 10年的主要進(jìn)展是離線摘要技術(shù),即:在程序分析之前對(duì)常用代碼庫(kù)生成摘要,從而加快使用這些代碼庫(kù)的客戶端的分析速度.離線摘要根據(jù)其自動(dòng)化程度的不同,可以分成人工編寫摘要和自動(dòng)生成摘要,分別在接下來(lái)的兩小節(jié)中加以介紹.

1) 人工編寫摘要

對(duì)于程序中一些難以分析的代碼,例如第三方的庫(kù)和系統(tǒng)代碼等,可采用人工編寫摘要的方式近似代碼的行為.這種技術(shù)原先應(yīng)用于程序驗(yàn)證中,比如ESC/Java通過(guò)用戶提供的前置條件和后置條件來(lái)對(duì)程序進(jìn)行模塊化驗(yàn)證.FlowDroid[66]在處理調(diào)用系統(tǒng)代碼和調(diào)用其他組件時(shí),采用由人工來(lái)編寫的近似摘要.這樣的摘要能夠模擬被調(diào)模塊中的常見數(shù)據(jù)流路徑.這種方式?jīng)]有考慮到用戶編寫的代碼對(duì)被調(diào)模塊的影響.Ali和Lhoták[77,78]提出了一種對(duì)庫(kù)建立輕量級(jí)的上近似摘要.這種摘要的建立,需要代碼庫(kù)滿足分離編譯假設(shè)(separate compilation assumption),無(wú)需應(yīng)用代碼即可編譯代碼庫(kù).Java代碼庫(kù)普遍滿足這項(xiàng)假設(shè).在該假設(shè)約束下的Java標(biāo)準(zhǔn)庫(kù)被簡(jiǎn)化為一個(gè)人工編寫的占位庫(kù),而這個(gè)占位庫(kù)的文件僅有80KB大小,遠(yuǎn)小于Java標(biāo)準(zhǔn)庫(kù)的原本大小.Ali和Lhoták[77,78]的方法改造了現(xiàn)有的全程序調(diào)用圖構(gòu)造算法,以占位庫(kù)作為所有庫(kù)函數(shù)的替代品,所有應(yīng)用代碼與庫(kù)函數(shù)代碼間的調(diào)用關(guān)系被簡(jiǎn)化為應(yīng)用代碼與占位庫(kù)間的調(diào)用關(guān)系.該方法既提升了效率(10倍以上),又保證了正確性,并且有足夠的精確度.

2) 自動(dòng)生成摘要

在程序分析過(guò)程前創(chuàng)建摘要,通常是對(duì)程序常用的模塊(如 Java代碼庫(kù))進(jìn)行摘要分析,隨后加速客戶代碼的分析.諸多的未知信息[79]和代碼庫(kù)太大造成算法難以擴(kuò)展.Cousot[80]從理論上總結(jié)了創(chuàng)建模塊摘要的各種方式.該工作首先分析了創(chuàng)建模塊摘要的主要問(wèn)題是處理模塊間的環(huán)形依賴.在沒(méi)有環(huán)形依賴時(shí),我們可以按照依賴關(guān)系給模塊排一個(gè)順序,每個(gè)模塊只依賴于之前的模塊,然后按順序依次分析.但是,由于環(huán)形依賴的存在,所有環(huán)形依賴的模塊就只能被當(dāng)作一個(gè)模塊分析,使得創(chuàng)建模塊的摘要無(wú)法進(jìn)行.文獻(xiàn)[80]針對(duì)環(huán)形依賴給出了3種解決方案.

· 基于簡(jiǎn)化的分析:這個(gè)方案的思路是針對(duì)環(huán)形依賴導(dǎo)致的大模塊上的分析通過(guò)標(biāo)準(zhǔn)的編譯技術(shù)(如partial evaluation)進(jìn)行化簡(jiǎn),提高分析速度.每個(gè)模塊上的分析程序可以被當(dāng)成是一個(gè)函數(shù),然后,把這些函數(shù)看成是標(biāo)準(zhǔn)程序之后就可以應(yīng)用普通的程序分析進(jìn)行化簡(jiǎn)了;

· 最壞情況分析:每個(gè)模塊分別分析,對(duì)于該模塊所依賴的其他模塊作最壞情況假設(shè).這樣的分析會(huì)導(dǎo)致不精確,并且在多數(shù)情況下嚴(yán)重不精確;

· 符號(hào)化關(guān)系型分析:把未知的信息做成符號(hào)化信息,然后把程序分析轉(zhuǎn)變成符號(hào)化分析.所有與符號(hào)化相關(guān)的部分不進(jìn)行計(jì)算.

Smaragdakis等人[81]提出了針對(duì)所有流不敏感指針?lè)治龅拇a庫(kù)預(yù)處理技術(shù),屬于基于簡(jiǎn)化的分析.該工作發(fā)現(xiàn):當(dāng)代碼中存在符合圖代碼模式時(shí),將模式中的冗余語(yǔ)句刪除,進(jìn)而避免冗余運(yùn)算,加速代碼分析.Rountev和Ryder[82]提出了另一種代碼庫(kù)的簡(jiǎn)化方式,對(duì)庫(kù)的摘要就是把庫(kù)里面所有的賦值語(yǔ)句提取出來(lái).這個(gè)摘要本身只是省掉了語(yǔ)法分析的時(shí)間.然后在摘要上進(jìn)行了兩個(gè)優(yōu)化.

a)對(duì)于連續(xù)賦值,比如a=b;c=a;去掉中間變量,替換成c=b;

b)去掉與客戶端無(wú)關(guān)的賦值語(yǔ)句.

這兩個(gè)優(yōu)化能省掉4%～69%的時(shí)間.該方法僅支持上下文不敏感且流不敏感的分析.

Rountev等人[83,84]提出的構(gòu)件級(jí)別分析(component-level analysis)對(duì)代碼庫(kù)的IFDS/IDE框架進(jìn)行了摘要分析.該方法采用 Sharir和 Pnueli[85]提出的函數(shù)型分析方法,為過(guò)程內(nèi)的數(shù)據(jù)流和過(guò)程間的部分?jǐn)?shù)據(jù)流建立了摘要.對(duì)于過(guò)程間邊相關(guān)的未知量,即虛函數(shù)調(diào)用(virtual function)和回調(diào)點(diǎn)(callback site),該方法在計(jì)算過(guò)程中不予考慮.該方法只考慮了函數(shù)中的局部變量.StubDroid[86]在 FlowDroid的基礎(chǔ)上采用了構(gòu)件級(jí)別分析對(duì)庫(kù)進(jìn)行了自動(dòng)分析,支持多層字段敏感性,無(wú)需手動(dòng)編寫摘要.

Tang等人[87]提出了條件可達(dá)性,解決了傳統(tǒng)摘要無(wú)法描述的回調(diào)函數(shù)問(wèn)題.具體而言,該工作考慮了過(guò)程間的數(shù)據(jù)依賴分析.當(dāng)代碼庫(kù)存在回調(diào)函數(shù)時(shí),部分信息缺失導(dǎo)致已有方法難以為代碼庫(kù)建立有效的摘要.為了處理回調(diào)函數(shù)帶來(lái)的影響,該工作提出了基于樹-鄰接語(yǔ)言的可達(dá)性的摘要分析技術(shù).注意到包含回調(diào)函數(shù)信息的可達(dá)性關(guān)系(稱為“條件可達(dá)性關(guān)系”)可用于加速用戶代碼的分析.為描述條件可達(dá)性關(guān)系,該工作引入了原本用于描述自然語(yǔ)言語(yǔ)法的形式語(yǔ)言——樹-鄰接語(yǔ)言,提出了樹-鄰接語(yǔ)言的可達(dá)性分析技術(shù).樹-鄰接語(yǔ)言可達(dá)性擴(kuò)展了表達(dá)兩點(diǎn)間可達(dá)關(guān)系的傳統(tǒng)上下文無(wú)關(guān)語(yǔ)言可達(dá)性,具有表達(dá) 4個(gè)點(diǎn)之間的可達(dá)關(guān)系的能力,從而更自然地描述了上述條件可達(dá)性關(guān)系.實(shí)驗(yàn)結(jié)果表明:建立基于樹-鄰接語(yǔ)言的可達(dá)性摘要可以在合理的時(shí)間內(nèi)完成,該技術(shù)所建立的摘要可以使得對(duì)用戶代碼分析的效率平均提高約8倍.在后續(xù)工作中[88],Tang等人進(jìn)一步將該方法擴(kuò)展到了 Dyck-CFL可達(dá)性分析上.該方法通過(guò)直接在較為通用的 CFL可達(dá)性分析過(guò)程[67]中引入帶條件邊,使得大量基于CFL可達(dá)性的分析就可以直接支持條件摘要.同時(shí),該方法引入橋接邊來(lái)避免條件組合爆炸的問(wèn)題.通過(guò)這些處理,該方法避免了原有的 Dyck-CFL分析中摘要不完整和分析效率不高的問(wèn)題.實(shí)驗(yàn)結(jié)果表明,其分析速度相比樹-鄰接語(yǔ)言進(jìn)一步提升了3倍多.

由于模塊含有大量的未知量,建立考慮所有情況的摘要在許多分析任務(wù)中非常困難.所以,一些工作通過(guò)動(dòng)態(tài)程序分析或訓(xùn)練的方式建立了部分摘要.Palepu等人[89]提出了加速程序分析速度的動(dòng)態(tài)依賴摘要技術(shù)(dynamic dependence summary),提前創(chuàng)建軟件庫(kù)的摘要,用來(lái)快速創(chuàng)建程序切片.盡管得到的是不充分的摘要,導(dǎo)致生成的程序切片并不保證完全正確,然而在程序測(cè)試的實(shí)踐中能夠找到大部分的錯(cuò)誤.Kulkarni等人[90]采用跨程序的訓(xùn)練辦法為代碼庫(kù)建立不完整的摘要,以提高客戶代碼的分析速度.該方法基于 Datalog語(yǔ)言,有效地對(duì)中間計(jì)算過(guò)程進(jìn)行剪枝,并將剪枝結(jié)果記錄于摘要中.同時(shí),該方法還對(duì) Datalog語(yǔ)言進(jìn)行改造,使得利用摘要進(jìn)行分析時(shí)可以跳過(guò)中間計(jì)算過(guò)程.該方法保證正確性的方式是人工編寫時(shí)間復(fù)雜度較低的規(guī)則,判斷訓(xùn)練得到的摘要是否能夠保證正確:如果不能保證正確性,則不采用摘要來(lái)進(jìn)行計(jì)算.

上述工作都是針對(duì)整個(gè)代碼庫(kù)進(jìn)行摘要分析.當(dāng)精度要求較高時(shí),分析完整的代碼庫(kù)比較困難.部分工作只對(duì)單個(gè)函數(shù)進(jìn)行分析.Yorsh等人[91]提出的框架可以為函數(shù)建立精確而簡(jiǎn)練的函數(shù)摘要.在不同上下文環(huán)境中,采用函數(shù)摘要與重新分析函數(shù)所得到的最終結(jié)果相同,從而保證精確性.框架中采用有限顯式輸入輸出表來(lái)表示摘要,并通過(guò)摘要組合操作,使得不同上下文之下分析過(guò)程的相似之處得以合并為更加簡(jiǎn)練的形式,從而利用有限的數(shù)據(jù)結(jié)構(gòu)表達(dá)無(wú)限可能的函數(shù)行為.該框架采用了微轉(zhuǎn)換子,微轉(zhuǎn)換子可以編碼的問(wèn)題包括IFDS/IDE問(wèn)題.該框架還可以解決模塊的線性常量傳播問(wèn)題和模塊的類型狀態(tài)[92]檢驗(yàn)問(wèn)題.

Dillig等人[93]的工作是針對(duì)C的上下文敏感、流敏感、不考慮字段的函數(shù)指向分析.核心問(wèn)題是分析一個(gè)函數(shù)時(shí),如何考慮所有可能的調(diào)用上下文.解決方案是將函數(shù)參數(shù)所有可能的別名關(guān)系編碼到一個(gè)二部圖上,一邊是參數(shù),另一邊是符號(hào)化的位置,表示彼此不交的內(nèi)存地址集合,中間連上帶約束的邊,編碼了不同的別名關(guān)系.當(dāng)遇到語(yǔ)句的轉(zhuǎn)移函數(shù)時(shí)則采用圖上再加一層的方法來(lái)保證流敏感性,這樣可以做到強(qiáng)更新.函數(shù)調(diào)用處理方面,需要計(jì)算出被調(diào)函數(shù)的別名情況,實(shí)例化主調(diào)函數(shù)的摘要,再把調(diào)用函數(shù)的圖和被調(diào)函數(shù)實(shí)例化的圖拼起來(lái).通過(guò)不動(dòng)點(diǎn)算法計(jì)算出一個(gè)上近似的結(jié)果.

2.4 符號(hào)執(zhí)行

符號(hào)執(zhí)行[94-97]是一種相對(duì)精確的程序分析技術(shù).傳統(tǒng)的符號(hào)執(zhí)行技術(shù)使用符號(hào)化輸入代替實(shí)際輸入以模擬執(zhí)行(不實(shí)際執(zhí)行)被分析程序,程序中的操作被轉(zhuǎn)化為相應(yīng)的符號(hào)表達(dá)式操作.在遇到條件語(yǔ)句時(shí),程序的執(zhí)行也相應(yīng)地分叉以探索每個(gè)分支,分支條件則被加入到當(dāng)前路徑的路徑條件(path condition)中.通過(guò)調(diào)用 SAT/SMT求解器,對(duì)路徑條件的可滿足性進(jìn)行求解來(lái)加以判斷:如果判定結(jié)果為可滿足,則說(shuō)明路徑實(shí)際可行(存在具體輸入能夠讓程序產(chǎn)生此路徑);如果判定結(jié)果為不可滿足,則表明此路徑不可行,終止對(duì)該路徑的分析.

在約束條件可被判定的情況下,符號(hào)執(zhí)行提供了一種系統(tǒng)遍歷程序路徑空間的手段.符號(hào)執(zhí)行中的程序路徑精確刻畫了程序路徑上的信息,可基于路徑信息開展多種軟件驗(yàn)證確認(rèn)階段的活動(dòng),包括自動(dòng)測(cè)試、缺陷查找以及部分的程序驗(yàn)證等[98].理論上,相比于需要固定程序輸入的分析方法,符號(hào)執(zhí)行通過(guò)符號(hào)分析,可覆蓋更多的程序行為.另一方面,符號(hào)執(zhí)行技術(shù)依賴于 SAT/SMT技術(shù),求解器的能力是決定符號(hào)執(zhí)行效果的關(guān)鍵因素.符號(hào)執(zhí)行中,程序路徑空間大小隨著程序規(guī)模的擴(kuò)大而呈指數(shù)級(jí)增長(zhǎng).例如:單就串行程序而言,一個(gè)具有n個(gè)條件語(yǔ)句的程序段就有可能包含2n條路徑,這也是制約符號(hào)執(zhí)行能力的關(guān)鍵因素.

最初,符號(hào)執(zhí)行主要用于程序自動(dòng)測(cè)試,但受制于當(dāng)時(shí)的計(jì)算能力和求解技術(shù)與工具的能力,符號(hào)執(zhí)行技術(shù)并沒(méi)有得到實(shí)際的應(yīng)用.近年來(lái),隨著計(jì)算能力的提高、SAT/SMT技術(shù)和工具的蓬勃發(fā)展[99-101],符號(hào)執(zhí)行技術(shù)得到了長(zhǎng)足的進(jìn)步,出現(xiàn)了以動(dòng)態(tài)符號(hào)執(zhí)行(concolic testing)[102,103]為代表的一批新的符號(hào)執(zhí)行方法或技術(shù),以及以 SAGE[104]、KLEE[105]、SPF[106]、Pex[107]、S2E[108]為代表的符號(hào)執(zhí)行工具.

不同于傳統(tǒng)的符號(hào)執(zhí)行,動(dòng)態(tài)符號(hào)執(zhí)行[102,103]實(shí)際運(yùn)行被分析的程序,在實(shí)際運(yùn)行的同時(shí)收集運(yùn)行路徑上的路徑條件,然后翻轉(zhuǎn)路徑條件得到新的路徑條件,通過(guò)對(duì)新的路徑條件進(jìn)行求解得到新的程序輸入以再一次地運(yùn)行被分析程序,從而探索與之前運(yùn)行不同的程序路徑.由于在實(shí)際運(yùn)行程序過(guò)程中,動(dòng)態(tài)符號(hào)執(zhí)行在碰到復(fù)雜或不可解的路徑條件時(shí),可以使用實(shí)際值來(lái)簡(jiǎn)化路徑條件.在碰到外部調(diào)用時(shí),也可以通過(guò)實(shí)際執(zhí)行來(lái)緩解外部調(diào)用的問(wèn)題.因此,在方法層面,動(dòng)態(tài)符號(hào)執(zhí)行通過(guò)犧牲部分分析的可靠性來(lái)提高方法的可擴(kuò)展性和可行性.

目前,符號(hào)執(zhí)行技術(shù)仍然面臨提高可擴(kuò)展性(scalability)與可行性(feasibility)這兩方面的挑戰(zhàn):可擴(kuò)展性挑戰(zhàn)是指如何在有限資源(比如時(shí)間、內(nèi)存)的前提下提高符號(hào)執(zhí)行的效率,更快地達(dá)成分析目標(biāo);可行性挑戰(zhàn)是指如何支持不同類型分析目標(biāo)的符號(hào)執(zhí)行,權(quán)衡分析的可靠性與精確性.已有的研究工作基本都是圍繞這兩個(gè)方面展開.

在可擴(kuò)展性方面,路徑空間爆炸和約束求解是主要的兩大難題.在緩解路徑空間爆炸方面,目前已有的工作基本分為兩個(gè)思路:(1) 在具體目標(biāo)下提供高效的搜索策略,使符號(hào)執(zhí)行分析更快地達(dá)到目標(biāo),包括提高程序的覆蓋率[105,109-111]、判斷某個(gè)程序點(diǎn)是否可達(dá)[112]、產(chǎn)生滿足正規(guī)性質(zhì)的程序路徑[113]、探索程序不同版本的差異部分[114,115]等;(2) 通過(guò)約束輸入范圍、削減或合并路徑來(lái)減小程序的路徑空間,包括基于輸入模版[116,117]、程序切片[118-121]、程序抽象(包括摘要技術(shù))[122-129]、偏序約減[130,131]、條件合并[132,133]以及等價(jià)路徑約減[121,134-136]等一些方法.在約束求解方面,已有的工作也可分為兩個(gè)方面:(1) 在調(diào)用求解器之前對(duì)路徑條件的查詢進(jìn)行優(yōu)化,以減少求解器的調(diào)用次數(shù)或縮短求解時(shí)間,包括查詢緩存和重用[105,137-139]、基于約束獨(dú)立性的優(yōu)化[103,105]、增量式求解[105,140]等;(2) 支持復(fù)雜程序特征的高效編碼,包括對(duì)機(jī)器數(shù)[104,105]、數(shù)組[100,105]、浮點(diǎn)[141-145]、字符串[146]、動(dòng)態(tài)數(shù)據(jù)結(jié)構(gòu)[147-149]等方面的支持.

在可行性方面,環(huán)境建模和多形態(tài)分析目標(biāo)的支持是目前的主要問(wèn)題.在環(huán)境建模方面,已有的工作基本都是在分析的精確性、可靠性、建模工作量以及可擴(kuò)展性之間進(jìn)行權(quán)衡和折中,包括手工建模[105,106]、自動(dòng)合成[150]、動(dòng)態(tài)執(zhí)行[102]、全棧執(zhí)行[108]等.在多形態(tài)分析目標(biāo)方面,主要是應(yīng)對(duì)多語(yǔ)言和多應(yīng)用領(lǐng)域的復(fù)雜性,包括二進(jìn)制程序[108,151,152]、腳本語(yǔ)言程序[153]、分布式程序[154]、數(shù)據(jù)庫(kù)操作程序[155]、無(wú)線傳感器網(wǎng)絡(luò)程序[156]、并發(fā)或并行程序[135,157,158]、嵌入式程序[159]、PLC程序[160]等符號(hào)執(zhí)行方法.

同時(shí),面向新的分析需求,也有一些新的符號(hào)執(zhí)行技術(shù)出現(xiàn),其中比較有代表性的是概率符號(hào)執(zhí)行技術(shù)[161-163],其基本思想是:通過(guò)符號(hào)執(zhí)行來(lái)得到程序的路徑,然后使用SMT解空間體積計(jì)算技術(shù)來(lái)計(jì)算每條路徑的路徑條件的解的個(gè)數(shù),通過(guò)每條路徑對(duì)應(yīng)的解的個(gè)數(shù),可以計(jì)算每條路徑的概率.基于此,可以開展包括低概率缺陷查找、低概率路徑的測(cè)試用例生成、生成程序的性能分布[164]、刻畫代碼變遷[165]等活動(dòng).

隨著符號(hào)執(zhí)行技術(shù)近些年的發(fā)展,符號(hào)執(zhí)行技術(shù)在工業(yè)界也得到了實(shí)際的采納和應(yīng)用,其中有代表性的工作有:微軟公司把自己開發(fā)的二進(jìn)制動(dòng)態(tài)符號(hào)執(zhí)行工具SAGE用于Win 7的測(cè)試,發(fā)現(xiàn)了文件模糊測(cè)試中1/3的缺陷[166].由于SAGE通常是微軟公司最后使用的缺陷檢測(cè)工具,因此,這些由SAGE發(fā)現(xiàn)的缺陷,很多都沒(méi)有被之前在開發(fā)過(guò)程中使用的靜態(tài)分析工具、黑盒測(cè)試工具所發(fā)現(xiàn).微軟公司多個(gè)開發(fā)小組已把SAGE作為日常工具在使用,SAGE目前也被商業(yè)化為微軟公司的安全風(fēng)險(xiǎn)檢測(cè)(microsoft security risk detection)服務(wù).微軟公司在Visual Studio 2015中正式發(fā)布了基于動(dòng)態(tài)符號(hào)執(zhí)行的C#自動(dòng)單元測(cè)試工具IntelliTest[167],可大幅度提高C#程序單元的測(cè)試效率.C程序符號(hào)執(zhí)行工具KLEE[105]對(duì)GNU Coreutils程序集進(jìn)行了自動(dòng)測(cè)試,可自動(dòng)達(dá)到94%的語(yǔ)句覆蓋率,并發(fā)現(xiàn)3個(gè)程序崩潰問(wèn)題;Canalyze[168]在開源軟件中發(fā)現(xiàn)數(shù)百個(gè)真實(shí)缺陷,并在工業(yè)界嵌入式系統(tǒng)中發(fā)現(xiàn)兩個(gè)缺陷.2016年 8月,在美國(guó)DARPA舉辦的網(wǎng)絡(luò)空間安全競(jìng)賽(CGC)中,最終排名前三的參賽隊(duì)伍全部使用了符號(hào)執(zhí)行技術(shù),用于自動(dòng)發(fā)現(xiàn)并利用二進(jìn)制程序中的漏洞.美國(guó) GrammaTech公司開發(fā)的商業(yè)程序分析工具CodeSonar中也使用了符號(hào)執(zhí)行技術(shù),用以發(fā)現(xiàn)程序中的深層缺陷.

未來(lái),符號(hào)執(zhí)行技術(shù)將進(jìn)一步在軟件工程、安全、系統(tǒng)、網(wǎng)絡(luò)等相關(guān)領(lǐng)域的實(shí)際需求驅(qū)動(dòng)下不斷發(fā)展.面向大規(guī)模軟件的高效符號(hào)執(zhí)行方法、技術(shù)和工具將是下一步研究所面臨的挑戰(zhàn)和重點(diǎn).同時(shí),符號(hào)執(zhí)行搜索策略的更加智能化[169]也將是下一步的研究重點(diǎn).此外,與其他技術(shù)在不同層面的密切結(jié)合[170-173],以進(jìn)一步提高軟件分析效果,也將成為符號(hào)執(zhí)行后續(xù)的研究趨勢(shì)之一.

2.5 動(dòng)態(tài)分析

動(dòng)態(tài)分析是指通過(guò)在指定測(cè)試用例下運(yùn)行給定的程序,并分析程序運(yùn)行過(guò)程或結(jié)果,用于缺陷檢測(cè)等.與靜態(tài)分析相比,動(dòng)態(tài)分析能夠更好地處理編程語(yǔ)言中的動(dòng)態(tài)屬性,例如指針、動(dòng)態(tài)綁定、面向?qū)ο笳Z(yǔ)言中的多態(tài)與繼承、線程交替等.動(dòng)態(tài)分析在一定程度上彌補(bǔ)了靜態(tài)分析的不足之處.

基本的程序動(dòng)態(tài)分析可以簡(jiǎn)單地分為在線(online)動(dòng)態(tài)分析與離線(offline)動(dòng)態(tài)分析[1].在線動(dòng)態(tài)分析是指在程序的運(yùn)行過(guò)程中分析當(dāng)前程序行為;而離線動(dòng)態(tài)分析需要記錄程序的運(yùn)行行為,在程序運(yùn)行結(jié)束后再進(jìn)行分析.兩者的基本思想都是通過(guò)對(duì)程序運(yùn)行過(guò)程或者結(jié)果的分析,查找定位缺陷.具體來(lái)說(shuō),一方面可以將程序運(yùn)行結(jié)果和預(yù)知結(jié)果對(duì)比,確定程序中是否含有缺陷;另一方面,可以通過(guò)插樁或其他監(jiān)控技術(shù)分析程序的運(yùn)行行為,查找錯(cuò)誤的行為.前者很直觀,但是對(duì)于被觸發(fā)了卻沒(méi)有反映在輸出中的缺陷無(wú)法檢測(cè);后者則可以直接觀察到程序中缺陷的觸發(fā),即使該次觸發(fā)并沒(méi)有導(dǎo)致錯(cuò)誤的輸出.但是后者需要提前定義錯(cuò)誤的行為,其對(duì)于非常見的缺陷無(wú)法檢測(cè).已有文獻(xiàn)中有大量這方面的介紹[174].

程序動(dòng)態(tài)分析,從報(bào)告缺陷的準(zhǔn)確性出發(fā),也可以分為:(1) 缺陷動(dòng)態(tài)檢測(cè);(2) 缺陷動(dòng)態(tài)預(yù)測(cè).一般所指的缺陷動(dòng)態(tài)查找方法是缺陷動(dòng)態(tài)檢測(cè),是指在程序的運(yùn)行過(guò)程中某個(gè)缺陷已經(jīng)發(fā)生了之后的檢測(cè),即,缺陷已經(jīng)反映在程序行為中或者運(yùn)行結(jié)果中.其關(guān)注點(diǎn)是:如何設(shè)計(jì)檢測(cè)算法等,保證將所有已經(jīng)發(fā)生的缺陷檢測(cè)出來(lái).然而,程序中的不同缺陷不會(huì)都在有限的若干測(cè)試用例中被觸發(fā).因此,為了提高缺陷動(dòng)態(tài)檢測(cè)的有效性,需要從程序若干次運(yùn)行中預(yù)測(cè)出該程序潛在的某些行為,并判斷這些潛在行為是否會(huì)觸發(fā)缺陷.這種方法稱為缺陷的動(dòng)態(tài)預(yù)測(cè).例如:某個(gè)程序中存在一個(gè)緩沖區(qū)溢出缺陷,該缺陷只有在輸入input大于128時(shí)發(fā)生.那么,如果我們可以從某個(gè)input不大于128的輸入下預(yù)測(cè)對(duì)應(yīng)行為是一個(gè)潛在缺陷,其可能會(huì)在input大于128時(shí)發(fā)生.進(jìn)一步地,我們可以構(gòu)造一個(gè)滿足預(yù)測(cè)條件的輸入,再次運(yùn)行程序去觸發(fā)(驗(yàn)證)缺陷.缺陷的動(dòng)態(tài)預(yù)測(cè)在并發(fā)程序的動(dòng)態(tài)分析中經(jīng)常用到,主要原因之一是:并發(fā)程序的運(yùn)行除了與輸入有關(guān)外,還與程序中線程之間的調(diào)度有關(guān).程序缺陷的動(dòng)態(tài)預(yù)測(cè)還會(huì)涉及到一些其他技術(shù),例如,測(cè)試用例生成、約束求解、缺陷重現(xiàn)、線程調(diào)度等,其分析過(guò)程與缺陷動(dòng)態(tài)檢測(cè)相比更為復(fù)雜.

2.6 基于機(jī)器學(xué)習(xí)的程序分析

經(jīng)典的程序分析技術(shù)提供相對(duì)精確的分析結(jié)果,但同時(shí)也帶來(lái)了包括路徑組合爆炸、誤報(bào)率較高等一系列在實(shí)踐中不可避免卻難以應(yīng)對(duì)的問(wèn)題.隨著近年來(lái)通用計(jì)算設(shè)備能力的提高,海量的程序執(zhí)行數(shù)據(jù)被存儲(chǔ)和管理;研究者采用機(jī)器學(xué)習(xí)、統(tǒng)計(jì)分析等系列技術(shù)提升現(xiàn)有的程序分析能力.

現(xiàn)有的程序分析技術(shù)依賴于一定的啟發(fā)式策略,如符號(hào)執(zhí)行技術(shù)中的深度(或廣度)優(yōu)先搜索.在動(dòng)態(tài)分析技術(shù)中,為了達(dá)到分析精度,這些策略可能帶來(lái)較高的計(jì)算成本.基于現(xiàn)有的標(biāo)記數(shù)據(jù)(即已知分析結(jié)果的程序)建立學(xué)習(xí)模型,機(jī)器學(xué)習(xí)技術(shù)可以學(xué)習(xí)新的可自適應(yīng)的策略,減少啟發(fā)式策略帶來(lái)的成本消耗.Li等人[144]為了解決符號(hào)執(zhí)行中的路徑可達(dá)性問(wèn)題,以最小化不滿足性為目標(biāo),建立機(jī)器學(xué)習(xí)模型 MLB,以減少經(jīng)典的約束求解方案在求解非線性約束及函數(shù)調(diào)用時(shí)的不足.Kong等人[175]面向自動(dòng)機(jī)驗(yàn)證,研究了多個(gè)隨機(jī)測(cè)試與符號(hào)執(zhí)行技術(shù)的整合策略,通過(guò)調(diào)整狀態(tài)轉(zhuǎn)移概率優(yōu)化動(dòng)態(tài)符號(hào)執(zhí)行.Wang等人[172]提出了基于馬爾可夫過(guò)程的動(dòng)態(tài)符號(hào)執(zhí)行方法,以達(dá)到應(yīng)用符號(hào)執(zhí)行獲得精確分析結(jié)果和應(yīng)用隨機(jī)測(cè)試覆蓋搜索空間的平衡.該方法采用貪心算法獲得優(yōu)化模型的解,以期找到對(duì)應(yīng)于近似最優(yōu)性能的策略.Chen等人[176]針對(duì)信息物理系統(tǒng)(cyber-physical system)的攻防模型,設(shè)計(jì)了基于程序變異的方案,獲得具有植入錯(cuò)誤的模型訓(xùn)練數(shù)據(jù)以避免人工建立模型的巨大成本.Xiong等人[177]提出了基于概率程序合成框架 L2S.該框架整合了包括程序合成的搜索空間、路徑和潛在解的概率估計(jì)方案,能夠按需地構(gòu)建程序合成和修復(fù)技術(shù),研究者可基于該框架深度定制和設(shè)計(jì)相關(guān)方法.

在靜態(tài)分析技術(shù)中,分析工具在獲得較高的分析精度的同時(shí),往往帶來(lái)過(guò)高的誤報(bào)率.研究者建立了機(jī)器學(xué)習(xí)模型,以剔除潛在的誤報(bào)并減少靜態(tài)分析的成本.Heo等人[178]提出了基于異常點(diǎn)檢測(cè)技術(shù)來(lái)濾除靜態(tài)分析結(jié)果中的誤報(bào).該方法提取代碼循環(huán)和函數(shù)調(diào)用中的特征,基于訓(xùn)練數(shù)據(jù)建立學(xué)習(xí)模型,識(shí)別潛在的誤報(bào)并提升靜態(tài)分析的實(shí)用性.Chae等人[59]針對(duì)上下文敏感的指針?lè)治?提出了基于分類器的自動(dòng)特征抽取方案.該方案可有效提升現(xiàn)有的靜態(tài)分析技術(shù).Oh等人[179,180]針對(duì)靜態(tài)分析的精度和計(jì)算成本,提出了基于貝葉斯優(yōu)化的自適應(yīng)學(xué)習(xí)方案,并以此建立面向數(shù)據(jù)流和上下文的部分靜態(tài)分析工具.Jeong等人[181]設(shè)計(jì)了數(shù)據(jù)驅(qū)動(dòng)的上下文敏感的指針?lè)治龇桨?該方案通過(guò)非線性的上下文選擇,建立了識(shí)別上下文敏感函數(shù)的學(xué)習(xí)方法.

3 面向特定軟件的程序分析技術(shù)

本節(jié)介紹程序分析技術(shù)在一些重點(diǎn)領(lǐng)域軟件的應(yīng)用,包括移動(dòng)應(yīng)用軟件、并發(fā)軟件、分布式系統(tǒng)、二進(jìn)制代碼等方面的重要應(yīng)用.

3.1 移動(dòng)應(yīng)用軟件

近10年來(lái),以智能手機(jī)為代表的智能終端以驚人的速度得以普及.目前,以Android和蘋果iOS系統(tǒng)為代表的智能手機(jī)數(shù)量和使用頻度已遠(yuǎn)超個(gè)人計(jì)算機(jī),成為最流行的個(gè)人電子設(shè)備.通過(guò)移動(dòng)支付、購(gòu)物和社交等各式各樣的移動(dòng)應(yīng)用,智能手機(jī)已經(jīng)深度滲透進(jìn)了人們的日?；顒?dòng)中.相應(yīng)地,這些應(yīng)用的運(yùn)行狀態(tài)和廣大用戶的日常生活和工作有著直接的關(guān)系,也在很大程度上影響到了整個(gè)互聯(lián)網(wǎng)的運(yùn)轉(zhuǎn).為此,研究人員通過(guò)對(duì)移動(dòng)應(yīng)用軟件的程序分析,來(lái)檢測(cè)其是否具有所期望的以安全性為核心的各種特性.

1) 污點(diǎn)分析技術(shù)

由于智能手機(jī)的使用特點(diǎn),移動(dòng)應(yīng)用的安全性分析常?？梢詺w結(jié)為應(yīng)用代碼上跟蹤敏感數(shù)據(jù)流的動(dòng)態(tài)/靜態(tài)污點(diǎn)分析(taint analysis)問(wèn)題.

· 動(dòng)態(tài)污點(diǎn)分析:最具代表性的 Android應(yīng)用動(dòng)態(tài)污點(diǎn)分析技術(shù)是 TaintDroid[182],其通過(guò)修改的 Dalvik Java虛擬機(jī),在應(yīng)用的Java字節(jié)碼的解釋執(zhí)行過(guò)程中進(jìn)行動(dòng)態(tài)插樁,以實(shí)施對(duì)敏感數(shù)據(jù)的跟蹤分析.在TaintDroid的基礎(chǔ)上,研究人員還研發(fā)出了其他一些應(yīng)用安全性分析和防護(hù)系統(tǒng),如 AppFence[183]和DroidBox[184]等.Yan等人開發(fā)了一個(gè)基于全系統(tǒng)虛擬化的動(dòng)態(tài)污點(diǎn)分析平臺(tái) DroidScope[185],構(gòu)建于CPU模擬器QEMU[186]之上,發(fā)展自面向桌面平臺(tái)的污點(diǎn)分析系統(tǒng)TEMU[187].DroidScope可在CPU指令模擬執(zhí)行層面對(duì)運(yùn)行于模擬器上的整個(gè)系統(tǒng)(包括 Android應(yīng)用和操作系統(tǒng))中的信息流進(jìn)行跟蹤,但在較低層面實(shí)施污點(diǎn)分析不可避免地帶來(lái)一定的語(yǔ)義鴻溝(semantic gap),從而影響到污點(diǎn)分析工作的精度;

· 靜態(tài)污點(diǎn)分析:FlowDroid[66]是影響較大的基于Android的靜態(tài)污點(diǎn)分析工具.FlowDroid基于過(guò)程間控制流圖進(jìn)行靜態(tài)的Jimple代碼模擬執(zhí)行,根據(jù)Jimple指令的語(yǔ)義跟蹤敏感數(shù)據(jù)在潛在執(zhí)行路徑上的傳播,從而檢測(cè)分析目標(biāo)應(yīng)用中可能存在的隱私泄露等危險(xiǎn)操作.類似地,在Android應(yīng)用Java字節(jié)碼層面進(jìn)行靜態(tài)污點(diǎn)分析的系統(tǒng)還有 AndroidLeaks[188]和 Apposcopy[189]等.為了更精確地分析Android應(yīng)用中的敏感信息流,DroidSafe[190]對(duì) Android底層系統(tǒng)進(jìn)行了建模,將其表示為與應(yīng)用開發(fā)語(yǔ)言相匹配的Java程序,從而跟蹤分析涉及到系統(tǒng)底層的信息流.Jin等人[191]針對(duì)采用JavaScript來(lái)實(shí)現(xiàn)應(yīng)用邏輯的HTML5混合型移動(dòng)應(yīng)用,設(shè)計(jì)實(shí)現(xiàn)了一種JavaScript代碼注入漏洞的靜態(tài)檢測(cè)方法,所采用的核心技術(shù)也是靜態(tài)污點(diǎn)分析.針對(duì)蘋果手機(jī)應(yīng)用,PiOS[192]通過(guò)對(duì)iOS應(yīng)用的Mach-O二進(jìn)制可執(zhí)行文件進(jìn)行靜態(tài)數(shù)據(jù)流分析來(lái)檢測(cè)應(yīng)用是否有泄露隱私的行為.

2) 面向移動(dòng)應(yīng)用特性的程序分析技術(shù)

與桌面應(yīng)用的分析相比,移動(dòng)應(yīng)用的分析還會(huì)涉及到一些與移動(dòng)平臺(tái)特性密切相關(guān)的分析任務(wù),如組件間通信(inter-component communication)的分析[193]、電量過(guò)度消耗等資源泄露(resource leak)的檢測(cè)[194]、權(quán)限泄露(capability leak)[195]以及權(quán)限重代理(permission re-delegation)[196]的檢測(cè)防御等.

3) 移動(dòng)應(yīng)用分析輔助技術(shù)

為了達(dá)到較好的分析效果,僅僅關(guān)注于應(yīng)用軟件分析技術(shù)本身是不夠的,研究人員還發(fā)展出一些分析輔助技術(shù)來(lái)進(jìn)一步提升分析效果.為了在動(dòng)態(tài)分析工作中獲得較高的覆蓋率,學(xué)術(shù)界研究出一些系統(tǒng)化的應(yīng)用運(yùn)行驅(qū)動(dòng)技術(shù),如 AndroidRipper[197]、Dynodroid[198]、AppDoctor[199]、EvoDroid[200]和 TrimDroid[201]等.為了較為方便地在真實(shí) Android手機(jī)環(huán)境中部署分析機(jī)制,You等人提出一種稱為引用劫持(reference hijacking)的技術(shù)[202],可在不刷機(jī)、不 ROOT設(shè)備的情況下,將動(dòng)態(tài)污點(diǎn)分析機(jī)制植入到底層系統(tǒng)庫(kù)中.與桌面平臺(tái)相比,移動(dòng)平臺(tái)具有更為復(fù)雜的權(quán)限管理機(jī)制.PScout[203]使用靜態(tài)分析從 Android系統(tǒng)源代碼中抽取出應(yīng)用編程 API所對(duì)應(yīng)的權(quán)限規(guī)范,從而為 Android應(yīng)用的安全分析提供了重要的支持.Android應(yīng)用中存在有大量的隱式調(diào)用,導(dǎo)致靜態(tài)構(gòu)建函數(shù)調(diào)用圖是一個(gè)非常具有挑戰(zhàn)性的任務(wù).EdgeMiner[204]通過(guò)靜態(tài)分析Android的Framework層代碼來(lái)生成各個(gè) API所導(dǎo)致的隱式控制流轉(zhuǎn)移的函數(shù)摘要,能夠被集成在已有的靜態(tài)分析工具中以提高Android應(yīng)用分析的精度.對(duì)應(yīng)用進(jìn)行污點(diǎn)分析需要明確知道引入敏感數(shù)據(jù)的 Source點(diǎn)和會(huì)導(dǎo)致危險(xiǎn)操作的Sink點(diǎn),但現(xiàn)實(shí)中缺乏一個(gè)完全的Source/Sink點(diǎn)規(guī)范.Rasthofer等人[205]利用機(jī)器學(xué)習(xí)技術(shù)設(shè)計(jì)了一個(gè)支持向量機(jī)分類器以自動(dòng)識(shí)別Android系統(tǒng)API中未知的Source點(diǎn)和Sink點(diǎn).為了獲得可供分析的代碼,研究者還研發(fā)了一些從加殼后的Android應(yīng)用中抽取Dex代碼的工具,代表性的有DexHunter[206]和PackerGrind[207].這些分析輔助技術(shù)對(duì)提高移動(dòng)應(yīng)用分析工作的效能具有重要的意義.

3.2 并發(fā)軟件

自從計(jì)算機(jī)進(jìn)入并發(fā)處理時(shí)代,系統(tǒng)效率得到顯著提升.然而,并發(fā)程序(如多線程程序)的使用,導(dǎo)致并發(fā)問(wèn)題(或者并發(fā)缺陷)的存在且難以解決.其難點(diǎn)是:并發(fā)程序在運(yùn)行時(shí),多個(gè)任務(wù)之間的交替運(yùn)行空間巨大,而搜索該空間是NP難的.2007年圖靈獎(jiǎng)、2013年圖靈獎(jiǎng)、2016年哥德爾獎(jiǎng)等都授予了為解決并發(fā)問(wèn)題而做出突出貢獻(xiàn)的學(xué)者.他們提出的方法,例如模型檢驗(yàn)[208]工具,雖然已成功用于很多并發(fā)程序(算法)的驗(yàn)證,但是仍然無(wú)法應(yīng)用到大規(guī)模真實(shí)程序中,從而失去了實(shí)際意義.2000年以來(lái),多核處理器的快速發(fā)展使得大規(guī)模多線程程序被廣泛使用,尤其是近幾年來(lái),大數(shù)據(jù)、云計(jì)算、高性能計(jì)算等產(chǎn)品的應(yīng)用中,都使用了大量的基于線程的高并發(fā)處理,這進(jìn)一步加劇了并發(fā)缺陷的嚴(yán)重性.

由于多線程程序運(yùn)行時(shí)各個(gè)線程之間的交替執(zhí)行(interleaving)[209-212]使其具有不確定性,傳統(tǒng)的單線程程序的測(cè)試方法無(wú)法用于測(cè)試多線程程序以找出并發(fā)缺陷.即使某個(gè)并發(fā)缺陷被檢測(cè)到一次,也很難被再一次檢測(cè)到或重現(xiàn)這個(gè)缺陷[213].因此,多線程程序中并發(fā)缺陷的檢測(cè)變得比較困難.也因此,近年來(lái)并發(fā)缺陷的相關(guān)研究也非常熱門.

并發(fā)缺陷的檢測(cè)包括靜態(tài)分析[214-216]、動(dòng)態(tài)分析[217-221]以及二者結(jié)合的混合分析[222].靜態(tài)分析主要是檢測(cè)程序代碼(源代碼、中間代碼和二進(jìn)制代碼等)中是否存在特定模式(即那些可能導(dǎo)致并發(fā)缺陷發(fā)生)的同步以及資源的訪問(wèn).雖然靜態(tài)分析能夠通過(guò)分析給定程序中所有的代碼來(lái)達(dá)到很大的覆蓋面,但是由于缺乏程序運(yùn)行時(shí)的信息,尤其是多線程程序特有的交替運(yùn)行信息,其檢測(cè)結(jié)果是非常不準(zhǔn)確的[223].動(dòng)態(tài)分析則是依賴于程序的具體運(yùn)行去檢測(cè)并發(fā)缺陷,其檢測(cè)結(jié)果相對(duì)靜態(tài)分析會(huì)準(zhǔn)確很多.但是一個(gè)多線程程序的運(yùn)行依賴于其中所有線程的交替運(yùn)行,而這種交替運(yùn)行的空間是非常大的.因此,單次或有限次多線程程序的運(yùn)行很難覆蓋該程序的所有其他運(yùn)行情況[224].從而動(dòng)態(tài)分析只能找到給定程序運(yùn)行中的缺陷,包括潛在的缺陷.另外,動(dòng)態(tài)分析會(huì)引起程序運(yùn)行時(shí)的時(shí)間開銷,例如,在 C++程序上動(dòng)態(tài)分析數(shù)據(jù)競(jìng)爭(zhēng)時(shí),其時(shí)間開銷很容易達(dá)到原有程序運(yùn)行的100多倍[225].混合分析則是結(jié)合了靜態(tài)分析和動(dòng)態(tài)分析各自的優(yōu)點(diǎn),其首先通過(guò)靜態(tài)分析找出所有潛在的缺陷,然后通過(guò)動(dòng)態(tài)分析去驗(yàn)證這些潛在的缺陷是否為真實(shí)的缺陷[222].但是,這種分析方法又受制于測(cè)試用例的生成.亦即:即使靜態(tài)分析中檢測(cè)到的一個(gè)潛在的缺陷是真實(shí)缺陷,但是怎樣通過(guò)動(dòng)態(tài)分析去驗(yàn)證它.因?yàn)橐粋€(gè)缺陷的發(fā)生不僅取決于程序運(yùn)行過(guò)程中線程之間的交替,還取決于運(yùn)行該程序時(shí)相應(yīng)的輸入是否可以導(dǎo)致該缺陷的發(fā)生[226].另外,如果潛在缺陷的數(shù)量非常龐大,則其需要大量地運(yùn)行給定的程序才能確認(rèn)每個(gè)潛在的缺陷.

1) 全面調(diào)度技術(shù)

動(dòng)態(tài)分析依賴于程序的具體運(yùn)行來(lái)檢測(cè)并發(fā)缺陷,因此其無(wú)法檢測(cè)那些沒(méi)有運(yùn)行或者被隱藏的并發(fā)缺陷.引入隨機(jī)性則可以增加動(dòng)態(tài)分析的檢測(cè)能力.ConTest[227]在程序運(yùn)行時(shí)隨機(jī)加入噪音(例如隨機(jī)休眠某個(gè)線程一小段時(shí)間),使得一個(gè)程序在每次運(yùn)行時(shí),各個(gè)線程之間的交替產(chǎn)生差異.然而,這種差異只能導(dǎo)致很少的一部分并發(fā)缺陷被檢測(cè)到,無(wú)法讓那些很難檢測(cè)到的并發(fā)缺陷被檢測(cè)到.

PCT[228]和 RPro[229]是最新的兩種有概率保證的調(diào)度技術(shù).PCT可使一個(gè)程序按照事先產(chǎn)生的隨機(jī)調(diào)度運(yùn)行,而這些隨機(jī)調(diào)度在概率上可以保證動(dòng)態(tài)分析檢測(cè)到每一個(gè)并發(fā)缺陷.但是PCT需要非常多的運(yùn)行次數(shù),因?yàn)槠涓怕实谋ＷC是非常小的.因此,在規(guī)模稍大的程序上,PCT效果很差.RPro提出了缺陷半徑的概念,并結(jié)合實(shí)際,使其每次產(chǎn)生的調(diào)度只會(huì)在特定的程序運(yùn)行范圍內(nèi),從而極大地提高了缺陷的檢測(cè)概率.從另一個(gè)角度來(lái)說(shuō),PCT是RPro以程序運(yùn)行中所有事件數(shù)量為半徑時(shí)的一個(gè)特例.

2) 限定調(diào)度

完全探索一個(gè)并發(fā)程序所有可能的運(yùn)行空間是 NP難的.近年來(lái),研究人員提出了限定調(diào)度技術(shù)來(lái)緩解這一難題.CHESS[213]只完全遍歷程序中引發(fā)不確定運(yùn)行的事件,包括線程同步以及對(duì)volatile變量的訪問(wèn)等,且其只限定在給定的有限個(gè)調(diào)度點(diǎn)之內(nèi)的事件.SKI[230]也采用了類似的思路,在系統(tǒng)內(nèi)核中通過(guò)遍歷未知運(yùn)行來(lái)找到并發(fā)缺陷.Maple[231]通過(guò)定義一些已知的模式來(lái)預(yù)測(cè)程序運(yùn)行中的潛在并發(fā)錯(cuò)誤.但這類工作在實(shí)際中的效果也不是很好.例如,一項(xiàng)最新的研究表明[232],這些工作(包括部分全面調(diào)度技術(shù))還是會(huì)漏掉很多并發(fā)缺陷.

3) 啟發(fā)式調(diào)度

并發(fā)缺陷主要包括死鎖(deadlock)、數(shù)據(jù)競(jìng)爭(zhēng)(data race)和原子性違反(atomicity violation)[233].不同的缺陷通常會(huì)有一些特別的檢查方法.

針對(duì)數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè),FastTrack[234]舍棄了全面內(nèi)存訪問(wèn)追蹤,在保證可以在每個(gè)內(nèi)存上檢測(cè)到第1個(gè)競(jìng)爭(zhēng)的條件下,改進(jìn)了檢測(cè)效率.DrFinder[235]通過(guò)預(yù)測(cè)并反轉(zhuǎn)同步的方法,提高數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)的覆蓋面.CP[236]通過(guò)重新定義數(shù)據(jù)競(jìng)爭(zhēng)的方法在一次運(yùn)行中檢測(cè)到更多的數(shù)據(jù)競(jìng)爭(zhēng).但是這種方法只能保證在一個(gè)給定程序中只有一個(gè)數(shù)據(jù)競(jìng)爭(zhēng)時(shí)是正確的.RaceMob[222]通過(guò)在程序的用戶端來(lái)確認(rèn)給定的潛在數(shù)據(jù)競(jìng)爭(zhēng)哪些是真實(shí)的,但其仍然需要靜態(tài)分析來(lái)首先找到潛在的數(shù)據(jù)競(jìng)爭(zhēng)缺陷.為了解決動(dòng)態(tài)分析的時(shí)間開銷,各種采樣的方法被用于數(shù)據(jù)競(jìng)爭(zhēng)的檢測(cè)中.LiteRace[237]首先通過(guò)降低一個(gè)程序中經(jīng)常被調(diào)用的方法的監(jiān)控來(lái)減少時(shí)間開銷.Pacer[238]采用定期采樣的方法,使得采樣率和數(shù)據(jù)競(jìng)爭(zhēng)的檢測(cè)率保持線性關(guān)系.Carisma[239]進(jìn)一步對(duì) Java程序中同一代碼產(chǎn)生的變量進(jìn)行采樣,其在采樣率很低時(shí),數(shù)據(jù)競(jìng)爭(zhēng)的檢測(cè)效果較好.采樣分析雖然減少了時(shí)間開銷,但也降低了數(shù)據(jù)競(jìng)爭(zhēng)的檢測(cè)數(shù)量,并且無(wú)法克服動(dòng)態(tài)分析漏報(bào)的缺點(diǎn).DataCollider[240]通過(guò)靜態(tài)采樣(代碼級(jí)別的采樣)來(lái)檢測(cè)數(shù)據(jù)競(jìng)爭(zhēng).其不但保證采樣率和數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)率的線性關(guān)系(與 Pacer類似),而且時(shí)間開銷比 Pacer更少.但是DataCollider只能檢測(cè)到特定類型的數(shù)據(jù)競(jìng)爭(zhēng),即:兩次訪問(wèn)中,寫操作數(shù)和另外一個(gè)讀或者寫操作數(shù)不一致的數(shù)據(jù)競(jìng)爭(zhēng).RaceFuzzer[241]在每一個(gè)潛在數(shù)據(jù)競(jìng)爭(zhēng)發(fā)生的位置去調(diào)度(例如主動(dòng)暫停)相關(guān)的線程來(lái)判斷這個(gè)潛在的數(shù)據(jù)競(jìng)爭(zhēng)是否會(huì)被觸發(fā).只有那些被觸發(fā)的數(shù)據(jù)競(jìng)爭(zhēng)才會(huì)被報(bào)告出來(lái).這種方法在一定程度上會(huì)檢測(cè)到更多的數(shù)據(jù)競(jìng)爭(zhēng),但其檢測(cè)能力仍然受制于所使用的調(diào)度算法.簡(jiǎn)單的調(diào)度并不會(huì)增強(qiáng)數(shù)據(jù)競(jìng)爭(zhēng)的檢測(cè)能力,而復(fù)雜的調(diào)度很難開發(fā).這一點(diǎn)不僅僅針對(duì)于數(shù)據(jù)競(jìng)爭(zhēng)的檢測(cè),在死鎖等的檢測(cè)上也是如此[217,242].Huang等人[243]最近提出了干擾程序運(yùn)行時(shí)的控制流來(lái)檢測(cè)到更多的數(shù)據(jù)競(jìng)爭(zhēng)的方法.這種方法需要針對(duì)每一個(gè)潛在的數(shù)據(jù)競(jìng)爭(zhēng)來(lái)解決相應(yīng)的約束條件,使其在潛在數(shù)據(jù)競(jìng)爭(zhēng)很多的時(shí)候,無(wú)法快速地解決相應(yīng)的約束條件.CRSampler[244]采用了一種新型的針對(duì)硬件采樣的數(shù)據(jù)競(jìng)爭(zhēng)定義方法,使其可以在時(shí)間開銷很低的情況下有效地檢測(cè)已部署程序中的數(shù)據(jù)競(jìng)爭(zhēng).AtexRace[245]則是一個(gè)針對(duì)跨運(yùn)行和跨線程的數(shù)據(jù)競(jìng)爭(zhēng)采樣技術(shù),在大量測(cè)試用例條件下,其可以減少整個(gè)測(cè)試的時(shí)間開銷.

原子性違反檢測(cè)的難點(diǎn),首先是如何確定程序中的內(nèi)存訪問(wèn)應(yīng)該是原子執(zhí)行的.一旦原子性區(qū)域被識(shí)別,其違反的檢測(cè)就會(huì)比較容易.AVIO[246]通過(guò)從正確運(yùn)行的程序中檢測(cè)單個(gè)變量上兩條訪問(wèn)指令上的原子性區(qū)域.MUVI[247]進(jìn)一步考慮多變量的內(nèi)存訪問(wèn)中的原子性區(qū)域.AtomFuzzer[248]直接假設(shè)每種方法中的內(nèi)存訪問(wèn)是原子性的.AtomTracker[249]首次提出了不需要原子性標(biāo)記且針對(duì)任意原子性區(qū)域、任意變量數(shù)下的原子性區(qū)域檢測(cè)方法.但是,AtomTracker需要運(yùn)行一個(gè)程序多次,且不能含有錯(cuò)誤運(yùn)行.

死鎖不同于數(shù)據(jù)競(jìng)爭(zhēng)和原子性違反,其涉及到線程之間的同步.同樣,死鎖一旦發(fā)生,則其很容易被檢測(cè)到.但是如何從一個(gè)沒(méi)有死鎖發(fā)生的程序中預(yù)測(cè)潛在死鎖,同樣是并發(fā)程序分析中的一個(gè)難題.其中的主要難題是如何高效地檢測(cè)死鎖.iGoodLock[242,250]提出了鎖依賴關(guān)系來(lái)表示程序中每個(gè)線程對(duì)鎖的獲取行為,并基于這些關(guān)系的集合來(lái)檢測(cè)死鎖.然而,在檢測(cè)過(guò)程中,由于需要生成大量的中間表示關(guān)系,iGoodLock會(huì)消耗很多內(nèi)存,導(dǎo)致其效率低下.MagicLock[250,251]被認(rèn)為是死鎖檢測(cè)方面截止目前最快的檢測(cè)方法.其將鎖依賴關(guān)系針對(duì)線程來(lái)分析存放,且提出了鎖依賴的等價(jià)關(guān)系與非等價(jià)關(guān)系以及一系列優(yōu)化措施,使得死鎖的檢測(cè)效率大為提高.

4) 消除誤報(bào)與漏報(bào)

并發(fā)缺陷的檢測(cè)通常會(huì)有誤報(bào)[217,241].近年來(lái),主動(dòng)調(diào)度技術(shù)(active scheduling)被廣泛提及,并用于誤報(bào)消除.RaceFuzzer[241]和 AtomFuzzer[248]通過(guò)在有潛在缺陷的點(diǎn)插入調(diào)度點(diǎn),并通過(guò)隨機(jī)調(diào)度來(lái)觸發(fā)預(yù)測(cè)缺陷.DeadlockFuzzer[242]采用了類似的想法來(lái)觸發(fā)死鎖.這些技術(shù)都受制于 Thrashing,使其觸發(fā)概率不高.Conlock[217,252]和 ASN[253]通過(guò)產(chǎn)生約束以及并發(fā)缺陷觸發(fā)的必要條件來(lái)觸發(fā)死鎖,在一定條件下,這兩種技術(shù)可以保證觸發(fā)真實(shí)死鎖.

另一方面,動(dòng)態(tài)分析必然產(chǎn)生漏報(bào),其中一個(gè)原因就是缺乏并發(fā)測(cè)試用例.ConTeGe[254]針對(duì) Java庫(kù)程序,提出了一種簡(jiǎn)單的包含兩個(gè)線程且針對(duì)單個(gè)共享變量的并發(fā)測(cè)試用例生成技術(shù).CovCon[255]進(jìn)一步考慮了并發(fā)覆蓋度,從而針對(duì)那些很少被覆蓋的代碼來(lái)生成(選擇)更多的測(cè)試用例.

3.3 分布式系統(tǒng)

隨著越來(lái)越多的數(shù)據(jù)與計(jì)算從本地向云端遷移,大規(guī)模分布式系統(tǒng)逐步得到廣泛使用,比如分布式存儲(chǔ)系統(tǒng)、分布式計(jì)算框架、同步服務(wù)、集群管理服務(wù)等.典型的大規(guī)模分布式系統(tǒng)包括 HDFS、Hbase、Hadoop、Spark、ZooKeeper、Mesos、YARN等.與傳統(tǒng)的單機(jī)系統(tǒng)相比,大規(guī)模分布式系統(tǒng)具有較好的可擴(kuò)展性和容錯(cuò)能力,獲得同樣計(jì)算能力的成本較低.因此,分布式系統(tǒng)在應(yīng)對(duì)復(fù)雜業(yè)務(wù)場(chǎng)景以及單機(jī)無(wú)法完成的大規(guī)模計(jì)算任務(wù)時(shí)具有較大的優(yōu)勢(shì),已成為支撐大規(guī)模網(wǎng)絡(luò)應(yīng)用不可或缺的一部分.大規(guī)模分布式系統(tǒng)已在大型互聯(lián)網(wǎng)公司,如阿里巴巴、谷歌、百度等得到廣泛應(yīng)用.

大規(guī)模分布式系統(tǒng)必須管理大量分布式軟件組件、硬件及其配置,使得該類系統(tǒng)異常復(fù)雜.因而,大規(guī)模分布式系統(tǒng)不可避免地會(huì)發(fā)生故障,并影響到大量終端用戶,降低了它的可靠性和可用性[256].例如:2013年1月10日,由于一個(gè)客戶端與服務(wù)器的同步錯(cuò)誤,Dropbox故障超過(guò)15個(gè)小時(shí);2014年6月23與24日,Microsoft Lync與Exchange相繼故障,導(dǎo)致其部分用戶9小時(shí)無(wú)法訪問(wèn)郵件系統(tǒng);2017年2月,亞馬遜AWS服務(wù)宕機(jī),造成許多基于亞馬遜云服務(wù)的互聯(lián)網(wǎng)應(yīng)用無(wú)法正常工作.因此,分布式系統(tǒng)中缺陷理解、檢測(cè)及驗(yàn)證技術(shù)成為當(dāng)前研究的一個(gè)重點(diǎn).

1) 分布式系統(tǒng)中缺陷的實(shí)證研究

近年來(lái),為了提高復(fù)雜分布式系統(tǒng)的可靠性,研究人員對(duì)分布式系統(tǒng)中的各種缺陷進(jìn)行實(shí)證研究以加深對(duì)這些缺陷的理解.CBS[257]針對(duì)6個(gè)開源分布式系統(tǒng)(Hadoop MapReduce、HDFS、Hbase、Cassandra、ZooKeeper和 Flume)中 3 655個(gè)致命缺陷進(jìn)行綜合性分析研究,詳細(xì)總結(jié)了分布式系統(tǒng)中出現(xiàn)的各種缺陷類型,包括可靠性、性能、可用性、安全性、可擴(kuò)展性等方面的缺陷,并形成一個(gè)開放的分布式系統(tǒng)缺陷數(shù)據(jù)集.但是,CBS沒(méi)有對(duì)分布式系統(tǒng)中不同類型的缺陷進(jìn)行深入分析,比如缺陷模式等.因此,后續(xù)研究對(duì)分布式系統(tǒng)中特定類型的缺陷進(jìn)行深入分析.TaxDC[258]深入分析了 4個(gè)開源分布式系統(tǒng)(Cassandra、Hadoop MapReduce、HBase和ZooKeeper)中的104個(gè)并發(fā)相關(guān)缺陷.Dai等人[259]對(duì)11個(gè)常用的云服務(wù)系統(tǒng)中156個(gè)超時(shí)(timeout)相關(guān)缺陷進(jìn)行了分析,總結(jié)了若干超時(shí)相關(guān)缺陷模式.CREB[260]針對(duì)4個(gè)開源分布式系統(tǒng)(Cassandra、Hadoop MapReduce、HBase和ZooKeeper)中的103個(gè)與節(jié)點(diǎn)失效恢復(fù)相關(guān)的缺陷進(jìn)行了深入分析,總結(jié)了分布式系統(tǒng)中若干節(jié)點(diǎn)失效恢復(fù)相關(guān)的缺陷模式.Guo等人[261]對(duì)分布式系統(tǒng)中的惡性失效恢復(fù)行為進(jìn)行了歸類說(shuō)明,認(rèn)為失敗恢復(fù)應(yīng)該遵守?zé)o害準(zhǔn)則.Yuan等人[262]對(duì)發(fā)生在Cassandra、Hbase、HDFS、Hadoop MapReduce和Redis上的198個(gè)系統(tǒng)失效進(jìn)行了深入分析,理解分布式系統(tǒng)中的故障最終會(huì)演變?yōu)橛脩艨梢娛〉哪Ｊ?Wang等人[263]詳細(xì)分析了幾十萬(wàn)臺(tái)服務(wù)器上的 290 000個(gè)硬件失敗報(bào)告,發(fā)現(xiàn)了若干硬件失效模式.上述實(shí)證研究使得研究人員對(duì)分布式系統(tǒng)中不同類型的缺陷得到深入理解,為進(jìn)一步分析、檢測(cè)相關(guān)缺陷提供支撐.

2) 基于動(dòng)態(tài)/靜態(tài)分析的分布式系統(tǒng)缺陷檢測(cè)

由于分布式系統(tǒng)的復(fù)雜性,很少有動(dòng)態(tài)/靜態(tài)分析工具直接檢測(cè)分布式系統(tǒng)特有的缺陷,比如由于消息引起的并發(fā)缺陷、節(jié)點(diǎn)失效引起的缺陷、超時(shí)相關(guān)缺陷等.得益于近年來(lái)對(duì)分布式系統(tǒng)中缺陷的深入分析,開發(fā)人員構(gòu)建了一系列新的開發(fā)工具.DCatch[264]將分布式系統(tǒng)中并發(fā)缺陷歸結(jié)為節(jié)點(diǎn)本地的內(nèi)存訪問(wèn)沖突問(wèn)題.DCatch通過(guò)記錄一次正確的執(zhí)行中的關(guān)鍵事件(節(jié)點(diǎn)交互消息),建立起分布式系統(tǒng)中事件之間的偏序關(guān)系,靜態(tài)地對(duì)這些事件進(jìn)行分析,識(shí)別并發(fā)的內(nèi)存訪問(wèn)沖突,發(fā)現(xiàn)可能的分布式系統(tǒng)并發(fā)缺陷.FCatch[265]識(shí)別在發(fā)生節(jié)點(diǎn)失效情況下可能的沖突操作,自動(dòng)地預(yù)測(cè)與節(jié)點(diǎn)故障事件相關(guān)的缺陷.Aspirator[262]基于發(fā)現(xiàn)異常處理錯(cuò)誤的缺陷模式,開發(fā)了一個(gè)基于規(guī)則的靜態(tài)檢查器,發(fā)現(xiàn)不恰當(dāng)?shù)漠惓Ｌ幚頇C(jī)制導(dǎo)致的系統(tǒng)失效.D3S[266]通過(guò)在運(yùn)行時(shí)檢查系統(tǒng)是否違反開發(fā)者指定的分布式屬性斷言來(lái)發(fā)現(xiàn)可能的問(wèn)題,并提供導(dǎo)致問(wèn)題的狀態(tài)序列來(lái)幫助開發(fā)者更快地解決問(wèn)題.Xu等人[267]結(jié)合源代碼分析和信息檢索來(lái)解析控制日志,構(gòu)建復(fù)合特征,然后使用機(jī)器學(xué)習(xí)的方法來(lái)分析這些特征,自動(dòng)地檢測(cè)系統(tǒng)運(yùn)行中的問(wèn)題.Dinv[268]利用靜態(tài)和動(dòng)態(tài)的程序分析方法來(lái)自動(dòng)地推斷分布式系統(tǒng)中不同節(jié)點(diǎn)上變量之間的關(guān)系,從而幫助開發(fā)者揭露系統(tǒng)在運(yùn)行時(shí)應(yīng)當(dāng)滿足的屬性.為了簡(jiǎn)化失效重現(xiàn)場(chǎng)景,DEMi[269]通過(guò)動(dòng)態(tài)偏序推理[270]和Delta debugging[271]來(lái)自動(dòng)地削減分布式系統(tǒng)的錯(cuò)誤執(zhí)行序列,從而定位錯(cuò)誤.

3) 分布式系統(tǒng)驗(yàn)證與模型檢驗(yàn)

大規(guī)模分布式系統(tǒng)由數(shù)量眾多的計(jì)算節(jié)點(diǎn)組成,運(yùn)行不同的復(fù)雜協(xié)議.建立可驗(yàn)證的分布式系統(tǒng)是避免錯(cuò)誤的一個(gè)重要手段.Verdi[272]、IronFleet[273]和Chapar[274]通過(guò)利用證明框架Coq和TLA來(lái)建立可驗(yàn)證的分布式系統(tǒng)協(xié)議.IronFleet結(jié)合TLA風(fēng)格的狀態(tài)機(jī)精煉和霍爾邏輯驗(yàn)證來(lái)構(gòu)建實(shí)際的且能被證明正確的分布式系統(tǒng).Verdi通過(guò)對(duì)各種網(wǎng)絡(luò)語(yǔ)義和不同的故障進(jìn)行規(guī)范化,使得開發(fā)者在驗(yàn)證分布式系統(tǒng)實(shí)現(xiàn)時(shí)可以選擇最合適的故障模型.比如,首先在一個(gè)理想化的故障模型上進(jìn)行驗(yàn)證,再將得到的正確性保證轉(zhuǎn)移到一個(gè)更加現(xiàn)實(shí)的故障模型上.Chapar利用Coq和Ocaml,模塊化地驗(yàn)證Key-value存儲(chǔ)實(shí)現(xiàn)及客戶端程序的因果一致性.但是,通過(guò)驗(yàn)證方法,以較小的性能開銷來(lái)構(gòu)建可驗(yàn)證的、真實(shí)的大規(guī)模系統(tǒng)還有一定困難.當(dāng)前的研究也發(fā)現(xiàn),形式化驗(yàn)證過(guò)的分布式系統(tǒng)實(shí)現(xiàn)依然不是完全可靠的[275].

模型檢驗(yàn)是分析現(xiàn)存分布式系統(tǒng)可靠性的重要手段.MODIST[276]系統(tǒng)化分析分布式系統(tǒng)在所有可能事件下的響應(yīng).利用模型檢驗(yàn)的方法檢測(cè)分布式系統(tǒng)往往需要應(yīng)對(duì)巨大的狀態(tài)空間.DEMETER[277]利用分布式系統(tǒng)的模塊具有良好定義接口的特性,對(duì)接口行為進(jìn)行抽象,從而大大縮減了狀態(tài)空間.SAMC[278]攔截分布式系統(tǒng)中的不確定性事件并交換它們的順序.SAMC采用灰盒測(cè)試技術(shù),在傳統(tǒng)黑盒模型檢驗(yàn)的基礎(chǔ)上加入分布式系統(tǒng)的語(yǔ)義信息,從而縮減了狀態(tài)空間,盡可能地避免模型檢驗(yàn)中的狀態(tài)爆炸問(wèn)題.SDE[279]開發(fā)了一種新的算法,能夠顯著地消減測(cè)試中的冗余狀態(tài),使得對(duì)分布式系統(tǒng)進(jìn)行可擴(kuò)展的符號(hào)執(zhí)行成為可能.

4) 基于失效注入的分布式系統(tǒng)分析技術(shù)

在分布式系統(tǒng)中,計(jì)算節(jié)點(diǎn)可能由于硬件、斷電、操作系統(tǒng)錯(cuò)誤等發(fā)生失效.分布式系統(tǒng)需要從節(jié)點(diǎn)失效中正確恢復(fù),以保證系統(tǒng)的正確性.但是由于節(jié)點(diǎn)失效時(shí)機(jī)、失效恢復(fù)過(guò)程難以測(cè)試,研究人員開發(fā)了一系列工具分析分布式系統(tǒng)的失效恢復(fù)行為.SETSUD[280]利用對(duì)系統(tǒng)內(nèi)部狀態(tài)的感知來(lái)精確地控制擾動(dòng)的時(shí)序,暴露分布式系統(tǒng)中系統(tǒng)層面的缺陷.PreFail[281]是一個(gè)可編程的失敗注入工具,允許用戶自定義失敗注入策略.FATE and DESTINI[282]通過(guò)避免測(cè)試相同的恢復(fù)行為來(lái)盡可能地測(cè)試多種多樣的失敗場(chǎng)景.用戶可以通過(guò)Datalog來(lái)描述故障測(cè)試方法以及分布式系統(tǒng)恢復(fù)規(guī)范,從而系統(tǒng)化測(cè)試分布式系統(tǒng)中故障恢復(fù)邏輯.PACE[283]通過(guò)系統(tǒng)地生成和探索分布式系統(tǒng)執(zhí)行中可能產(chǎn)生的文件信息,來(lái)檢測(cè)與所有副本同時(shí)失效相關(guān)的分布式系統(tǒng)漏洞.CORDS[284]通過(guò)注入文件系統(tǒng)錯(cuò)誤檢測(cè)分布式系統(tǒng)的失效恢復(fù)能力.MOLLY[285]采用譜系驅(qū)動(dòng)的故障注入方法來(lái)發(fā)現(xiàn)故障容忍的分布式數(shù)據(jù)管理系統(tǒng)中的缺陷.

3.4 二進(jìn)制代碼

二進(jìn)制分析是經(jīng)久不衰的研究話題.盡管越來(lái)越多的程序是用解釋型語(yǔ)言(Python、JavaScript等)編寫,但是它們?nèi)匀恍枰M(jìn)制程序來(lái)解釋執(zhí)行,或者通過(guò)即時(shí)編譯(JIT)技術(shù)轉(zhuǎn)換為二進(jìn)制代碼執(zhí)行.另一方面,傳統(tǒng)的操作系統(tǒng)等對(duì)性能要求較高的應(yīng)用仍然是以 C/C++等編譯型語(yǔ)言編寫.此外,物聯(lián)網(wǎng)中大量設(shè)備的計(jì)算資源有限,運(yùn)行的都是C等語(yǔ)言編寫的二進(jìn)制程序.再者,從安全的角度來(lái)講,二進(jìn)制程序中可能引入源碼中不存在的安全問(wèn)題,例如Thompson提出的編譯器后門問(wèn)題[286]、Xcode Ghost污染事件[287]等.

二進(jìn)制分析的首要任務(wù)是反匯編,即識(shí)別二進(jìn)制程序中的代碼和數(shù)據(jù),解析函數(shù)間調(diào)用關(guān)系,及函數(shù)內(nèi)的控制流圖.最直接的反匯編方法是線性掃描[288],通過(guò)逐條指令解碼的方式恢復(fù)代碼.更精確的方式是遞歸遍歷[289],根據(jù)指令的語(yǔ)義尋找下一條指令的位置并解碼.但是遞歸遍歷面臨著一個(gè)巨大的挑戰(zhàn):靜態(tài)分析無(wú)法準(zhǔn)確識(shí)別間接跳轉(zhuǎn)指令的跳轉(zhuǎn)目標(biāo).Cifuentes等人[290]基于程序切片技術(shù)將間接跳轉(zhuǎn)表進(jìn)行規(guī)范化表示,根據(jù)一些啟發(fā)式特征識(shí)別間接跳轉(zhuǎn)語(yǔ)句的目標(biāo).Kinder通過(guò)在(不完整)控制流圖上進(jìn)行數(shù)據(jù)流分析,進(jìn)而完善控制流圖,再迭代式地進(jìn)行數(shù)據(jù)流分析,逐步恢復(fù)程序的控制流圖[289,291].Xu等人[292]通過(guò)動(dòng)態(tài)分析識(shí)別間接跳轉(zhuǎn)的目標(biāo),并采用強(qiáng)制執(zhí)行的方式驅(qū)動(dòng)程序探索所有路徑,從而構(gòu)建相對(duì)完整的控制流圖.隨著人工智能技術(shù)的發(fā)展,研究人員也將深度學(xué)習(xí)技術(shù)應(yīng)用到反匯編中,例如,Shin等人[293]通過(guò)RNN識(shí)別二進(jìn)制程序中的函數(shù)邊界.然而,反匯編仍然是一個(gè)開放的難題,現(xiàn)有的方案仍然存在很多局限[294].

二進(jìn)制分析面臨的另一個(gè)難題是高級(jí)語(yǔ)義恢復(fù).恢復(fù)二進(jìn)制程序語(yǔ)義可以用于多種安全應(yīng)用,例如漏洞挖掘和安全防護(hù).與源碼程序不同,二進(jìn)制程序中大量信息缺失,例如函數(shù)和變量名、函數(shù)類型、數(shù)據(jù)結(jié)構(gòu)定義、虛函數(shù)調(diào)用與類信息等.Chua等人[295]采用自然語(yǔ)言處理類似的技術(shù)識(shí)別二進(jìn)制程序中的函數(shù)特征(參數(shù)類型及個(gè)數(shù)).Cifuentes等人[296]通過(guò)切片技術(shù)提取函數(shù)調(diào)用指令的操作數(shù)的規(guī)范化表示,根據(jù)啟發(fā)式特征識(shí)別虛函數(shù)調(diào)用點(diǎn).Reps等人[297]通過(guò)識(shí)別程序中靜態(tài)已知的全局地址、棧偏移等識(shí)別全局變量和棧變量,通過(guò)數(shù)據(jù)流分析識(shí)別間接內(nèi)存讀操作的返回結(jié)果等,實(shí)現(xiàn)對(duì)二進(jìn)制程序中的內(nèi)存訪問(wèn)操作語(yǔ)義的識(shí)別.Jin等人[298]通過(guò)過(guò)程間數(shù)據(jù)流分析,跟蹤this指針的流向,識(shí)別候選的類成員函數(shù)及變量,從而恢復(fù)二進(jìn)制程序中的C++對(duì)象.Lin等人[299]提出了一種基于動(dòng)態(tài)分析的數(shù)據(jù)結(jié)構(gòu)識(shí)別方法,對(duì)執(zhí)行過(guò)程中的變量賦予時(shí)間戳標(biāo)簽,進(jìn)而進(jìn)行前向和后向傳播分析,根據(jù)標(biāo)簽傳播到已知類型的使用位置,反推原始變量的類型和成員布局.Lin將同樣的思想應(yīng)用到內(nèi)核二進(jìn)制代碼中,可以識(shí)別內(nèi)核中的對(duì)象[300].

二進(jìn)制程序分析通常需要對(duì)二進(jìn)制程序進(jìn)行代碼插裝或改寫.主流有 3類二進(jìn)制插裝方案:在原始二進(jìn)制程序中直接靜態(tài)修改、將二進(jìn)制程序提升到中間表示中進(jìn)行修改或者在代碼執(zhí)行過(guò)程中動(dòng)態(tài)修改.第1類方案,靜態(tài)二進(jìn)制插裝,面臨的最大挑戰(zhàn)是反匯編的準(zhǔn)確率,基于不準(zhǔn)確的反匯編結(jié)果進(jìn)行代碼插裝可能導(dǎo)致程序執(zhí)行異常.Smithson等人[301]提出了一種兼容的方案 SecondWrite,通過(guò)保留未知的代碼段以及對(duì)間接跳轉(zhuǎn)指令進(jìn)行保守的指針轉(zhuǎn)換,確保二進(jìn)制程序改寫的正確性.UROBOROS[302,303]和 Ramblr[304]方案則通過(guò)將二進(jìn)制程序反匯編,進(jìn)而在匯編碼上進(jìn)行插裝,最后再組裝生成新的二進(jìn)制程序的方式進(jìn)行二進(jìn)制改寫.第 2類方案是通過(guò)將二進(jìn)制程序提升到中間表示IR上進(jìn)行修改,這類方案的優(yōu)點(diǎn)是插裝在 IR上完成,從而與二進(jìn)制的指令集無(wú)關(guān).Song等人提出的BitBlaze平臺(tái)[305]的VINE模塊通過(guò)將二進(jìn)制程序轉(zhuǎn)換為VEX中間表示完成分析和插裝.Brumley等人提出的BAP平臺(tái)[306]基于VINE提出了一個(gè)新的中間語(yǔ)言.第3類方案是在程序運(yùn)行時(shí)插裝,通過(guò)受控的執(zhí)行環(huán)境,在目標(biāo)基本塊、函數(shù)等執(zhí)行之前進(jìn)行插裝,經(jīng)典的方案包括 DynamoRIO[307]、Dyinst[308]、Valgrind[309]以及Intel PIN[310].

二進(jìn)制分析是許多安全分析的基礎(chǔ),具體的安全應(yīng)用場(chǎng)景包括漏洞挖掘、惡意代碼識(shí)別、安全防護(hù)等.在漏洞挖掘方面,二進(jìn)制分析方案通常通過(guò)匹配漏洞模式的方式來(lái)挖掘漏洞.Machiry等人[311]通過(guò)靜態(tài)分析掃描驅(qū)動(dòng)代碼,根據(jù)漏洞模式識(shí)別未知驅(qū)動(dòng)漏洞.Wang等人[312]提出了雙取漏洞的更精確的模型,進(jìn)而采用靜態(tài)分析在內(nèi)核中發(fā)現(xiàn)了多個(gè)雙取漏洞.Dewey等人[313]基于靜態(tài)分析識(shí)別虛函數(shù)調(diào)用點(diǎn),進(jìn)而基于可達(dá)性分析識(shí)別虛函數(shù)表溢出漏洞.在惡意代碼識(shí)別方面,大部分方案也是通過(guò)匹配惡意行為特征實(shí)現(xiàn)檢測(cè).Feng等人[189]通過(guò)靜態(tài)分析組件間的調(diào)用關(guān)系,與惡意代碼的特征進(jìn)行匹配,從而識(shí)別 Android惡意代碼.Kruegel等人[314]通過(guò)靜態(tài)分析內(nèi)核接口,識(shí)別正常調(diào)用所訪問(wèn)的內(nèi)核內(nèi)存,與目標(biāo)模塊所訪問(wèn)的內(nèi)核內(nèi)存進(jìn)行對(duì)比,從而發(fā)現(xiàn)內(nèi)核 rootkit.Bergeron等人[315,316]通過(guò)采用摘要技術(shù)和符號(hào)替換技術(shù),比對(duì)目標(biāo)代碼的特征與已知惡意代碼的抽象表示,從而識(shí)別混淆的惡意代碼.在安全防護(hù)方面,主流的二進(jìn)制方案是通過(guò)二進(jìn)制改寫部署新的安全策略.Padraig等人[317]通過(guò)二進(jìn)制改寫工具 SecondWrite對(duì)二進(jìn)制程序植入眾多經(jīng)典源碼層的防御方案,可以有效地保護(hù)歷史遺留的二進(jìn)制代碼.Wartell等人[318]通過(guò)靜態(tài)改寫二進(jìn)制程序,在程序加載時(shí)對(duì)代碼位置進(jìn)行隨機(jī)化,能夠有效緩解部分攻擊.他們提出了另外一個(gè)方案[319],通過(guò)對(duì)所有 API調(diào)用點(diǎn)植入安全檢查,自動(dòng)引入安全監(jiān)控器來(lái)增強(qiáng)二進(jìn)制程序安全性.Zhang等人[320]通過(guò)反匯編二進(jìn)制程序,并植入控制流完整性安全策略,可以有效地緩解控制流劫持攻擊.Batyuk等人[321]利用靜態(tài)分析評(píng)估了Android應(yīng)用中的惡意行為比例,并通過(guò)二進(jìn)制改寫緩解應(yīng)用中的惡意行為.Zhang等人[322]通過(guò)靜態(tài)分析識(shí)別虛函數(shù)調(diào)用點(diǎn),進(jìn)而通過(guò)二進(jìn)制改寫部署安全策略,極大地緩解了虛函數(shù)劫持攻擊.

4 討論與展望

程序分析是一項(xiàng)重要的基礎(chǔ)性技術(shù),它不僅能夠直接用于發(fā)現(xiàn)各類軟件中的缺陷、改進(jìn)軟件質(zhì)量,還可以在軟件測(cè)試、調(diào)試、維護(hù)以及缺陷預(yù)測(cè)等方面發(fā)揮作用,包括測(cè)試數(shù)據(jù)生成、軟件維護(hù)與程序理解、程序修復(fù)等.例如,軟件測(cè)試的一個(gè)重要問(wèn)題是:如何自動(dòng)構(gòu)造比較合適的測(cè)試數(shù)據(jù),從而達(dá)到一定的測(cè)試覆蓋率.Xu和Zhang[323]針對(duì)C程序的單元測(cè)試,采用符號(hào)執(zhí)行、約束求解與線性規(guī)劃等技術(shù),自動(dòng)構(gòu)造較小的測(cè)試數(shù)據(jù)集.在軟件調(diào)試方面,Wu等人提出了 ChangeLocator[324],在控制流分析和程序切片的基礎(chǔ)上,根據(jù)軟件崩潰報(bào)告自動(dòng)識(shí)別出引發(fā)崩潰的代碼變更(crash-inducing changes),從而幫助開發(fā)者較快地理解軟件崩潰的原因并找到解決方案.在自動(dòng)化程序修復(fù)方面,Gao等人[325]基于前述數(shù)據(jù)流分析技術(shù),通過(guò)建立合適的抽象域,自動(dòng)修復(fù)程序中的內(nèi)存泄漏并保證安全性;Xuan等人[326]基于動(dòng)態(tài)分析提取實(shí)時(shí)運(yùn)行值,將程序合成轉(zhuǎn)換為約束求解問(wèn)題,并應(yīng)用 SMT獲得可修復(fù)程序的代碼補(bǔ)丁.在缺陷預(yù)測(cè)方面,Briand等人[327,328]利用程序分析技術(shù)提取面向?qū)ο蟪绦蛑械膬?nèi)聚性和耦合性等特征,構(gòu)建定量模型,預(yù)測(cè)可能包含缺陷的類.

隨著新型軟件形式的出現(xiàn),程序分析技術(shù)也面臨一些新的問(wèn)題.下面針對(duì)新興的智能合約及機(jī)器學(xué)習(xí)軟件上的程序分析進(jìn)行討論.

4.1 面向智能合約的程序分析

最近數(shù)年,源自比特幣(bitcoin)的區(qū)塊鏈(blockchain)技術(shù)已成為各行各業(yè)關(guān)注的焦點(diǎn).區(qū)塊鏈可被認(rèn)為是一種分布式、去中心化的計(jì)算與存儲(chǔ)架構(gòu),除了支持?jǐn)?shù)字資產(chǎn)外,還能被用于商品溯源、信用管理乃至游戲等各種各樣的去中心化應(yīng)用(decentralized application,簡(jiǎn)稱DApp).為了方便DApp的開發(fā),一些基于區(qū)塊鏈技術(shù)的區(qū)塊鏈平臺(tái)應(yīng)運(yùn)而生,其中最為引人注目的是以太坊(Ethereum)[329].以太坊被認(rèn)為是一種可編程的區(qū)塊鏈,用戶可以在其上編寫和部署由智能合約(SmartContract)組成的DApp.目前,以太坊智能合約是最流行的DApp模式.

智能合約由Solidity語(yǔ)言開發(fā),被編譯為字節(jié)碼后在以太坊虛擬機(jī)EVM上運(yùn)行.由于智能合約可能承載著數(shù)額巨大的數(shù)字資產(chǎn),自然也成為了黑客的攻擊目標(biāo).針對(duì)智能合約的攻擊已經(jīng)造成了驚人的財(cái)產(chǎn)損失[330,331],研究人員開始探索通過(guò)軟件分析技術(shù)來(lái)檢測(cè)、驗(yàn)證智能合約的安全性.如在文獻(xiàn)[332,333]中,符號(hào)執(zhí)行技術(shù)被用于在字節(jié)碼層面檢測(cè)智能合約中的已知類型的潛在漏洞.此外,相對(duì)于傳統(tǒng)軟件,智能合約的體量較小(代碼一般為數(shù)十至數(shù)百行),使得對(duì)其使用形式化技術(shù)成為可能,涌現(xiàn)出多個(gè)智能合約驗(yàn)證系統(tǒng)[334-339].這些系統(tǒng)根據(jù)用戶給出的待驗(yàn)證屬性或斷言,采用模型檢驗(yàn)等技術(shù)來(lái)驗(yàn)證目標(biāo)合約的實(shí)現(xiàn)是否具有相關(guān)特性.與傳統(tǒng)軟件的分析相比,智能合約的分析在技術(shù)角度上并無(wú)太大不同,有的工作[334,338]甚至直接將智能合約代碼轉(zhuǎn)換為已有驗(yàn)證系統(tǒng)所能支持的形式,借助已有驗(yàn)證系統(tǒng)快速形成了對(duì)智能合約的分析能力.如在文獻(xiàn)[338]中,智能合約的Solidity代碼被轉(zhuǎn)換為 LLVM Bitcode,從而可以利用已有的分析和驗(yàn)證工具來(lái)驗(yàn)證智能合約.但是智能合約的分析工作也具有一些特殊性,突出表現(xiàn)為部署后的智能合約升級(jí)維護(hù)較為困難,難以像傳統(tǒng)軟件那樣隨意打補(bǔ)丁,使得人們特別期望能夠在部署前就發(fā)現(xiàn)所有的潛在問(wèn)題,這對(duì)智能合約分析系統(tǒng)的分析效能提出了很高的要求.目前,智能合約分析工作面臨的主要挑戰(zhàn)是如何有效地提供分析所需的安全模式或?qū)傩?這往往會(huì)同時(shí)涉及特定領(lǐng)域知識(shí)和程序驗(yàn)證知識(shí),僅僅依賴用戶提供并不現(xiàn)實(shí).此外,智能合約相關(guān)技術(shù)還處在進(jìn)化中,可能會(huì)涌現(xiàn)出新的應(yīng)用模式和新的安全問(wèn)題,需要持續(xù)不斷地跟蹤歸納.如何高效地提取分析所需的先驗(yàn)知識(shí),是一個(gè)非常有意義的研究問(wèn)題.

4.2 面向機(jī)器學(xué)習(xí)軟件的程序分析

近年來(lái),機(jī)器學(xué)習(xí)及其他智能技術(shù)在行業(yè)軟件中得到了廣泛的應(yīng)用,尤其是深度學(xué)習(xí)技術(shù)與工具在語(yǔ)音識(shí)別、圖像檢索、自動(dòng)駕駛等領(lǐng)域取得了較大突破.然而,由于廣泛存在的概率模型、多層傳播的復(fù)雜網(wǎng)絡(luò)結(jié)構(gòu)、黑盒形式的用戶接口等特性,深度學(xué)習(xí)工具的質(zhì)量難以度量.現(xiàn)有的軟件分析技術(shù)難以直接應(yīng)用.研究者提出了一系列程序分析方案用以發(fā)現(xiàn)機(jī)器學(xué)習(xí)系統(tǒng)的潛在風(fēng)險(xiǎn)和程序錯(cuò)誤,提升機(jī)器學(xué)習(xí)系統(tǒng)的質(zhì)量[340].Qin等人[341]提出了基于程序合成的機(jī)器學(xué)習(xí)系統(tǒng)的功能評(píng)估方法 SynEva,該方法通過(guò)學(xué)習(xí)場(chǎng)景的程序合成,用于評(píng)估機(jī)器學(xué)習(xí)系統(tǒng).Sun等人[342]提出了面向深度學(xué)習(xí)的動(dòng)態(tài)符號(hào)執(zhí)行方法,該符號(hào)執(zhí)行方法將測(cè)試需求表示為量化線性運(yùn)算(quantified linear arithmetic),以神經(jīng)元覆蓋為目標(biāo)測(cè)試深度神經(jīng)網(wǎng)絡(luò)的魯棒性.

在形式化驗(yàn)證方面,Gehr等人[55]提出將卷積神經(jīng)網(wǎng)絡(luò)轉(zhuǎn)化為CAT函數(shù),再使用抽象解釋技術(shù)對(duì)CAT函數(shù)的行為進(jìn)行上近似,從而驗(yàn)證對(duì)應(yīng)神經(jīng)網(wǎng)絡(luò)的局部魯棒性.Wang等人[56]設(shè)計(jì)了基于符號(hào)化區(qū)間的形式化驗(yàn)證方案,用來(lái)驗(yàn)證不適宜使用 SMT的屬性.Ruan等人[343]針對(duì)深度神經(jīng)網(wǎng)絡(luò),提出了基于可證明保障(provable guarantee)的可達(dá)性分析方法.Huang等人[344]提供了基于 SMT的深度神經(jīng)網(wǎng)絡(luò)的安全性驗(yàn)證方法.機(jī)器學(xué)習(xí)軟件往往依賴于復(fù)雜的數(shù)據(jù)處理.針對(duì)數(shù)據(jù)量過(guò)大難以調(diào)試的問(wèn)題,學(xué)術(shù)界也提出了若干方法.Ma等人[345]提出了LAMP,該方法用較低的開銷在基于圖的機(jī)器學(xué)習(xí)算法中記錄追蹤關(guān)系,以方便程序員定位缺陷.Gulzar等人[346]設(shè)計(jì)了一系列的調(diào)試算子,用于在基于 Spark的大數(shù)據(jù)分析程序中進(jìn)行低成本的交互式調(diào)試,而不必反復(fù)重啟整個(gè)計(jì)算過(guò)程.然而,由于機(jī)器學(xué)習(xí)技術(shù)的復(fù)雜特性,相對(duì)于傳統(tǒng)軟件的分析,機(jī)器學(xué)習(xí)軟件的靜態(tài)分析、動(dòng)態(tài)分析等方面都鮮見成果.針對(duì)深度學(xué)習(xí)工具的程序分析仍在起步階段.

5 結(jié)束語(yǔ)

程序分析是剖析復(fù)雜軟件系統(tǒng)、提高軟件質(zhì)量的重要手段,是軟件工程、程序設(shè)計(jì)語(yǔ)言、操作系統(tǒng)、信息安全等領(lǐng)域日益受到關(guān)注的研究方向.經(jīng)過(guò)多年的發(fā)展,程序分析已在多個(gè)方面取得了長(zhǎng)足的進(jìn)步.研究人員將程序語(yǔ)言理論與編譯、人工智能、數(shù)據(jù)處理等技術(shù)相結(jié)合,針對(duì)不同的軟件形態(tài)發(fā)展出眾多程序分析技術(shù),同時(shí)開發(fā)了高效率的自動(dòng)化分析工具,其中有些工具幫助人們?cè)陂_源軟件中找到了很多缺陷、漏洞,有些工具在大公司里得到應(yīng)用,并發(fā)揮了重要作用.由于篇幅所限,本文只是簡(jiǎn)述了該方向近期的一部分重要成果.

當(dāng)前,程序分析技術(shù)還面臨一系列挑戰(zhàn),比如準(zhǔn)確性、可擴(kuò)展性等.另外,新型的軟件形態(tài),如智能合約、深度學(xué)習(xí)等,也需要全新的程序分析技術(shù).隨著軟件應(yīng)用范圍的發(fā)展以及對(duì)軟件可靠性要求的提高,程序分析在軟件開發(fā)、維護(hù)過(guò)程中起的作用將越來(lái)越大.

致謝在本文寫作過(guò)程中,日本九州大學(xué)的趙建軍和國(guó)防科技大學(xué)的王戟提供了很多建設(shè)性意見,中國(guó)科學(xué)院軟件研究所的蘇靜和劉晴幫助整理了部分資料,在此一并感謝.