Sound Input Filter Generation for Integer Overflow Errors (2014)

原文：Sound Input Filter Generation for Integer Overflow Errors

静态分析源代码得到输入过滤器，以消灭可能导致整数溢出的程序输入。过滤结果是正确的，即通过过滤器的输入不会（在检查点）发生溢出。目前检查点只包括内存分配和拷贝(*alloc和mem*)系列函数。

过滤器即一组约束。传统的生成方法有：

1. 由一条引发错误的输入着手，生成出错路径。然后在路径上前向符号执行，收集导致错误路径执行的约束，称为Vulnerability Signature。这个签名就是过滤器，满足签名的输入会导致错误，于是被过滤掉。显然，这种方法不够完备，它没有考虑有别的错误路径存在。
2. 由vulnerable site入手，利用weakest precondition反推该点的过滤器。这种方法需要注意对循环和别名的处理。

贡献

• 工具；
• 正确高效的静态分析；
• 输入域的新抽象。一条输入中可能有多个值（实例）对应同一个输入域，比如包含多个同类型对象时。该抽象允许代表同一个域的变量之间互换，因为每个变量都代表所有的可能的实例。该方法没有追求程序变量和同一个输入中属于同一输入域的多个实例。
• 首次将现成的（正确的）指针分析和前件生成算法结合，将指针分为不同的等价类。
• 实验结果：没有漏报，过滤时间在毫秒级别。（但注释过程需要人工，最久的花了30分钟。）

工作原理

1. 由开发者指定要处理输入的模块，对解析输入的语句加注释，标记它所读入的输入域。
2. SIFT实施过程间、需求驱动的静态最弱前件分析，为每个关键点（内存分配和拷贝点）生成关键表达式（在内存分配和拷贝点的表达式）。
3. 沿控制流反向传播关键表达式，获得程序运行到关键点的符号条件。符号条件记录了关键表达式如何被计算的，只考虑算数表达式的约束，不考虑（路径）条件表达式的约束。
4. 利用Hachior之类的输入格式解析器，将输入按输入域分组并录入。
5. 利用解析器和符号条件生成过滤器。过滤器先用格式解析器分析输入构成，然后计算每个符号条件，如果满足，则抛弃，如果不满足则通过。

不考虑路径约束可以提高效率，保证正确性（路径约束是合取的，子约束数量越多过滤掉的越少；约束越多，花的时间越长）。实验证明不检查路径不影响精度没有false positive，6万多个测试用的输入中，没有发现好的（不引发漏洞）输入被过滤掉。

符号表达式可能包括和变量和指针。不同变量可能对应相同输入域的不同实例，因此需要输入域的抽象；指针显然需要指针分析；某些输入域是在循环中调用函数读入的，于是需要过程间的循环不变式分析传播符号条件。循环次数（上限）需要由别的什么分析得到，或者人工注释。

过程间分析使用了标准的summary table技术，主要计算两件事：和符号条件中的变量相关的变量返回值，以及相关的指针操作结果，以此修改符号条件。

有价值的部分

• 循环的不动点解法很fancy
• 将正确的指针分析引入正则变换很讨巧