基於定理證明的軟體脆弱性分析方法研究

《基於定理證明的軟體脆弱性分析方法研究》是依託南京大學，由曾慶凱擔任項目負責人的面上項目。

基本介紹

• 中文名：基於定理證明的軟體脆弱性分析方法研究
• 項目類別：面上項目
• 項目負責人：曾慶凱
• 依託單位：南京大學

項目摘要

根據軟體脆弱性分析的需求和技術發展，課題擬研究脆弱性程式語義、以及驗證條件生成和啟發式驗證等方法，從而形成基於定理證明的脆弱性分析框架，以支持對包含複雜數據結構和數據類型的大型軟體系統進行脆弱性分析。與模型檢測分析方法單純依賴脆弱性模型不同，本方法通過研究軟體脆弱性形成原理，在脆弱性的程式語義、驗證條件和驗證證明等方面，不僅考慮脆弱性模型特徵，而且引入軟體的安全策略因素，使之既能檢測脆弱性模型所表達的脆弱性，又能根據安全策略表達的約束檢測未建模的脆弱性。通過研究、利用脆弱性的原理和特徵，啟發脆弱性驗證過程的判定過程，結合語義推導、驗證條件生成和反例生成等自動化技術，大幅度提高脆弱性分析過程的自動化程度。研究分析推理的最佳化方法，進一步改善分析驗證過程。課題研究將在軟體安全性分析工具和安全軟體的設計開發等方面發揮積極的促進作用，並為軟體脆弱性的分類和建模等研究提供參考和依據。

結題摘要

本課題目標是研究基於定理證明的軟體脆弱性分析方法，以提高軟體的安全性。課題研究了脆弱性程式語義、驗證條件生成、啟發式驗證和最佳化方法，重點在程式脆弱性語義、驗證屬性生成、脆弱性檢測、啟發式驗證最佳化和脆弱性處理等方面開展了研究。研究了程式脆弱性語義，包括整數漏洞的建模、良性整數溢出的語義、並發執行緒的脆弱性描述、變數間的信息流分析等；研究了驗證屬性的提取方法，提出了程式循環不變式的改進生成方法；研究了各種脆弱性檢測方法，包括檢測IO2BO的動態跟蹤技術、基於數據流分析的整數符號錯誤檢測方法、基於信息流的整數漏洞驗證方法、Web注入型脆弱性檢測改進方法等；研究了啟發式驗證和最佳化方法，包括基於脆弱性知識的靜態分析指導漏洞檢測方法、基於脆弱性知識的檢測輸入評價方法、基於混合執行的漏洞檢測方法、LTL屬性分解方法等；探討了各種脆弱性利用和處理方法，包括基於循環的代碼復用攻擊、基於硬體的代碼復用攻擊檢測、脆弱性環境下記憶體保護、核心監控以及數據沙箱等方法。課題研究中，發表論文27篇，申請發明專利12項、獲得授權3項，開發了多個具有較好套用前景的軟體脆弱性檢測和安全保護工具。