总结

        目标：挖掘Double-Fetch漏洞。操作系统内核代码中，可能出现两次读取用户空间数据的情况，如果两次读取之间，用户数据遭到篡改，而内核代码第二次读取没有对所读数据进行验证，就会可能导致Double-Fetch漏洞。

        以往工作：由于错误的假定和不准确的漏洞定义，导致误报和漏报率过高。例如，不支持设备模拟、过程间分析、循环处理。

        解决方法：形式化精确定义DF，提出DEADLINE—静态分析工具。首先采用静态程序分析寻找multi-read，再采用定制的符号化检查来检测multi-read是否导致DF。

        结果：找到Linux和FreeBSD中24个漏洞；提出四种打补丁方法。

        贡献：

            a.形式化精确定义DF，自动确认DF

            b.实现端到端系统DEADLINE，裁剪版符号执行自动确认DF

            c.发现24个漏洞

            d.提出四种通用补丁方法

1.简介

（1）multi-read定义

Wang[10]定义：根据第一次读的作用可分为 a.size checking—申请空间取决于size变量；b.type selection—申请空间取决于opcode值；c.shallow copy—头中包含指针，指向用户空间中第二段缓冲区。

本文定义：a.依赖查询—根据请求头的信息查询对应的handler，再拷贝整个请求；b.协议/签名检查—根据协议号采取对应处理方式；c.信息推测—当有信息缺失时，内核通过选择性读取来推测缺失信息，最后拷贝所有数据。

（2）现有的DF漏洞检测技术

Wang[10]：静态模式匹配，产生误报和漏报，且忽略了跨循环或函数调用的DF（缺乏过程间分析）；模式匹配引擎Coccinelle[16]不支持宏扩展，设置某些配置如CONFIG_COMPAT时，与兼容性有关的函数才会生效，它们可能含有漏洞。需手动验证DF。

Bochspwn[9]：动态方法，难扩展到全内核分析，只有部分驱动能模拟；代码覆盖率低，只覆盖热点路径。需手动验证DF。

（3）DF条件及形式化定义

DF条件：

        a.两次从用户空间读，multi-read。

        b.读空间重叠，overlapped-fetch。

        c.有依赖关系，控制/数据依赖。

        d.用户线程可修改重叠区域的内容。

形式化定义：

double-fetch形式化定义

2.DEADLINE Overview

选择符号执行原因：a.求解约束判定可满足性；b.可扩展性，不依赖硬件；c.能从任意点开始路径探索，类似UC-KLEE[17]。

选择LLVM IR原因：a.信息丰富，类型、函数名、参数；b.指令属于单一静态赋值形式，类似SE；c.可重用LLVM分析，如调用图构建、函数内联等。

总体步骤：

        见Algorithm1。

Algorithm1-DEADLINE总体步骤

    2-收集所有fetch；4-对每个fetch，前向后向搜索控制流程图，查找另一个fetch，构成multi-read；6-对每对fetch构造可能的路径；8-调用符号执行引擎检查multi-read是否为DF漏洞。

3.具体步骤

3.1搜索multi-read

（1）fetch对搜集

方法：见Algorithm2。

         a.识别所有fetch

         b.对给定的1个fetch，收集附近（前后）的fetch与之配对，嵌入函数内也要搜索。

         c.找到包含两个fetch的闭合函数Fn，<F0,F1,Fn>表示1个multi-read。

Algorithm2-搜集multi-read

（2）执行路径构建

方法：

        a.遍历Fn的CFG，找F0->F1的执行路径。

        b.只保留相关指令，对该fetch有影响（fetch的地址和长度从该指令得来），或者被fetch影响（用到fetch-in值）。

        执行路径线性化，即生成IR指令序列。Loop只展开1次（假定循环是为了递增读取输入，展开多次没必要）

3.2识别DF漏洞

    见Figure4。

Fig4-DF示例及识别流程

（1）案例解读

漏洞：存在size区域读重叠，第二次读入的attr->size没有进行检查，可被篡改attr->size=0xffffffff，触发竞争漏洞。

符号执行：见4c。$S—符号值，@X—$X指向的内存，<i,j,L>内存对象（L：K/U权限），循环处理/指针解决—见附录A。

（2）IR转化为SR

符号表示：PARM—参数/全局变量（没被定义过，看作roots），KMEM/UMEM—内存blob。

SE三种指令处理：

        a.分支指令，不同于传统SE，只沿具体路径走，不探索新路径，搜集所走路径的分支条件。最后用求解器求解约束条件。

        b.库函数，类型包括内存分配/内存操作/字符串操作/同步操作/调试和错误报告，方法是作函数摘要，linux中45个FreeBSD中12个。

        c.内联汇编，一般忽略，对常见的作摘要。

（3）内存模型

现有内存模型：KLEE[14]/SAGE[15]，内存由bit/byte线性数组表示，用select(a,i)/store(a,i)从数组a的位置i处读取和存入。

问题：未考虑到两次读取之间，数据被其他线程修改，找不到DF漏洞。

改进：

        a.给用户空间读标注，以区分不同时间的读。

        b.__user标注指针指向用户空间，否则指向内核空间。

        c.内存模型，全内存字节组改为，1个指针对应1个字节数组。不同的函数参数和全局变量；新分配的指针如kmalloc；指针赋值是例外，新旧指针指向同一内存；不能证明指向同一内存对象的指针。

（4）形式化检查

        a.是否有空间重叠

        b.检测是否有控制/数据依赖

3.3实现

基于LLVM+Z3。

（1）增大代码覆盖率：编译更多内核代码，设置所有编译选项参数（#ifdef声明），如CONFIG_COMPAT。

（2）源码编译为LLVM IR： 所有bitcode文件整合为1个模块。

4.实验评估与讨论

实验结果：Linux和FreeBSD中发现23个和1个漏洞。

double-fetch利用方法：泄露信息；绕过检查；拒绝服务

不能自动判断可利用性原因：没有crash信号，需手动判断exploit是否成功；很难构造exploit。

打补丁方法：

        a.采用第一次fetch的size；

        b.判断两次fetch的size是否相等；

        c.避免重复读取用户空间，增量读取；

        d.重构代码，一次fetch所有用户数据。

DEADLINE优势：

    （1）路径探索策略：离线探索，对特定路径进行符号执行，不执行无关路径。

    （2）内存模型：对不同的用户空间读进行标记，抓住DF漏洞本质；现有符号执行技术中，指针可以指向任意区域，Deadline中，1个指针指向1个内存对象，从multi-read中筛选出不相关的fetch。

局限性：

        （1）源码覆盖：a.LLVM编译不成功，3个文件系统4个驱动；b.没展开的宏代码。

        （2）路径构造：a.路径构造数有限（最多4096条）；b.循环需多次展开或跨循环才会触发的漏洞；c.循环中有分支，分支需先满足后不满足才会触发。

        （3）符号化检查：a.漏报，忽略了很多内联汇编，且有些汇编总结不精确；b.漏报，没分析指针别名，可能访问了同一用户空间；c.误报，若第二次fetch正确性检查发生在闭函数之外，可能误判定为满足DF漏洞条件。