作者簡介
高祥,北京航空航天大學(xué)軟件學(xué)院副教授。研究領(lǐng)域:程序分析、軟件自動修復(fù)、軟件安全。 ? ?
高效快速地修復(fù)軟件漏洞是增強(qiáng)軟件安全性的關(guān)鍵。然而,據(jù)統(tǒng)計,一個漏洞從發(fā)現(xiàn)到修復(fù)平均需要 60 天,這會讓軟件系統(tǒng)長期暴露在風(fēng)險中。自動程序修復(fù)是輔助開發(fā)人員修復(fù)程序缺陷的技術(shù)。現(xiàn)有的修復(fù)方法通常以通過給定的測試用例作為修復(fù)目標(biāo)。但是,測試用例驅(qū)動的修復(fù)技術(shù)易于產(chǎn)生“過擬合”的補(bǔ)丁,即修復(fù)后的程序在給定的測試用例上表現(xiàn)正確,但是在測試用例之外的輸入上仍然有錯誤。我將介紹如何使用程序分析技術(shù)緩解漏洞修復(fù)的過擬合問題。主要采用測試用例生成和形式化方法來增強(qiáng)程序規(guī)約,進(jìn)而提升自動化生成補(bǔ)丁的質(zhì)量。
以下為正文。
我們每個月都會發(fā)現(xiàn)很多的安全漏洞,然而安全漏洞的修復(fù)速度卻非常慢。據(jù)統(tǒng)計,一個安全漏洞從被發(fā)現(xiàn)到被修復(fù),大概要花費(fèi) 70 天的時間,即便是針對一些特別嚴(yán)重的安全漏洞,也需要花費(fèi)大概 50 天的時間來修復(fù)。
這種緩慢的修復(fù)速度會讓軟件長期暴露在安全的隱患中,我們的工作就是希望能夠自動化地生成程序漏洞的補(bǔ)丁,從而幫助開發(fā)人員盡快修復(fù)程序中缺陷。
對于人工修復(fù)來說,程序的修復(fù)往往需要定位異常、分析、修復(fù)這樣的過程。
人工程序修復(fù)
對于自動修復(fù)來說,我們希望把這個過程自動化。即給定一個程序的正確性規(guī)約 Specification,以及一個帶缺陷的程序,通過程序的自動修復(fù)系統(tǒng)來生成正確的程序。
自動化程序修復(fù)
# 程序修復(fù)方法
## 基于搜索的方法
現(xiàn)有的最簡單的程序修復(fù)方式之一是基于搜索的方法。
Search-based approach
首先定義程序的轉(zhuǎn)換規(guī)則,給定一個有錯誤的程序。利用給定的轉(zhuǎn)換規(guī)則,生成候選補(bǔ)丁的搜索空間。給定一組程序的正確性規(guī)約(假設(shè)是以 Test case 的形式給定)。程序修復(fù)的目標(biāo)是使得修復(fù)后的程序能夠通過所有的 Test case。
修復(fù)的過程是在搜索空間中通過某種搜索算法找到一個補(bǔ)丁,能夠通過所有的 Test case。
## 過擬合問題
基于搜索的方法最大的局限在于過擬合 Overfitting 問題。
Overfitting
給定一組 Test case,這組 Test case 表示的程序的正確性規(guī)約可能是不完善的,修復(fù)后的程序可能在給定的 Test case 上表現(xiàn)是正確的,但它沒有辦法泛化到其他的 Test case 上。
下面是一個簡單的例子,給定一個錯誤的測試用例,當(dāng)輸入是 1 的時候,期待的返回值是 1,但是在這個程序里面返回值是 0。那么如何用自動化的方式來生成一個正確的補(bǔ)丁?首先按照給定的轉(zhuǎn)換規(guī)則,對潛在的有錯誤的語句做轉(zhuǎn)換,比如 x - 1 > 0 → x - 2 > 0,x - 1 > 0 → x - 1 >= 0 等。
Overfitting
通過這種方式生成的程序,可能可以通過給定的 Test case,但它不一定能夠泛化到其他的 Test case 上。
# 如何緩解程序過擬合問題 #
下面介紹如何緩解在修復(fù)安全漏洞時的過擬合問題。主要是通過增強(qiáng)程序的正確性規(guī)約,并進(jìn)一步通過程序分析方法來推斷開發(fā)人員或用戶的意圖。我們用到的方法包括測試用例生成、基于邏輯推理的方法等。
研究如何緩解程序過擬合問題
今天我會介紹三個近期的工作。
# 生成測試用例
第一個工作是通過生成更多的測試樣例來緩解程序的過擬合問題。
既然過擬合的補(bǔ)丁無法泛化到其他的測試用例 test case 上,那么我們是否可以通過自動算法來生成更多的測試用例,再使用修復(fù)系統(tǒng)生成修復(fù)后的程序呢?
已有的用例生成工具主要以提升程序覆蓋率為目的,這類工具并不了解補(bǔ)丁的語義。因此目前的用例生成技術(shù),在我們的場景下其表現(xiàn)效果不是特別好。
Test Generation to Alleviate Overfitting
下圖中,假設(shè)最大的圈表示所有的補(bǔ)丁空間 search space,在補(bǔ)丁空間中有一些 plausible patches,這些 patches 能夠通過給定的測試用例,但它們不一定是正確的。在 plausible patches 里,可能只有一小部分是 correct patches。
Distinguish crashing and crash-free patches (practical)
我們的主要想法是通過測試用例生成,來區(qū)分出 plausible patches 里正確的和不正確的補(bǔ)丁。
在介紹具體的技術(shù)之前,我們先補(bǔ)充一下灰盒測試的背景。灰盒模糊測試 Grey-Box Fuzzing 以一組種子 seed (即測試用例) 作為輸入,測試引擎會基于給定的種子不斷修改來生成新的測試用例,并在程序上運(yùn)行這些新的測試用例,同時判斷新的測試用例是不是 isInteresting 的。在傳統(tǒng)的場景下,灰盒測試會判斷新測試用例是否提升了代碼的覆蓋率,如果有提升,就將其加入到 Input Queue 里,進(jìn)行進(jìn)一步的變異。但這種判斷方法對于補(bǔ)丁的語義是沒有任何理解的。
Grey-Box Fuzzing
為了解決這個問題,我們希望在用例判斷的過程中加入補(bǔ)丁的語義信息。例如,生成新測試用例時,先判斷測試用例有沒有發(fā)現(xiàn)候選補(bǔ)丁行為的差異,如果新測試用例發(fā)現(xiàn)了補(bǔ)丁之間行為的差異,則把該用例加到 Input Queue 里進(jìn)行變異。這樣做的最終目標(biāo)是通過不斷發(fā)現(xiàn)補(bǔ)丁之間行為的差異,從而區(qū)分出哪些補(bǔ)丁是正確的,哪些補(bǔ)丁是錯誤的。
Crash-avoiding Program Repair
## 舉個例子
下面介紹一個緩存溢出和數(shù)據(jù)泄露的例子。
如下代碼示例中,給定一個測試用例 s="foo", t="", n=4,運(yùn)行會觸發(fā)緩沖區(qū)溢出錯誤。
?
?
//?copy?the?first?n?characters?of?s?to?t char*?strncpy(char*?s,?char*?t,?int?n)?{ ????for?(int?i=0;?i?
?
我們假設(shè)通過轉(zhuǎn)換規(guī)則生成了一系列候選補(bǔ)丁。
?
ID Patch p1 i < n - 1 p2 i < 3 p3 i < n && i < strlen(s) p4 i > n ...... ...... ?
我們將補(bǔ)丁空間劃分為 Plausible partition 和 Incorrect patch (Plausible partition 即能夠通過給定測試用例的補(bǔ)丁,Incorrect patch 指仍然會觸發(fā)異常的補(bǔ)丁)。其中,Plausible partition 又可以劃分為 Crashing partition 和 Crash-free patch (Crashing partition 指雖然能夠通過給定的測試用例,但在一些其他的測試用例上仍然會觸發(fā)異常的補(bǔ)丁;Crash-free patch 是指正確的補(bǔ)丁)。
為了對 Plausible partition 進(jìn)行進(jìn)一步的劃分,可以通過測試用例生成的方法,對原有的測試用例進(jìn)行修改和變異。
?
ID Patch p1 i < n - 1 p2 i < 3 p3 i < n && i < strlen(s) ?
若新生成的測試用例能夠發(fā)現(xiàn)補(bǔ)丁之間行為的差異,那么就認(rèn)為基于此測試用例的進(jìn)一步變異,有更高的概率繼續(xù)發(fā)現(xiàn)補(bǔ)丁之間行為的差異。通過不斷生成測試用例,不斷劃分補(bǔ)丁分區(qū),最終找到正確的補(bǔ)丁。
## 實(shí)現(xiàn)方法
下面介紹具體的實(shí)現(xiàn)方法。
我們定義了 ,用以表示一個新生成的測試用例是否能夠發(fā)現(xiàn)補(bǔ)丁之間行為的差異:
Separability 有兩個作用,一是判斷一個新生成的測試用例是否是 isInteresting 的 (即 non-zero separability),若是,那么就進(jìn)行進(jìn)一步的變異。
第二是使用 Separability 來定義種子的能量值 Energy。能量值 Energy 指對一個種子進(jìn)行變異的次數(shù)。假設(shè)我們通過變異某個種子生成了 4 個新的測試用例,則其能量值為 4。擁有更高 separability 的種子會被分配更高的能量值。
不同時間和不同 separability 下能量值不同。
## 工具與實(shí)驗(yàn):Fix2Fit
基于上述方法,我們實(shí)現(xiàn)了一個開源工具 Fix2Fit,并與 AFL、AFLGo 進(jìn)行了對比。可以看到,F(xiàn)ix2Fit 相比 AFL 和 AFLGo 過濾掉了更多錯誤的補(bǔ)丁。
Percentage of plausible patches that are ruled out
更多 Fix2Fit 信息:
Github 地址:https://github.com/gaoxiang9430/Fix2Fit
相關(guān)論文:Crash-avoiding Program Repair Xiang Gao, Sergey Mechtaev, Abhik Roychoudhury. ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) 2019.## 思考:如何進(jìn)一步排除補(bǔ)丁
上述方法可以過濾掉 Crashing Patch,但實(shí)際上還有一些沒有引發(fā)安全隱患 (crash-free patch) 但依然是錯誤的補(bǔ)丁。怎樣去區(qū)分這部分補(bǔ)丁 (下圖中紅色部分) 和正確補(bǔ)丁呢?這需要開發(fā)者參與進(jìn)來。
我們假設(shè)通過一個測試用例,發(fā)現(xiàn)了兩個補(bǔ)丁的差異行為,那么在程序確定的前提下,其中只有一個補(bǔ)丁會是正確的,那么此時我們就需要人的反饋來過濾掉不正確的補(bǔ)丁。需要強(qiáng)調(diào)的是,我們的研究工作不是為了取代人,而是為了幫助開發(fā)者生成一些推薦,使開發(fā)者能夠更高效地修復(fù)問題。
如下所示,我們的實(shí)驗(yàn)中,如果有 5-10 次的人的參與反饋,那么我們可以從眾多的 plausible patches 中篩選到 10 個左右。
Number of plausible patches that can be ruled out if a few tests are empowered with more human oracles
# 程序狀態(tài)變異
我們發(fā)現(xiàn),如果從程序的入口處 entry point 開始對程序輸入進(jìn)行變異,會浪費(fèi)掉大量的資源,要到達(dá) patch location 是一件非常困難的事情。為了解決這個問題,我們提出,是否可以在補(bǔ)丁的位置直接進(jìn)行變異呢?我們叫這種在 patch location 進(jìn)行變異的方法為 State-level (Snapshot) Fuzzing,即對程序的狀態(tài)進(jìn)行變異。
Snapshot Fuzzing for repair
具體的方法是:
第一步,生成一些程序入口處的 Test Input ,針對每一個程序輸入,收集它在 patch location 的程序狀態(tài) ;
第二步,根據(jù)程序狀態(tài) 推斷程序補(bǔ)丁 ;
第三步,通過 Snapshot Fuzzing,對程序狀態(tài)進(jìn)行修改,生成一個新的狀態(tài) ,去測試推斷的補(bǔ)丁是否正確,同時也把新的狀態(tài)加入到狀態(tài)集合中 ;
返回第二步或者直接結(jié)束。
Snapshot Fuzzing 和傳統(tǒng) Test Generation 最大的區(qū)別在于,Snapshot Fuzzing 不是從程序的入口處對程序的輸入狀態(tài)進(jìn)行變異,而是在 patch location 直接變異。這是一個不斷循環(huán)的過程,最終的目標(biāo)就是不斷生成新的程序狀態(tài),同時不斷優(yōu)化程序的補(bǔ)丁。
## 實(shí)現(xiàn)方法
Patch Inference
那么,如何根據(jù)生成的程序狀態(tài)推斷一個補(bǔ)丁呢?這里用到了程序合成技術(shù)。
在程序狀態(tài) S 中,存在正樣本和負(fù)樣本。正樣本是指不能觸發(fā)安全事件的程序狀態(tài),負(fù)樣本是指能夠觸發(fā)安全事件的程序狀態(tài)。最終的目標(biāo)是推斷出一個程序補(bǔ)丁,使其在正樣本上原有的程序執(zhí)行保持不變,在負(fù)樣本上,需要對程序的狀態(tài)進(jìn)行修改,從而把漏洞狀態(tài)給關(guān)閉掉。
Patch Generation
生成程序補(bǔ)丁有兩種方式。一種是加入到原有的 if/for/while 中,另一種是插入一個 if-guard 關(guān)閉錯誤的程序狀態(tài)。
## 思考:Infeasible States
這里存在一個問題,雖然我們用直接修改的方式在程序中間生成了一個程序狀態(tài),但是這個程序狀態(tài)在真實(shí)的場景中不一定存在,即不一定是合法的。
針對這個問題我們也做了分析。如下圖所示,通過 Snapshot Fuzzing 生成的程序狀態(tài),可能是 infeasible state,但即使生成了 infeasible state,對于 disable vulnerable state 是沒有什么影響的。這主要因?yàn)椋摼€表示的橢圓有可能也 disable 了一些 infeasible state,但它對于最終的目標(biāo)是沒有任何影響的。
Snapshot mutation can generate infeasible states
## 工具與實(shí)驗(yàn):VulnFix
在本個實(shí)驗(yàn)中,我們使用了 AsiaCCS'21 的數(shù)據(jù)集,其中包含 39 個真實(shí)世界的安全漏洞。我們設(shè)置了 30 分鐘的超時機(jī)制。實(shí)驗(yàn)結(jié)果表明,VulnFix 可以成功修復(fù)其中的 19 個 漏洞,在已有的工具基礎(chǔ)上有了明顯的提升。
VulnFix generated more correct patches than CPR and SenX.
# 語義分析與推理
前面介紹的兩個工作,主要是基于 Fuzzing 的方式來緩解過擬合問題。雖然能夠在一定程度上緩解,但仍然沒有辦法保證生成的補(bǔ)丁能夠修復(fù)所有錯誤的 Test case。
為了解決這個問題,我們提出了一種 基于語義分析與推理方式修復(fù) 的方案。當(dāng)一個安全漏洞被發(fā)現(xiàn)時,通常會有一個能夠觸發(fā)安全漏洞的 Exploit (Failing Test),如果僅以修復(fù) Exploit 作為目標(biāo),很容易產(chǎn)生過擬合問題。
除了 Exploit 之外,可能還存在很多其他能觸發(fā)缺陷的程序輸入。那么,能否通過一種抽象的方式,將具體的 Exploit 抽象成一種針對所有 Failing Input 的表示?在這個場景下,我們使用抽象的條件約束 constraints 來表示一個缺陷,這樣修復(fù)的目標(biāo)就不再是使其通過測試用例,而是使其滿足給定的條件約束。
## 實(shí)現(xiàn)方法
生成條件約束
我們定義了一些模板,用以生成條件約束。比如,
buffer overflow:access(buffer) < base(buffer) + size(buffer)
Integer overflow/underflow (a op b):MIN ≤ a op b ≤ MAX (over Z)
下面是一個的 buffer overflow 的例子。假設(shè) rows 聲明的長度是 256,訪問時的 nrows 也是 256。根據(jù)約束 access(buffer) < base(buffer) + size(buffer) 可知,nrows 必須小于 rows,此時 buffer overflow 就會被觸發(fā)。
怎樣提取出程序狀態(tài)?
通過插樁和運(yùn)行時抽象的方法來提取抽象的條件約束。
在分配內(nèi)存的時候會同時記錄元數(shù)據(jù),包括 buffer 的大小、長度等,在運(yùn)行時參照元數(shù)據(jù)生成抽象的條件約束。
Concrete State Abstraction
約束傳遞
條件約束是在 bug location 生成的,稱之為 CFC。如果滿足 CFC,缺陷就會被修復(fù)。但問題在于,條件約束的生成是在 bug location,而修復(fù)的過程是在 fix location,這時候就需要向后的 CFC 的傳遞。
Constraints Propagation
計算一個在 fix location 針對于 CFC 的最弱前提條件 CFC',如果 CFC' 在 fix location 滿足,那么 CFC 在 bug location 也滿足。具體的計算過程我就不展開講了,我們用了一個向前的符號執(zhí)行來計算最弱的前提條件。
將固定位置的實(shí)時變量設(shè)置為符號變量
在固定位置和崩潰位置之間進(jìn)行符號執(zhí)行
用一個例子簡單介紹一下,假設(shè) fix location 在程序的第 2 行,bug location 在程序的第 6 行,CFC 在第 6 行要滿足約束 y>5。這時候要從第 2 行進(jìn)行程序的符號執(zhí)行,發(fā)現(xiàn)兩條程序執(zhí)行路徑,我們可以計算出第 6 行 CFC -> (y>5) 在第 2 行的最弱前提條件 CFC' -> (x>4 ? i>0) ? (x>6 ? i≤0)。
Patch Synthesis
最后一步就是需要在 fix location 生成一個補(bǔ)丁。生成補(bǔ)丁之后,CFC' 一定是被滿足的。這里其實(shí)是一個程序合成的問題,需要合成一個表達(dá)式,應(yīng)用了表達(dá)式之后,CFC' 一定是滿足的。具體的技術(shù)細(xì)節(jié)不展開了。
## 工具與實(shí)驗(yàn):ExtractFix
關(guān)于實(shí)驗(yàn),我們實(shí)現(xiàn)了工具 ExtractFix。在 30 個現(xiàn)實(shí)的 CVE 中,我們的工具能夠生成 24 個補(bǔ)丁,其中有 16 個和開發(fā)人員生成的補(bǔ)丁是一樣的。
Experiments with Existing CVEs
更多 ExtractFix 信息:
網(wǎng)站:https://extractfix.github.io/
論文:Beyond Tests: Program Vulnerability Repair via Crash Constraint Extraction. Xiang Gao, Bo Wang, Gregory J. Duck, Ruyi Ji, Yingfei Xiong, Abhik Roychoudhury. Transactions on Software Engineering and Methodology (TOSEM), 2020.# 總結(jié) #
總結(jié)一下,今天主要介紹了三個緩解安全漏洞修復(fù)時過擬合問題的方法。包括 Test case Generation、Snapshot Fuzzing、以及語義分析與推理。
還是需要強(qiáng)調(diào)一下,由于程序 oracle (期待的程序行為) 的缺失,這些方法并沒有徹底地解決過擬合的問題。因此我們只是提出了一些方法去緩解,最終的目標(biāo)也是幫助開發(fā)人員更高效的修復(fù)程序缺陷。
以上。
# 相關(guān)論文 #
Crash-avoiding Program Repair Xiang Gao, Sergey Mechtaev, Abhik Roychoudhury.?ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) 2019.
Beyond Tests: Program Vulnerability Repair via Crash Constraint Extraction. Xiang Gao, Bo Wang, Gregory J. Duck, Ruyi Ji, Yingfei Xiong, Abhik Roychoudhury.?Transactions on Software Engineering and Methodology (TOSEM), 2020.
編輯:黃飛
評論
查看更多