基于性质制导符号执行的Linux驱动程序缺陷检测研究  

Property guided symbolic execution based bug detection of Linux Drivers

作　　者：陈英杰[1] 陈振邦[1] 董威[1] 

机构地区：[1]国防科学技术大学计算机学院,湖南长沙410073

出　　处：《计算机工程与科学》2017年第4期734-739,共6页Computer Engineering & Science

基　　金：国家973计划(2014CB340703);国家自然科学基金(61472440;61632015;61272140)

摘　　要：驱动程序是操作系统的重要组成部分。驱动程序运行于内核态,其可靠性对于操作系统的安全可靠非常关键。针对Linux驱动程序,研究基于符号执行的驱动程序缺陷自动检测方法。提出了基于性质制导符号执行的Linux驱动程序缺陷检测框架,以及多性质制导的符号执行方法,支持针对多个缺陷性质的快速缺陷检测。在LLVM和KLEE的基础上实现了提出的框架和方法,并在实际的Linux驱动程序上开展了初步实验。实验效果表明了所提方法和检测框架的有效性和高效性。Device drivers constitute an important part of an operation system （OS）. The reliability of device drivers is critical to the security and reliability of OSs. We propose a property guided symbolic execution based framework for the bug detection of Linux device drivers. To analyze multiple properties simultaneously, we propose a multiple properties guided symbolic execution method. Based on the LLVM and KLEE, the framework and the property guided method are implemented. The results of the preliminary experiments on real world Linux drivers demonstrate the effectiveness and efficiency of the proposal.

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]