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

计算机工程与科学

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

陈英杰，陈振邦，董威

（国防科学技术大学计算机学院,湖南长沙 410073）

收稿日期:2016-12-11 修回日期:2017-02-17 出版日期:2017-04-25 发布日期:2017-04-25
基金资助:
国家973计划（2014CB340703）；国家自然科学基金（61472440,61632015,61272140）

Property guided symbolic execution

based bug detection of Linux Drivers

CHEN Ying-jie，CHEN Zhen-bang，DONG Wei

（College of Computer,National University of Defense Technology,Changsha 410073,China）

Received:2016-12-11 Revised:2017-02-17 Online:2017-04-25 Published:2017-04-25

摘要/Abstract

摘要：

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

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

Abstract:

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.

Key words: drivers, symbolic execution, defect detection

陈英杰，陈振邦，董威. 基于性质制导符号执行的Linux驱动程序缺陷检测研究[J]. 计算机工程与科学.

CHEN Ying-jie，CHEN Zhen-bang，DONG Wei.

Property guided symbolic execution

based bug detection of Linux Drivers

[J]. Computer Engineering & Science.

[1]	赵玥, 肖梦燕, 邱宝军, 罗军, 王小强, 罗道军. 基于机器视觉的集成电路声扫图像缺陷检测软件设计[J]. 计算机工程与科学, 2023, 45(10): 1806-1813.
[2]	吴栋梁, 刘知贵, . 基于轻量化YOLOX的电子元器件缺陷检测方法研究[J]. 计算机工程与科学, 2023, 45(08): 1463-1471.
[3]	马美荣，李东喜. 基于RetinaNet的手机主板缺陷检测研究[J]. 计算机工程与科学, 2020, 42(04): 673-682.
[4]	周洲，黄茜，胡志辉. 基于显著性判别的缺陷检测方法[J]. 计算机工程与科学, 2018, 40(12): 2219-2223.
[5]	蔡军，邹鹏，熊达鹏，何骏. 结合静态分析与动态符号执行的软件漏洞检测方法[J]. 计算机工程与科学, 2016, 38(12): 2536-2541.
[6]	徐永健1,2,王丹1,陈渝2,范文良2. 使用符号化驱动环境检测Linux设备驱动程序的漏洞[J]. J4, 2016, 38(02): 290-296.
[7]	范文良，茅俊杰，肖奇学，徐永健，杨维康，陈渝. 辅助检测Linux驱动中漏洞的符号驱动环境[J]. J4, 2015, 37(06): 1058-1063.
[8]	贺延涛1，徐琪2，唐亮1，游晓明3. 基于纹理特征的磁片表面刀纹缺陷检测[J]. J4, 2012, 34(6): 88-92.
[9]	吴君钦，宋健，刘昊. 基于S3C6410和ADV7180的嵌入式视频采集系统设计与实现[J]. J4, 2012, 34(12): 115-119.
[10]	代子营,毛晓光,马晓东,王瑞. 基于抽象符号表的内存模型[J]. J4, 2011, 33(6): 84-90.
[11]	魏超苗克坚杨成果. 基于CPCI的ARINC429总线通信卡的WDM驱动程序开发[J]. J4, 2008, 30(10): 156-158.
[12]	褚亚铭吕强. 一个教学用操作系统的驱动扩展[J]. J4, 2006, 28(3): 126-127.
[13]	潘登[1] 刘光明[2]. EFI结构分析及Driver开发[J]. J4, 2006, 28(2): 115-117.
[14]	冯翔[1] 李仁发[1] 喻飞[2] 易非[1]. 嵌入式Linux中闪存设备驱动程序开发[J]. J4, 2005, 27(3): 96-98.
[15]	袁楚明胡志新陈幼平尹勇周祖德. 基于PCI总线的物理隔离卡WDM架构驱动程序开发[J]. J4, 2004, 26(8): 83-82.