基于性质制导符号执行的Linux驱动程序缺陷检测研究
【出 处】:
【作 者】:
陈英杰
陈振邦
董威
国防科学技术大学计算机学院
湖南长沙410073
【摘 要】驱动程序是操作系统的重要组成部分。驱动程序运行于内核态,其可靠性对于操作系统的安全可靠非常关键。针对Linux驱动程序,研究基于符号执行的驱动程序缺陷自动检测方法。提出了基于性质制导符号执行的Linux驱动程序缺陷检测框架,以及多性质制导的符号执行方法,支持针对多个缺陷性质的快速缺陷检测。在LLVM和KLEE的基础上实现了提出的框架和方法,并在实际的Linux驱动程序上开展了初步实验。实验效果表明了所提方法和检测框架的有效性和高效性。
上一篇:一个基于两区间八边形约束的抽象域
下一篇:基于SAT求解器的故障树最小割集求解算法