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

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.

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

由于运行环境的依赖性、运行层次的特殊性以及交互和逻辑的复杂性，以驱动程序为代表的软件的质量保证非常困难，研究其缺陷检测和验证技术具有非常重要的意义。本项目研究基于混合程序分析的自动程序缺陷检测和关键性质验证机制和方法。主要研究内容包括：缺陷特征分析与形式规约关键技术，符号执行可扩展和可行性关键技术，以及缺陷检测和验证工具。本项目的主要研究成果包括：. （1）提出了面向正规性质的动态符号执行引导方法，能更快找到程序中满足正规性质的路径；研究了符号执行与随机测试最优结合问题，给出了面向语句覆盖率的优化结合算法，能更快提高程序覆盖率；提出了面向浮点程序的热点符号执行方法，以及基于求解开销预测的符号执行搜索策略，以提高浮点程序符号执行效率。. （2）提出了面向正规性质的程序路径切片方法，在验证过程中能削减更多的程序路径；同时，提出了典型并行程序的符号化验证方法，支持通用时序性质的验证。. （3）实现了Linux驱动程序缺陷检测工具、并行程序符号化验证工具以及正规性质制导的Java程序动态符号执行工具。并对典型的软件系统进行了实验验证，取得良好的效果。. 本项目的研究能丰富和发展基于符号执行的混合程序分析方法，为提高以设备驱动为代表的软件系统的质量保证提供有力支持。