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