辅助检测Linux驱动中漏洞的符号驱动环境

辅助检测Linux驱动中漏洞的符号驱动环境*

范文良，茅俊杰，肖奇学，徐永健，杨维康，陈渝

(清华大学计算机科学与技术系，北京 100084)

摘要：Linux系统中的驱动漏洞被证实是内核漏洞的主要来源，可以被利用导致严重的安全问题。通过系统模型、驱动与内核的交互和驱动与设备的交互这三部分的设计与实现，构建了符号驱动环境，用于辅助检测Linux驱动中的漏洞。使用符号驱动环境对两个真实的驱动进行检测，成功检测出了两个漏洞，证实了该工具的可行性。与SymDrive工具的性能相比，符号驱动环境执行速度快90%，覆盖率提高20%。

关键词：驱动漏洞；漏洞检测；符号执行；驱动环境

中图分类号：TP309.2 文献标志码：A

doi:10.3969/j.issn.1007-130X.2015.06.005

收稿日期：*2014-05-05;修回日期：2014-06-11

基金项目：国家自然科学基金资助项目(61170050)；核高基重大专项基金资助项目(2012ZX01039-004)

作者简介:

通信地址：100084 北京市清华大学FIT楼3-124

Address:Room 3-124,FIT Building,Tsinghua University,Beijing 100084,P.R.China

Symbolicdriverenvironment:atoolaidedtodetectLinuxdriverbugs

FANWen-liang,MAOJun-jie,XIAOQi-xue,XUYong-jian,YANGWei-kang,CHENYu

(DepartmentofComputerScienceandTechnology,TsinghuaUniversity,Beijing100084,China)

Abstract:It has been proved that Linux driver bugs are the major bug source of the whole system, which can lead to serious security problems.A tool called symbolic driver environment (SDE) is designed to detect Linux driver bugs, which consists of the system model,the interactions between driver and kernel, and the interactions between driver and device.Using SDE, we detect two real Linux drivers, and find two bugs. The results prove that the tool is feasible, and the speed is 90% faster and the coverage is 20% larger compared with an existing tool called SymDrive.

Keywords:driverbugs;detectbugs;symbolicexecution;driverenvironment

1引言

Linux是一个使用广泛的开源操作系统，由于每个用户都可以获得并分析Linux的源代码，再加上近年来Android系统(基于Linux)在移动端广泛使用，使得Linux系统的安全性面临着重大的挑战。近来很多研究表明，内核驱动程序(简称驱动)是内核漏洞的主要制造者。斯坦福大学的一项研究表明[1]，Linux驱动中的漏洞要比内核中的其余部分多3～7倍。在另一流行的操作系统Windows中，也有研究表明[2]，有27%的系统崩溃是由驱动所引起的，相比之下由内核本身引起的只有2%。这些都证明了安全驱动的重要性。

驱动中的漏洞类型有硬件依赖错误、API误用、竞争、申请释放不匹配、内存泄露、驱动接口误用、指针问题等。现有的漏洞检测工具主要分为：静态分析工具、符号执行工具和动态分析工具。使用现有的工具检测驱动中的漏洞存在以下问题：

(1)观测性：驱动误用内核接口的真正位置很难检测，这是由于大多数驱动对内核接口的误用不会立即导致系统崩溃，而是使系统处于不稳定的状态，在之后引发崩溃或异常行为。

(2)覆盖率：驱动中的漏洞通常会发生在一些很少见的状态中，传统的测试工具通常无法覆盖到这些状态，也就无法检测出这些漏洞。

针对上述问题，本文首先介绍了用于漏洞检测的三种主要方法：静态分析、符号执行和动态分析。然后，综合上述方法的特点，提出了辅助检测Linux驱动中漏洞的原型系统——符号驱动环境，改进了静态分析误报率高，动态分析依赖输入、难以定位漏洞位置、符号执行会引起路径爆炸的问题。最后，通过将符号驱动环境应用于Linux中的lp打印机驱动和e100网卡驱动，检测出两个真实存在的漏洞，验证了该原型系统的可行性，并通过与SymDrive的对比，表明了符号驱动环境执行速度更快，覆盖率更高。

2相关工作

2.1静态分析

静态分析是指在不运行代码的方式下，通过词法分析、语法分析、控制流分析等技术对程序代码进行扫描，验证代码是否满足规范性、安全性、可靠性、可维护性等指标的一种代码分析技术，近来静态分析越来越多地被应用到漏洞检测领域。静态分析十分快速，但误报率较高。静态分析工具有：麻省理工学院开发的KINT[3]，用于检测C语言源码中的整数溢出漏洞；伯克利大学开发的BLAST[4]，用于解决C语言源码中的可达性问题，即如何从程序入口点到达程序中的给定点；微软公司开发的SDV(StaticDriverVerifier)[5]，用于检测Windows驱动中的内核接口的正确使用。

SDV具有典型的代表性，其主要包括Windows系统的模型及驱动运行的模拟环境以及60余条内核接口的使用规则。SDV在系统模型中模拟运行驱动源码，在内核接口中通过规则检测对其的正确使用，最后输出错误报告。SDV通过检测规则来定义内核接口的正确使用，从而解决了驱动检测中观测性的问题。

微软公司使用SDV对大量驱动进行了检测并发现了120余个严重的漏洞，但SDV仍存在如下问题：首先，SDV是一个闭源工具，无法将其移植用于检测Linux驱动中漏洞；其次，SDV限于静态分析，难以分析函数指针以及用于内存检测等；最后，SDV虽能够覆盖到驱动调用内核接口失败的情况，但是对驱动中由于设备输入而引起的分支情况覆盖率很低。

2.2符号执行

符号执行技术在程序分析和漏洞检测方面有着广泛的应用，其原理是用符号作为输入，对程序进行解释执行，以此枚举出程序所有可能的执行情况。在解释执行的过程中，执行引擎将所有变量对应为一个包含代数运算及内存访问的表达式，表示该变量与输入符号的关系；当变量用于条件判断时，执行引擎枚举该条件为真和为假的两条分支路径，在每条路径上记录其被执行的条件(称为“路径约束”)，并独立地继续执行这两条路径。当需要给变量指定具体值时，使用求解器对约束表达式进行求解。符号执行举例如图1所示。

Figure 1　Example of symbolic execution 图1　符号执行例子

设x为符号值，在遇到x<5这一分支判断时，执行引擎会分支并形成两条路径，一条路径关于x的约束表达式是x<5，该路径继续执行判断体内的语句；另一条路径关于x的约束表达式是x≥5，该路径跳过判断体继续执行。判断体中的x<0同理。设sysFn函数中要输出x的值，求解器就会在x<5这一范围内给x赋随机值，比如0。

符号执行工具有：洛桑理工学院开发的S2E(SelectiveSymbolicExecution)[6]，是用于符号执行二进制代码的虚拟机；斯坦福大学开发的KLEE[7]，是用于解释执行LLVM[8]中间代码的平台。KLEE是具有代表性的符号执行引擎，使用执行状态来表示程序运行过程中某一时刻的状态，每一条执行状态代表一条路径，KLEE解释执行LLVM中间代码的过程实际就是执行状态发生变化的过程。KLEE只能对链接生成的目标文件进行符号执行分析，因此无法符号执行Linux系统，从而无法符号执行依赖于操作系统的Linux驱动。符号执行覆盖率很高，但是存在路径爆炸的问题：即路径数目呈指数型增长，最后导致内存耗尽。KLEE提供了一些限制手段来防止路径爆炸，如限制路径深度、限制最大路径分支数等。

2.3动态分析

动态分析是指在运行时监控程序行为、收集程序信息进行漏洞检测，一般通过构造特定的输入来触发漏洞。动态分析可以解决静态分析很难解决的问题，如指针、内存检测等，但动态分析需要很大的工作量来构造输入，由于观测性的问题，动态分析也很难定位驱动中漏洞的位置。动态分析往往和别的分析方法综合使用，检测效果较好的工具有：洛桑理工学院基于S2E开发的DDT[9]，用于检测Windows网卡驱动中的漏洞；威斯康辛大学基于S2E开发的SymDrive[10]，用于检测Linux驱动中的多种漏洞。

SymDrive的总体结构见图2。SymDrive是源码级的工具，首先使用源码转换工具CIL[11]对驱动源码进行插桩，来辅助动态符号执行，然后使用符号化设备来模拟硬件产生的输入，最后将驱动运行在QEMU虚拟机中执行检测。SymDrive提出并实现了符号化设备这一思想，其原理如下：首先，虚拟机可以发现并配置虚拟的符号化设备，然后加载合适的驱动；其次，当驱动需要设备提供输入时，符号化设备可以产生一系列符号值，来辅助驱动的符号执行，达到高覆盖率测试的目的。SymDrive的检测依赖CIL的源码插桩，通过在驱动的源代码中插入一些相应的规则，在动态执行到该检测点时验证当前路径能否通过该检测。这种检测方式比较准确，但由于其真实地执行代码，会花费大量的时间在内核执行上，所以执行时间通常很长；另外，由于符号化设备会产生大量的符号值，经常会造成路径爆炸，SymDrive提供了注释插件来规避这一问题。

Figure 2　Architecture of SymDrive 图2　SymDrive总体结构

3符号驱动环境

本文在SymDrive的符号化设备和KLEE符号执行的基础上，实现了符号驱动环境——辅助检测Linux驱动中漏洞的工具。符号驱动环境使用符号执行改进了SDV覆盖率低的问题，使用Linux系统模型解决了无法在KLEE中执行驱动的问题，使用内核接口和改进的符号化设备改进了SymDrive执行时间长和路径爆炸的问题。在符号驱动环境上可以通过定制系统行为来模拟驱动功能、支持不同类型驱动，以及添加检测规则来检测多种类型的漏洞。符号驱动环境的设计目的是为Linux驱动提供一个轻量级的运行环境，更充分地测试驱动代码，减少内核代码的执行时间，从而减少测试时间，提高代码覆盖率。

符号驱动环境具备以下特点：

(1)可定制性：不同类型的驱动的功能各不相同，如网卡驱动可用于发包、收包、查询网络参数，LED驱动可用于控制LED灯的亮、暗等。符号驱动环境通过系统模型管理操作系统主动调用驱动的流程，用户可以简单地通过定制系统模型来模拟驱动的功能，实现对不同类型驱动的支持，提高对驱动代码测试的覆盖率。

(2)可扩展性：符号驱动环境通过规则来检测漏洞，不同类型的漏洞需要有不同的检测规则，本文在符号驱动环境中添加了常见的如内存、锁等方面的检测规则。符号驱动环境还可以添加更多的检测规则，从而实现对更多类型漏洞的检测，提高了整个工具的扩展性。

符号驱动环境的结构如图3所示。符号驱动环境主要分为系统模型、驱动与内核的交互以及驱动与设备的交互三部分，其执行流程如下：首先，通过系统模型来主动调用驱动；然后，当驱动执行到内核接口时，通过简化的内核实现来完成相应的功能并执行检测；之后，当驱动需要与设备交互时，通过符号化设备来完成交互；最后，完成系统模型的调用逻辑之后，输出错误报告并使用求解器求解出可以触发漏洞的相关输入的具体值。

Figure 3　Architecture of symboilc driver environment 图3　符号驱动环境总体结构

3.1系统模型

系统模型用于模拟Linux系统对驱动调用的流程和完成驱动功能(如触发网卡驱动收包)，以达到可定制地执行各种类型驱动的目的。每一种类型的驱动都有其固定的调用模式，这一模式也反映在每类驱动都有一些固定的函数指针上，如表1所示(以e100网卡驱动为例)。

Table 1　 Some function pointers in e100 net driver( part)

下边以e100网卡驱动为例，说明定制了收、发包功能的系统模型的调用模式：首先，通过module_init()暴露的驱动函数开启驱动的注册，并调用probe和open函数指针完成驱动的注册；然后，调用ndo_start_xmit函数指针模拟实现发包的功能，模拟硬中断触发收包，调用驱动注册的中断处理函数完成收包的操作；最后，以与注册相反的顺序，调用close、remove函数指针和module_exit()暴露的函数来注销驱动。

以上就是定制了收、发包功能的网卡驱动的调用模式，这一调用模式能覆盖50%左右的网卡驱动函数，包括注册中读取设备配置信息等函数，发包、收包的主要函数，以及注销中释放内存、垃圾回收等函数。用户可以通过定制系统模型的调用模式，来实现对更多类型驱动的支持；也可以通过定制更多的功能，例如，模拟用户使用ifconfig查询网络参数的功能，来达到更高的代码覆盖率。这样设计的好处是用户可以通过定制系统模型来模拟特定场景和驱动功能，使测试更加灵活和自由，体现了符号驱动环境的可定制性。另外，系统模型的设计使得驱动可以链接成一个目标文件，从而在KLEE中进行符号执行分析。

3.2驱动与内核的交互

驱动通过使用内核提供的接口和结构，来辅助完成驱动自身的功能。例如使用kmalloc()函数来申请内存等。符号驱动环境中的内核接口主要提供功能上的实现及相应的检测规则。驱动中使用的内核接口可能会失败，一个鲁棒的驱动在这种情况下也不会简单地崩溃，而会尝试恢复或者停止工作并报告问题，符号驱动环境对这种情况也进行了模拟。本文设计了以下原则来实现内核接口：成功时，简化地实现Linux系统中原函数的功能；失败时，使用符号执行返回相应的失败值；在需要的地方添加检测规则来实现对漏洞的检测。

为了检测未进行任何改动的驱动源码中的漏洞，需要在符号驱动环境的内核接口中添加若干检测规则。针对各种类型的漏洞，可以实现不同的检测规则对其进行检测。以在spin_lock中实现的检测规则为例：

voidspin_lock(spinlock_t *a) {

if(a→flags !=unlock) {

klee_warning("doublelock ");

klee_stace_trace();

}

a→flags=lock;

}

当驱动调用spin_lock函数时，通过修改的内核结构spin_lock_t中状态变量来判断锁是否处于unlock状态，如果锁处于lock状态则报错；如果锁处于unlock状态则将其标记为lock状态，以便下次检测。spin_unlock中也会实现类似的规则。综合这两个函数中的规则可以检测出驱动中的doublelock和doublefree的漏洞。

这一设计原则的优势如下：简化实现内核接口功能，可以减少在内核中符号执行的时间，使整个测试更加快速。通过分支路径来模拟驱动调用内核接口失败的可能性，可以模拟出驱动在真实执行时很少发生但是很可能出问题的情况，提高了覆盖率。在内核接口中添加检测规则，可以精确定位到漏洞发生的位置，解决了可观测性的问题，同时体现了符号驱动环境的可扩展性。

3.3驱动与设备的交互

驱动通过设备的交互来获取设备的输入和对设备进行输出，本文根据SymDrive的思想，设计并改进了符号化设备来辅助完成这一交互，减少了不必要的符号值，改善了中断处理函数调用的次数，以及采用符号值具体化的策略来解决路径爆炸的部分问题。下边分三个部分进行具体说明。

3.3.1符号化I/O

驱动中的I/O主要分为端口I/O和内存映射I/O，其设计原则为：读操作返回符号值；写操作忽略。读操作返回符号值可以模拟设备出错的情况，检测驱动能否从异常状态恢复，达到执行的高覆盖率。写操作忽略不会影响到驱动的执行。端口I/O和内存映射I/O通过不同的策略来实现：端口I/O通过重写如inb的指令来实现；内存映射I/O则标记一段内存空间，当读取这一范围的值则返回符号值，向这一范围写值则忽略。

SymDrive的内存映射I/O的策略限于动态执行，是将整个映射的区域符号化。本文的内存映射I/O策略与SymDrive相比，减少了符号值的数量，节约了约束求解器求解符号值的时间。

3.3.2符号化中断

设备的一个特性是可以产生中断，从而触发中断处理函数的运行。本文在SymDrive策略的基础上，设计了一种新的策略来实现中断的触发，加快了执行速度。SymDrive实现的策略为：在每个驱动和内核转换的地方触发注册的中断；改进的策略为：在系统模型中特定的时机触发注册的中断。

前者在实用和简洁中取得了一个折衷，能够保证中断被充分地调用，使驱动的检测更加完备，但是会生成一些本不会发生的中断。后者在一些特定驱动中可以有很好的实用性，可以为系统模型中的定制驱动功能提供支持，如网卡驱动的中断用于触发收包，但存在漏掉驱动的中断处理中漏洞的可能性。

3.3.3符号化DMA

很多驱动都使用DMA操作来与设备进行数据交互，本文仿照内存映射I/O设计了DMA的执行策略：当驱动调用一个DMA映射函数时，会分配一段DMA缓冲并进行标记。每次对这一缓冲进行读操作时返回符号值，所有写操作被忽略；当驱动取消DMA映射时，将这段缓冲的标记取消，并恢复成之前的状态。

和I/O相比，DMA更多地用于大规模数据的交互，所以更可能发生路径爆炸的问题。例如，网卡驱动的收包过程依赖于DMA映射，如果返回符号值会导致收包循环无法结束。针对这种情况，本文参照硬件规范将一部分符号值具体化(就上例来说为指定收包的数目)，来解决可能发生的路径爆炸问题。

4实验结果及分析

检测环境配置如下：24核Intel2.40GHz，E5645CPU，内存12GB。操作系统为Ubuntu12.04LTS，相关软件版本为LLVM2.9版本，KLEE2013.12.11版本。在符号驱动环境下执行Linux内核3.12版本中的lp打印机驱动和e100网卡驱动，结果如表2所示。

Table 2　 Detecting results of Linux drivers

从表2中可以看出，符号驱动环境检测出lp打印机驱动中一个整数溢出漏洞，以及e100网卡驱动中的一个DMA映射相关漏洞。这一结果证明了符号执行环境的可行性。

与SymDrive动态符号分析工具进行性能对比如表3所示。

Table 3　 Performance comparison between symbolic

从表3的结果可以看到：符号驱动环境的检测时间比SymDrive快90%以上；符号驱动环境的函数覆盖率比SymDrive高20%左右。

从时间角度来说，SymDrive在虚拟机上运行真实的Linux系统，所以会在内核的执行中耗费大量时间；而符号执行环境实现了简化的内核接口，因此运行时间主要集中在驱动内部，所以执行的指令数更少，运行时间更短。从函数覆盖比角度来说，由于SymDrive在初始化驱动时采用了成功路径优先的调度策略，而符号驱动环境覆盖了可能发生失败的路径，所以覆盖率更高。这一结果也表明符号驱动环境基本达到了设计的目的：快速检测以及高覆盖率。

5结束语

本文提出并实现了符号驱动环境这一辅助检测Linux驱动中漏洞的工具，结合了静态分析、符号执行和动态分析工具的特点，改善了驱动检测中面临的观测性和覆盖率的问题。在符号驱动环境中，用户可以通过定制系统模型来支持更多的驱动，以及实现特定的功能，还可以通过添加规则来实现针对各种类型漏洞的检测。实验中以lp打印机驱动和e100网卡驱动为例，成功使用该工具检测出两个真实的漏洞，表明其可行性；通过与SymDrive的性能比较，表明了符号驱动环境有快速和覆盖率高的优势。

符号驱动环境还需要进一步改进和完善，今后可以在以下几个方面进行更深一步的研究：(1)对竞争、调度引起的线程或进程间漏洞的检测；(2)优化调度策略和路径剪枝策略，进一步解决路径爆炸问题；(3)支持更多类型的驱动，添加更多的检测规则。

参考文献:

[1]ChouA,YangJ,ChelfB,etal.Anempiricalstudyofoperatingsystemserrors[C]//Procofthe8thACMSymposiumonOperatingSystemPrinciples, 2001:73-88.

[2]SwiftMM,MartinS,LevyHM,etal.Nooks:Anarchitectureforreliabledevicedrivers[C]//Procofthe10thWorkshoponACMSIGOPSEuropeanWorkshop, 2002:102-107.

[3]WangX,ChenH,JiaZ,etal.ImprovingintegersecurityforsystemswithKINT[C]//Procofthe10thUSENIXConferenceonOperatingSystemsDesignandImplementation, 2012:163-177.

[4]BeyerD,HenzingerTA,JhalaR,etal.ThesoftwaremodelcheckerBLAST:Applicationstosoftwareengineering[J].InternationalJournalonSoftwareToolsforTechnologyTransfer, 2007,9(5-6):505-525.

[5]BallT,BounimovaE,CookB,etal.Throughstaticanalysisofdevicedrivers[J].ACMSIGOPSOperatingSystemsRe-

view, 2006, 40(4):73-85.

[6]ChipounovV,KuznetsovV,CandeaG.S2E:Aplatformforin-vivomulti-pathanalysisofsoftwaresystems[J].ACMSIGARCHComputerArchitectureNews, 2011, 39(1):265-278.

[7]CadarC,DunbarD,EnglerDR.KLEE:Unassistedandautomaticgenerationofhigh-coveragetestsforcomplexsystemsprograms[C]//ProcofOSDI, 2008:209-224.

[8]LattnerC,AdveV.LLVM:Acompilationframeworkforlifelongprogramanalysis&transformation[C]//ProcofInternationalSymposiumonCodeGenerationandOptimization, 2004:75-86.

[9]KuznetsovV,ChipounovV,CandeaG.Testingclosed-sourcebinarydevicedriverswithDDT[C]//Procofthe2010USENIXAnnualTechnicalConference, 2010.

[10]RenzelmannMJ,KadavA,SwiftMM.Symdrive:Testingdriverswithoutdevices[C]//ProcofOSDI,2012:4.

[11]NeculaGC,McPeakS,RahulSP,etal.CIL:IntermediatelanguageandtoolsforanalysisandtransformationofCprograms[C]//ProcofCompilerConstruction, 2002:213-228.

范文良(1988-),男,吉林九台人，硕士生，研究方向为操作系统和计算机信息安全。E-mail:fanwlexca@gmail.com

FANWen-liang,bornin1988,MScandidate,hisresearchinterestsincludeoperatingsystem,andcomputerinformationsecurity.