基于混合程序分析的驱动程序缺陷检测与验证研究

项目名称： 基于混合程序分析的驱动程序缺陷检测与验证研究

项目编号： No.61472440

项目类型： 面上项目

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 陈振邦

作者单位： 中国人民解放军国防科技大学

项目金额： 81万元

中文摘要： 由于驱动程序对运行环境的依赖性、运行层次的特殊性以及交互和逻辑的复杂性，驱动程序的质量保证非常困难，研究驱动程序的缺陷检测和验证对于提高系统软件的可靠与安全具有非常重要的意义。本项目将以国产化操作系统中的典型驱动为背景，结合近年来在程序分析、形式验证以及虚拟化等方向的最新进展，研究基于混合程序分析的自动高效驱动程序缺陷检测和关键性质验证机制和方法。具体研究内容包括：驱动程序缺陷特征分析与形式规约关键技术，以发现驱动程序的特征模式，建立面向驱动程序的多维规约方法；驱动程序符号执行可扩展性关键技术，能够面向性质引导符号执行的搜索过程，并结合程序抽象技术，削减路径空间；驱动程序符号执行可行性以及精度提升关键技术，支持可演化的环境建模，以及全系统的符号执行；最终建立自动化程度高的驱动程序缺陷检测和验证工具。本项目的研究能丰富和发展基于符号执行的混合程序分析方法，为提高设备驱动的质量提供有力支持。

中文关键词： 程序分析；符号执行；形式化规约；设备驱动；缺陷检测

英文摘要： Device drivers have the characteristics of heavily relying the environment, the specialty of the running mode and the complexity of communication and implementation. These characteristics make it very hard to ensure the correctness of device drivers. Therefore, the research for the method of bug finding and verification of device drivers is very important to improve the reliability and security of system software. Under the background of the device driver in domestically developed operating system, this project will investigate hybrid program analysis based automatic bug fining and verification mechanisms and techniques for device drivers. There are following research topics in this project: the bug features of drivers and the technique of formally specifying device drivers, which aim to find the bug patterns of drivers and develop the methods for formally specifying the critical properties of drivers in multi-dimensions; the techniques to improve the scalability of symbolic execution, which can guide the exploration of symbolic execution with respect to the properties to check or verify, and reduce the path space of symbolic execution by using program abstraction methods; the techniques to improve the feasibility and the precision of symbolic execution, which support evolvable environment modeling and in-vivo symbolic execution; the development of the highly automatic bug finding and verification tools for device drivers. The results of this project can promote symbolic execution based hybrid program analysis, and directly make contribution to improve the reliability of device drivers.

英文关键词： Program Analysis;Symbolic Execution;Formal Specification;Device Driver;Bug Finding