摘要：驱动程序是操作系统的重要组成部分。驱动程序运行于内核态,其可靠性对于操作系统的安全可靠非常关键。针对Linux驱动程序,研究基于符号执行的驱动程序缺陷自动检测方法。提出了基于性质制导符号执行的Linux驱动程序缺陷检测框架,以及多性质制导的符号执行方法,支持针对多个缺陷性质的快速缺陷检测。在LLVM和KLEE的基础上实现了提出的框架和方法,并在实际的Linux驱动程序上开展了初步实验。实验效果表明了所提方法和检测框架的有效性和高效性。

关键词：驱动程序 符号执行 缺陷检测 

单位：国防科学技术大学计算机学院; 湖南长沙410073