检测整数溢出的静态代码分析技术答案

【问题标题】：Techniques for static code analysis in detecting integer overflows检测整数溢出的静态代码分析技术
【发布时间】：2014-12-03 19:37:56
【问题描述】：

我正在尝试找到一些有效的技术，可以作为我的integer-overflow 检测工具的基础。我知道那里有许多现成的检测工具，但我正在尝试自己实现一个简单的工具，这既是出于我个人对该领域的兴趣，也是出于我的知识。

我知道Pattern Matching 和Type Inference 之类的技术，但我读到需要更复杂的代码分析技术来检测int 溢出。还有Taint Analysis 可以“标记”不受信任的数据源。

是否有其他一些我可能不知道的技术能够检测整数溢出？

【问题讨论】：

在 x86 CPU 上有一个进位标志 CF，在每次导致溢出的 int 算术运算后将其设置为 1。当然它只能用于运行时检查，您是在寻找纯静态分析吗？
是的，我正在寻找更多的编程技术来检测溢出。不过我会记下来，谢谢！
任何特定的编程语言？
C 是我想要使用的。
我建议将主题修改为：“检测整数溢出的静态代码分析技术”

标签： c detection static-analysis integer-overflow

【解决方案1】：

可能值得尝试使用cppcheck 静态分析工具，claims 从版本 1.67 开始检测有符号整数溢出：

新检查：
- 检测移位过多、有符号整数溢出和危险符号转换

请注意，它同时支持 C 和 C++ 语言。

对于无符号整数没有溢出检查，因为标准无符号类型永远不会溢出。

这是一些基本的例子：

#include <stdio.h>

int main(void)
{
    int a = 2147483647;
    a = a + 1;

    printf("%d\n", a);

    return 0;
}

通过这样的代码，它得到：

$ ./cppcheck --platform=unix64 simple.c 
Checking simple.c...
[simple.c:6]: (error) Signed integer overflow for expression 'a+1'

但是我不会对它有太多期望（至少在当前版本中），因为程序略有不同：

int a = 2147483647;
a++;

通过而没有注意到溢出。

【讨论】：

谢谢！我会检查一下。
静态分析仍然可以寻找可能无意的无符号整数换行。

【解决方案2】：

您似乎正在寻找某种价值范围分析，并检测该范围何时会超过设定的界限。这是一件表面上看起来很简单，但实际上很难的事情。会有很多误报，即使不计算实现中的错误。

暂时忽略细节，您将一对[lower bound, upper bound] 与每个变量相关联，并进行一些数学运算以找出每个运算符的新界限。例如，如果代码添加了两个变量，则在您的分析中，您将上限加在一起形成新的上限，并将下限加在一起以获得新的下限。

但当然没那么简单。首先，如果有非直线代码怎么办？ if 还不错，您可以只评估双方，然后取其后的范围的并集（这可能会丢失信息！如果两个范围之间有间隙，它们的并集将跨越间隙）。循环需要技巧，一个简单的实现可能会在循环上运行数十亿次分析迭代，甚至根本不会终止。即使您使用没有无限上升链的抽象域，您仍然会遇到麻烦。解决此问题的关键字是“加宽运算符”和（可选，但可能是个好主意）“收窄运算符”。

比这更糟糕，因为什么是变量？您的标量类型的常规局部变量永远不会被占用，这还不错。但是数组呢？现在您甚至不确定哪个条目受到影响——索引本身可能是一个范围！然后是混叠。这远非一个已解决的问题，并导致许多现实世界的工具做出非常悲观的假设。

还有，函数调用。您将从某些上下文中调用函数，希望是已知的（如果不是，那么很简单：您什么都不知道）。这很困难，不仅突然间要同时跟踪更多状态，还可能有几个地方可以调用函数，包括自身。对此的通常反应是在其参数之一的范围已扩展时重新评估该函数，如果不仔细执行，这可能需要数十亿步。还有一些算法可以针对不同的上下文对函数进行不同的分析，这样可以提供更准确的结果，但很容易花费大量时间来分析差异不大的上下文。

无论如何，如果您已经做到了这一点，您可以阅读Accurate Static Branch Prediction by Value Range Propagation 和相关论文，以了解如何实际执行此操作。

这还不是全部。仅考虑单个变量的范围而不关心（关键字：非关系抽象域）它们之间的关系，这对非常简单（对于人类读者）的事情不利，例如减去两个值总是接近的变量，为此它将产生一个很大的范围，假设它们可能在它们的界限允许的范围内相距很远。即使是一些琐碎的事情，例如

; assume x in [0 .. 10]
int y = x + 2;
int diff = y - x;

对于人类读者来说，diff = 2 很明显。在到目前为止描述的分析中，结论将是y in [2 .. 12] 和diff in [-8, 12]。现在假设代码继续

int foo = diff + 2;
int bar = foo - diff;

现在我们得到foo in [-6, 14] 和bar in [-18, 22]，即使bar 显然又是2，范围又翻了一番。现在这是一个简单的示例，您可以编造一些临时黑客来检测它，但这是一个更普遍的问题。这种影响往往会迅速扩大变量范围并产生大量不必要的警告。部分解决方案是将范围分配给变量之间的差异，然后您会得到所谓的差异绑定矩阵（不出所料，这是 relational 抽象域的示例）。对于过程间分析，它们可能会变得又大又慢，或者如果您也想向它们抛出非标量变量，那么算法就会开始变得更加复杂。而且它们只能让你到目前为止 - 如果你在混合中加入乘法（包括x + x 和变体），事情仍然会很快变坏。

因此，您可以在混合中添加可以处理乘以常数的其他内容，例如 Abstract Domains of Affine Relations⋆ - 这与范围非常不同，并且它本身不会告诉您有关变量范围的太多信息，但您可以使用它来获得更准确的范围。

故事并没有就此结束，但这个答案越来越长。我希望这不会阻止您研究这个主题，这个主题非常适合从简单的开始，并为您的分析工具添加越来越多有趣的东西。

【讨论】：

【解决方案3】：

检查 C 中的整数溢出：

当您将两个 32 位数字相加并得到 33 位结果时，低 32 位被写入目标，最高位作为进位标志发出信号。包括 C 在内的许多语言都没有提供访问此“进位”的方法，因此您可以使用限制，即<limits.h>，在执行算术运算之前进行检查。考虑 unsigned int 的 a 和 b：

如果MAX - b < a，我们肯定知道a + b 会导致溢出。这个C FAQ 给出了一个例子。

注意： 正如 chux 所指出的，这个例子对于有符号整数是有问题的，因为它不会处理 MAX - b 或 MIN + b if b < 0 .第二个链接（如下）中的示例解决方案涵盖了所有情况。

数字相乘也会导致溢出。一个解决方案是将第一个数字的长度加倍，然后进行乘法运算。比如：

(typecast)a*b

注意： (typecast)(a*b) 会不正确，因为它先截断然后再进行类型转换。

c 的详细技术可以在HERE 找到。使用宏似乎是一个简单而优雅的解决方案。

【讨论】：

"... 两个 32 位数字并得到 33 位结果，低 32 位写入目标，..." 不是 C 规范定义的。使用int 溢出，结果是未定义的行为。这里所说的结果是常见的，但 C 没有指定。
@chux 抱歉，我的意思是“不会导致溢出”，谢谢指出！
MAX - b >= a --> 溢出有问题。考虑a=any_thing, b= -1。 INT_MAX - -1 未定义。任何检测溢出的测试都不应自身溢出。最好在完成任何 +/- 之前先进行比较。考虑detect int overflow

【解决方案4】：

我希望Frama-C 能够提供这样的功能。 Frama-C 专注于 C 源代码，但我不知道它是方言敏感的还是特定的。我相信它使用抽象解释来建模价值观。我不知道它是否专门检查溢出。

我们的DMS Software Reengineering Toolkit 有多种语言前端，包括 C 的大多数主要方言。它提供控制和数据流分析，以及对计算范围的抽象解释，作为您构建答案的基础。我的Google Tech Talk on DMS 在大约 0:28:30 专门讨论了如何使用 DMS 对值范围的抽象解释来检测溢出（缓冲区索引）。检查数组大小上限的一种变体是检查不超过 2^N 的值。但是，现成的 DMS 不提供任何针对 C 代码的特定溢出分析。 OP 有空间做有趣的工作：=}

【讨论】：