基於混合程式分析的驅動程式缺陷檢測與驗證研究

《基於混合程式分析的驅動程式缺陷檢測與驗證研究》是依託中國人民解放軍國防科技大學，由陳振邦擔任項目負責人的面上項目。

基本介紹

• 中文名：基於混合程式分析的驅動程式缺陷檢測與驗證研究
• 項目類別：面上項目
• 項目負責人：陳振邦
• 依託單位：中國人民解放軍國防科技大學

中文摘要

由於驅動程式對運行環境的依賴性、運行層次的特殊性以及互動和邏輯的複雜性，驅動程式的質量保證非常困難，研究驅動程式的缺陷檢測和驗證對於提高系統軟體的可靠與安全具有非常重要的意義。本項目將以國產化作業系統中的典型驅動為背景，結合近年來在程式分析、形式驗證以及虛擬化等方向的最新進展，研究基於混合程式分析的自動高效驅動程式缺陷檢測和關鍵性質驗證機制和方法。具體研究內容包括：驅動程式缺陷特徵分析與形式規約關鍵技術，以發現驅動程式的特徵模式，建立面向驅動程式的多維規約方法；驅動程式符號執行可擴展性關鍵技術，能夠面向性質引導符號執行的搜尋過程，並結合程式抽象技術，削減路徑空間；驅動程式符號執行可行性以及精度提升關鍵技術，支持可演化的環境建模，以及全系統的符號執行；最終建立自動化程度高的驅動程式缺陷檢測和驗證工具。本項目的研究能豐富和發展基於符號執行的混合程式分析方法，為提高設備驅動的質量提供有力支持。

結題摘要

由於運行環境的依賴性、運行層次的特殊性以及互動和邏輯的複雜性，以驅動程式為代表的軟體的質量保證非常困難，研究其缺陷檢測和驗證技術具有非常重要的意義。本項目研究基於混合程式分析的自動程式缺陷檢測和關鍵性質驗證機制和方法。主要研究內容包括：缺陷特徵分析與形式規約關鍵技術，符號執行可擴展和可行性關鍵技術，以及缺陷檢測和驗證工具。本項目的主要研究成果包括： （1）提出了面向正規性質的動態符號執行引導方法，能更快找到程式中滿足正規性質的路徑；研究了符號執行與隨機測試最優結合問題，給出了面向語句覆蓋率的最佳化結合算法，能更快提高程式覆蓋率；提出了面向浮點程式的熱點符號執行方法，以及基於求解開銷預測的符號執行搜尋策略，以提高浮點程式符號執行效率。 （2）提出了面向正規性質的程式路徑切片方法，在驗證過程中能削減更多的程式路徑；同時，提出了典型並行程式的符號化驗證方法，支持通用時序性質的驗證。 （3）實現了Linux驅動程式缺陷檢測工具、並行程式符號化驗證工具以及正規性質制導的Java程式動態符號執行工具。並對典型的軟體系統進行了實驗驗證，取得良好的效果。 本項目的研究能豐富和發展基於符號執行的混合程式分析方法，為提高以設備驅動為代表的軟體系統的質量保證提供有力支持。