[發明專利]基于函數調用圖的并行化安全漏洞檢測方法

無效

• 申請號: 201110417105.3
• 申請日: 2011-12-14
• 公開（公告）號: CN102567200A
• 公開（公告）日: 2012-07-11
• 發明（設計）人: 王雷;王剛;王歡;陳歸;李康
• 申請（專利權）人: 北京航空航天大學
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F21/00
• 代理公司: 暫無信息
• 代理人: 暫無信息

技術領域：

本發明涉及一種源代碼漏洞的并行檢測方法。

背景技術：

隨著信息技術的發展，計算機軟件已經滲透到國民經濟的各個領域中，并與人們的生產生活息息相關。軟件的安全問題也越來越凸顯其重要性，一些關鍵軟件一旦遭到破壞，將會造成行業性乃至全國性的癱瘓。惡意的用戶可以針對特定軟件的錯誤，運行惡意的代碼從而得到訪問非法數據的權限。緩沖區溢出漏洞是目前這類安全漏洞中最主要的一種。惡意的用戶可以通過分析程序的輸入數據格式，并確定這些數據存放在程序的緩沖區中，這樣用戶就有可能通過特殊的輸入數據，將棧空間的敏感數據覆蓋掉，特別的將保存的返回地址替換為用戶自己定義的非法代碼的地址，這樣非法用戶就可以控制程序流程、執行非法操作。

軟件的漏洞可以通過靜態方法和動態方法進行檢測。靜態方法分為一般的靜態檢測方法和基于完備理論的形式化驗證方法，第一類主要是基于程序分析的方法檢查代碼中可能存在的漏洞；第二類方法則以形式邏輯、自動機理論為基礎，驗證程序是否具有某種性質。程序分析的方法不能夠對程序的所有狀態進行窮舉，因此精確度欠佳，模型檢測可以對所有程序的狀態進行窮舉，然而為了驗證一個短小程序的性質，需要搜索的程序狀態可能就非常龐大，因此純模型檢測的方法不能有效地進行漏洞檢測。目前比較有效的一種模型檢測方法是基于抽象-驗證-細化范例的軟件模型檢測方法，代表工具是加州大學伯克利分校研制的Blast，這種方法能夠適當忽略與安全漏洞屬性不相關的代碼，從而簡化了整個驗證過程。這不僅可以增加檢測出的漏洞數目而且可以減小誤報率，提高檢測精度。與靜態檢測方法不同的是，動態檢測技術對程序的規模沒有限制，可以對大型程序進行檢測，然而明顯的不足是動態檢測技術對輸入的依賴性，只有當特定的輸入使程序執行到危險點時，漏洞才會被發現，從而導致誤報率較高。

單純的模型檢測方法一般不能直接檢測程序的漏洞，比如Blast曾借助于Securd檢測程序中空指針的引用問題，但是不能檢測更復雜緩沖區操作的安全性。此外，在檢測大規模程序時，模型檢測方法會產生狀態空間爆炸問題。

發明內容：

本發明要解決的技術問題是：針對模型檢測方法會產生狀態空間爆炸問題，提出一種并行化模型檢測的方法來對緩沖區溢出漏洞進行驗證，目前該方法能夠實際地應用于大規模的程序以及嵌入式操作系統模塊中，并且具有減少狀態空間、低誤報率的優點。

本發明采用的技術方案是：基于函數調用圖的并行化安全漏洞檢測方法，其特征在于：通過分析待檢測程序的函數調用關系生成函數調用圖，查找出調用圖樹中的葉節點函數，再啟動并行化程序，同時利用模型檢測工具完成對葉節點函數的檢測，從而判斷和分析出安全漏洞以及引發路徑。

本發明采用基于函數和多線程的并行優化方法。首先，針對輸入的多文件模塊同時利用GCC的寄存器傳遞語言(RTL)特性分析出待檢測的模塊中各文件里的函數調用關系，此時，生成函數關系調用圖。然后，對函數關系調用圖進行分析，找到入度為零的函數節點(葉節點)。最后，對葉節點所在的文件進行預處理，啟動多線程并利用模型檢測工具BLAST對經過預處理的文件進行可達性驗證。

整個函數調用圖主要分如下幾個部分：

(1)調用圖生成模塊，此模塊完成函數調用關系圖的生成，通過生成待檢測文件模塊的函數的調用關系圖，可以方便地從底層函數開始分析和檢測，也可以方便地調度整個檢測過程；

(2)分析調度模塊，此模塊的任務是在調用圖的基礎上調度整個檢測過程，由于模塊文件間的獨立性，來自不同調用子樹的函數一般具有較小的相關性或者沒有相關性，可以方便對此類的函數進行并行檢測；

(3)預處理模塊，此模塊主要在GCC的抽象語法樹上進行約束分析，建立了一套針對緩沖區溢出漏洞的約束分析機制，為緩沖區增加屬性長度信息，不同的緩沖區操作語句對應于不同的屬性約束生成，已完成代碼插裝的過程，然后分析斷言assert的分布情況，為模型檢測模塊提供基礎；

(4)檢測模塊，此模塊使用模型檢測工具BLAST來完成經過預處理模塊處理后的文件，同時檢測系統啟動多線程進行檢測。

基于函數和多線程并行化的模型檢測最終是一種驗證給定的系統是否滿足特定的性質的技術。給定一個待檢測的系統和系統相關的性質描述，通過模型檢測算法的執行，算法可以證明此系統是否滿足給定的性質，如果系統不滿足給定的性質，系統會給出以一個包含反例的錯誤報告，從而檢測出一個安全漏洞，所以安全漏洞問題已經成功轉化為對錯誤標簽ERROR的可達性問題。

附圖說明：

圖1為本發明方法實施的結構圖解；