[發明專利]基于約束分析和模型檢驗的代碼安全漏洞檢測方法

有效

• 申請號: 200910086938.9
• 申請日: 2009-06-11
• 公開（公告）號: CN101571828A
• 公開（公告）日: 2009-11-04
• 發明（設計）人: 王雷;陳歸;趙朋超;張強
• 申請（專利權）人: 北京航空航天大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京科迪生專利代理有限責任公司
• 代理人: 李新華;徐開翟

1.基于約束分析和模型檢測的程序安全漏洞檢測方法，其特征在于：利用模型檢 測所具備的可達性分析，對經過約束分析提取后的程序緩沖區屬性約束模型進行可達性 判定，將安全漏洞檢測問題轉變為可達性判定問題，利用一階謂詞公理系統進行程序緩 沖區屬性約束模型求解，從而判斷和分析出安全漏洞以及引發路徑；所述安全漏洞為緩 沖區溢出漏洞；

模型檢測是一種驗證給定的系統是否滿足特定的性質的技術，給定一個待檢測的系 統和系統相關的性質描述，通過該系統執行模型檢測算法，可以證明此系統是否滿足給 定的性質，如果該系統不滿足給定的性質，該系統會給出以一個包含反例的錯誤報告； 所述模型檢測算法的輸入是系統相關的性質描述，如果給定的性質P滿足，表明對于給 定程序緩沖區的操作或變量的訪問是安全的；通過標準的編譯器前端分析，將針對指針、 數組的定義、指針引用、數組訪問以及危險函數的調用都添加了程序緩沖區屬性約束的 更新與斷言信息，如果程序緩沖區屬性約束的更新與斷言信息不成立，或者系統相關的 性質描述不成立，那么程序流會到達錯誤標簽ERROR，從而檢測出一個安全漏洞，所以 安全漏洞問題已經成功轉化為對錯誤標簽ERROR的可達性問題。

2.根據權利要求1所述的基于約束分析和模型檢測的程序安全漏洞檢測方法，其 特征在于，整個約束分析過程如下：

(1)將每個緩沖區與包含最大長度max_length和已用長度used_length的整數值 對相關聯，所述整數值對為相應緩沖區的屬性或屬性信息；

(2)將與緩沖區相關的語句和函數調用抽象為對緩沖區屬性信息的操作，包括屬性 傳遞和屬性驗證；

(3)通過步驟(1)(2)的分析建立關于程序緩沖區屬性的約束模型，用模型檢測算法 對程序緩沖區屬性約束模型進行求解，最終確定程序是否存在安全漏洞。

3.根據權利要求1所述的基于約束分析和模型檢測的程序安全漏洞檢測方法，其 特征在于：采用語法制導的方法，在GCC的抽象語法樹上進行約束分析，建立了一套針 對緩沖區溢出漏洞的約束分析機制，為緩沖區增加屬性長度信息，不同的緩沖區操作語 句對應于不同的屬性約束生成；為描述整個約束分析過程，首先對C語言進行抽象，分 析過程非流敏感的，不會處理控制流信息，為簡化分析將所關心的C語言語法進行抽象， 包括指針變量、整型變量、函數調用、內存分配以及賦值語句；根據這些語法抽象對緩 沖區的操作，生成相應的屬性處理語句，而生成規則是由xml配置文件給出，該文件將 直接指導緩沖區屬性模型的建立。

4.根據權利要求1所述的基于約束分析和模型檢測的程序安全漏洞檢測方法，其 特征在于：首先將緩沖區抽象為包含緩沖區最大長度和已用長度的整數值對，并稱其為 對應緩沖區的屬性，且將對緩沖區的各種操作抽象為對緩沖區屬性長度的操作，因此程 序是否存在安全漏洞需要驗證的性質P是：對于所有的緩沖區的操作，需驗證緩沖區最 大長度max_length＞＝緩沖區已用長度used_length是否成立，同時更新緩沖區的屬 性信息；利用模型檢測對程序緩沖區屬性約束模型進行性質P的驗證，從而判定安全漏 洞是否實際存在，并給出漏洞路徑。