Under-Constrained Symbolic Execution: Correctness Checking for Real Code (2015)
20 Nov 2015 | categories notes原文：Under-Constrained Symbolic Execution: Correctness Checking for Real Code
为什么要做
动态测试的覆盖率低，会漏掉bug；静态分析通过抽象来达到可扩展性，但这样会丧失精度，有时候会漏掉依赖于特定输入才能触发的bug
符号执行能较好地处理这两个缺点，但是它存在路径爆炸的问题。相对于全程序的符号执行，under-constrained符号执行直接执行任意函数，不需要从入口函数开始，这对于库和内核来说很实用。以函数为单位进行符号执行，路径总数只是各函数内路径数的和，而不像全程序符号执行那样，路径总数是各函数之乘积。
做了什么
UC-Klee是个可用于大规模程序的under-constrained符号执行框架，不需要人工撰写（输入）规范或测试用例。利用UC-Klee，作者
- 测试了BIND和OpenSSL的数百个补丁，检查其中是否引入了新的bug
- 结合三种错误的检查器（内存泄露，未初始化数据和未检查的用户输入），检查了最新版的BIND，OpenSSL和Linux内核
结果均发现了数量可观的新漏洞。
under constrained是针对通常程序的输入会受到各种约束（不同输入域间的牵制，程序内的检查等）而言的，因为它可以以任意函数为入口，忽略了由函数调用者传入的约束。它可以提供per-path验证的保证。这种办法显然会有误报，作者的手段是当误报太高时人工地提供约束信息。
UC-Klee作者3年前就提出来了，但是不能应对大规模的程序。
怎么做到的
核心思想是利用Lazy initialization为函数构造符号输入，而不是靠人工写规范或利用种子输入衍生。
- 对于函数参数，先生成符号值，设置为unbound状态，及不受任何限制，可以是值、地址、对象任何东西。
- 根据程序指令对符号值做运算，并决定它的类型，例如有最大值的整数或特定内存区域（从而加上了约束，不再是unbound的）
- 如果对象运算出现在循环里，手工设定循环展开的深度，超出阈值的路径会被扔掉
这样可以从under-constrained的输入中自动地恢复数据结构之间的联系。这种方法有些限制，如不能处理汇编和浮点运算，数据结构不能有环状结构等。在分析程序补丁的时候，这种方法不能处理修改了数据结构的补丁。
补丁检查
如果没打补丁的程序不崩溃，而打了补丁的崩溃了，则补丁有bug。采用剪枝技术删掉不会执行到补丁代码的路径，以及执行了补丁代码但没有引发错误的路径。引发同样错误（同样的pc寄存器读数和错误类型）的路径只留一条。
bug检查
基于规则检查三种bug
- 内存泄露：对于堆对象，如果返回入口函数后无法从根指针引用到，则认为有泄漏
- 未初始化数据：在分配堆栈对象时填入的垃圾数据，如果在之后的操作中被用到，则报告错误
- 未检查的用户输入：手工标注可疑的用户输入，如果路径出错（内存访问错误，assertion失败，零除等）且和可疑输入相关，检查是否有拿用户输入和其它值进行比较过，如果有则认为有用户输入检查，否则则报错。这种办法会有漏报。
效果如何
需要人为设置符号对象的最大尺寸和数据结构的最大深度。
补丁检查
选取BIND和OpenSSL在时间长度为14个月的时间里提交的数百个补丁，每个patch执行1小时，只关心补丁函数和它的调用函数crash的情况。BIND发现了3个，OpenSSL发现了6个未知漏洞。能够发现递归调用里的bug，静态方法由于对递归的推理不够精确很难发现这样的错误。
在给定输入约束的情况下，UC-Klee可以声称补丁没有引入crash，因为它检查了所有的执行路径。这种很强的声明静态分析和测试都无法保证。但是，这会产生误报，解决办法是手工加约束或者采用自动启发式。
手工加约束的办法基于误报来源主要是缺少三类信息【全么？】：
- 数据结构内部的不变量。如二叉查找树的右子节点总大于左子节点
- 状态机不变量。如对某个数值只能单调增长，变量赋值只能是特定序列等
- API不变量。如函数参数不能是空指针
这些信息由人工加入到生成的路径约束的最后，只有路径导致错误且满足这些约束之后才会被视为真的bug路径。试验中这样的约束大概手工添加了400多行。
自动启发式包括两条规则：如果所有执行相同路径的输入都会导致bug，那么这条路径一定有bug；如果函数自身逻辑矛盾，则一定有bug
bug检查
给定编译过的模块和入口函数，要求所有调用的函数都链接进模块。如果检查时发现没链接进来的函数，直接跳过，用一个under-constrained的值代替返回值。内敛汇编和未解析的符号函数指针也都如此处理。这也会引起漏报。
检查了BIND和OpenSSL里超过2000个函数，以及Linux Kernel，每个函数设定检查时间为几分钟，总共发现了67个未知漏洞。可以很强的保证，证明某些函数没有访问未初始化的数据；发现从网络字节顺序转换到主机字节顺序的数据多半不可信。
然后呢
发现更一般的bug，如越界访问等；利用ranking给错误报告排序或发现更多的不变量（约束）以减少FP。