使用符号化驱动环境检测Linux设备驱动程序的漏洞

J4 ›› 2016, Vol. 38 ›› Issue (02): 290-296.

使用符号化驱动环境检测Linux设备驱动程序的漏洞

徐永健1,2,王丹1,陈渝2,范文良2

(1.北京工业大学计算机学院,北京 100124；2.清华大学计算机科学与技术系,北京 100084)

收稿日期:2015-03-10 修回日期:2015-05-06 出版日期:2016-02-25 发布日期:2016-02-25
基金资助:
国家自然科学基金(61202074)

Symbolic device driver environment for
detecting bugs in Linux device driver

XU Yongjian1,2,WANG Dan1,CHEN Yu2,FAN Wenliang2

(1.School of Computer Science,Beijing University of Technology,Beijing 100124;
2.Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China)

Received:2015-03-10 Revised:2015-05-06 Online:2016-02-25 Published:2016-02-25

摘要/Abstract

摘要：

研究表明，驱动程序的漏洞是造成Linux系统安全问题的主要原因之一,可引发提权、拒绝服务等高危情况。针对无具体设备的情况下,无法对驱动程序进行运行时漏洞检测的问题,提出了对驱动程序进行符号化执行的思路,提出了一种基于符号执行技术实现的驱动程序模拟环境,可以用于分析和检测Linux设备驱动程序中存在的安全漏洞。该环境通过模拟内核提供给驱动程序的服务接口,使驱动程序可以在应用层进行符号执行进而可对其进行漏洞检测。同时,该环境无需真实硬件的支持,并且具备覆盖率高、执行速度快、易于扩展等特点。通过将该环境作用于6个不同的Linux设备驱动,检测出了6个真实的漏洞,其中三个漏洞已向驱动维护者提交补丁并被接受。实验结果表明，符号化驱动环境具备一定的漏洞检测能力,并且拥有资源消耗低、检测速度快和不依赖于硬件设备的特点。

关键词: 漏洞检测, 符号执行, Linux, 设备驱动

Abstract:

Studies have shown that driver vulnerability is one of the main causes of Linux security issues, which can lead to privilege escalation, denial of service and other highrisk situations. Considering the difficulty of driver vulnerability detection without real devices, this paper proposes symbolic execution of Linux drivers and implements the symbolic device driver environment (SDDE ), which can detect bugs in Linux device driver. The SDDE provides symbolic kernel services and symbolic devices, making symbolic execution of Linux driver and runtime driver vulnerability detection possible. The SDDE works without real hardware, and has high coverage, high performance and good scalability. The SDDE is applied to 6 Linux drivers, and we found six real bugs, three of which are confirmed by Linux developers.

Key words: bug detection, symbolic execution, Linux, device driver

徐永健1,2,王丹1,陈渝2,范文良2. 使用符号化驱动环境检测Linux设备驱动程序的漏洞[J]. J4, 2016, 38(02): 290-296.

XU Yongjian1,2,WANG Dan1,CHEN Yu2,FAN Wenliang2. Symbolic device driver environment for
detecting bugs in Linux device driver [J]. J4, 2016, 38(02): 290-296.

参考文献［15］

［1］	Yin Z,Ma X,Zheng J,et al.An empirical study on configuration errors in commercial and open source systems［C］∥Proc of the 23th ACM Symposium on Operating Systems Principles,2011:159172.
［2］	Tan L,Liu C,Li Z,et al.Bug characteristics in open source software［J］.Empirical Software Engineering,2014,19(6):16651705.
［3］	Palix N,Thomas G,Saha S,et al.Faults in Linux:Ten years later［J］.ACM SIGARCH Computer Architecture News,2011,39(1):305318.
［4］	Chen H,Mao Y,Wang X,et al.Linux kernel vulnerabilities:Stateoftheart defenses and open problems［C］∥Proc of the 2nd AsiaPacific Workshop on Systems,2011:5.
［5］	Amani S,Ryzhyk L,Donaldson A F,et al.Static analysis of device drivers:We can do better!［C］∥Proc of the 2nd AsiaPacific Workshop on Systems,2011:8.
［6］	Cadar C,Sen K.Symbolic execution for software testing:Three decades later［J］.Communications of the ACM,2013,56(2):8290.
［7］	Ball T,Levin V,Rajamani S K.A decade of software model checking with SLAM［J］.Communications of the ACM,2011,54(7):6876.
［8］	Beyer D,Henzinger T A,Jhala R,et al.The software model checker Blast［J］.International Journal on Software Tools for Technology Transfer,2007,9(56):505525.
［9］	Wang X,Chen H,Jia Z,et al.Improving integer security for systems with KINT［C］∥Proc of the 10th Symposium on Operating Systems Design and Implementation,2012:163177.
［10］	Ball T,Bounimova E,Levin V,et al.The static driver verifier research platform［C］∥Computer Aided Verification,2010:119122.
［11］	Beyer D,Petrenko A.Linux driver verification［M］∥Leveraging Applications of Formal Methods,Verification and Validation.Applications and Case Studies.Berlin:Springer,2012:16.
［12］	Trinity:A Linux system call fuzz tester ［EB/OL］.［20141001］.http:∥codemonkey.org.uk/projects/trinity/.
［13］	Cadar C,Dunbar D,Engler D R.KLEE:Unassisted and automatic generation of highcoverage tests for complex systems programs［C］∥Proc of the 8th Symposium on Operating Systems Design and Implementation,2008:209224.
［14］	Chipounov V,Kuznetsov V,Candea G.S2E:A platform for invivo multipath analysis of software systems［J］.ACM SIGARCH Computer Architecture News,2011,39(1):265278.
［15］	Renzelmann M J,Kadav A,Swift M M.SymDrive:Testing drivers without devices［C］∥ Proc of the 10th Symposium on Operating Systems Design and Implementation,2012:46.

[1]	王利1,2，王晶1,2，张伟功2,3，邱柯妮2,3，陆克中4. Linux内核参数对Spark负载性能影响的研究[J]. 计算机工程与科学, 2017, 39(07): 1219-1226.
[2]	陈英杰，陈振邦，董威. 基于性质制导符号执行的Linux驱动程序缺陷检测研究[J]. 计算机工程与科学, 2017, 39(04): 734-739.
[3]	蔡军，邹鹏，熊达鹏，何骏. 结合静态分析与动态符号执行的软件漏洞检测方法[J]. 计算机工程与科学, 2016, 38(12): 2536-2541.
[4]	范文良，茅俊杰，肖奇学，徐永健，杨维康，陈渝. 辅助检测Linux驱动中漏洞的符号驱动环境[J]. J4, 2015, 37(06): 1058-1063.
[5]	陈鲍孜，吴庆波，谭郁松. 应用协同的进程组内存管理支撑技术[J]. J4, 2014, 36(01): 57-62.
[6]	叶常春. 基于Linux的移动终端操作系统级虚拟化方案及优势[J]. J4, 2013, 35(5): 56-60.
[7]	李岗，糜元根. 一种支持B/S模式的网络摄像机的实现[J]. J4, 2012, 34(3): 108-112.
[8]	代子营,毛晓光,马晓东,王瑞. 基于抽象符号表的内存模型[J]. J4, 2011, 33(6): 84-90.
[9]	袁安富，夏生凤. 基于ARM和Linux的DM9000网络接口设计及驱动实现[J]. J4, 2011, 33(2): 27-31.
[10]	刘震宇,吴俊军. 一种基于微内核虚拟化的设备驱动优化模型[J]. J4, 2011, 33(12): 44-51.
[11]	苏曙光，曹华，刘云生. 基于μCLinux的操作系统实时性扩展和应用[J]. J4, 2010, 32(4): 125-127.
[12]	汪永琳. 基于IPv6的应用服务器的研究与实现[J]. J4, 2010, 32(12): 12-14.
[13]	蒋文芳1，赵利1，莫金旺2. AODV算法在视频监控系统中的应用与研究[J]. J4, 2010, 32(12): 157-160.
[14]	戴烨飞殳伟群. 基于Linux的游戏杆控制的实现方法[J]. J4, 2008, 30(7): 131-132.
[15]	柯伟李波. 基于μCLinux的车载仪表图形界面的设计[J]. J4, 2008, 30(3): 47-49.