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

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.