tts*_*ras 5 static-analysis frama-c
在查看代码库时，我发现了一段特定的代码，它触发了关于“越界访问”的警告。查看代码后，我看不到报告访问的发生方式 - 并试图最小化代码以创建可重现的示例。然后，我使用我可以访问的两个商业静态分析器以及开源 Frama-C 检查了这个示例。
他们三个人都看到相同的“越界”访问权限。
我不。我们来看一下：
3 extern int checker(int id);
4 extern int checker2(int id);
5
6 int compute(int *q)
7 {
8 int res = 0, status;
9
10 status = checker2(12);
11 if (!status) {
12 status = 1;
13 *q = 2;
14 for(int i=0; i<2 && 0!=status; i++) {
15 if (checker(i)) {
16 res = i;
17 status=checker2(i);
18 }
19 }
20 }
21 if (!status)
22 *q = res;
23 return status;
24 }
25
26 int someFunc(int id)
27 {
28 int p;
29 extern int data[2];
30
31 int status = checker2(132);
32 status |= compute(&p);
33 if (status == 0) {
34 return data[p];
35 } else
36 return -1;
37 }
请不要试图判断代码的质量，或者它为什么这样做。这是原始版本的黑客、裁剪和变异版本，其唯一目的是通过一个小示例来演示该问题。
我有权访问的所有分析器都报告相同的事情 - 第 34 行调用者中的索引，执行该操作return data[p]可能通过无效索引“2”读取。这是 Frama-C 的输出 - 但请注意，两个商业静态分析器提供完全相同的评估：
$ frama-c -val -main someFunc -rte why.c |& grep warning
...
why.c:34:[value] warning: accessing out of bounds index. assert p < 2;
让我们逆向执行代码，看看第 34 行的越界访问是如何发生的：
status来自两个呼叫checker2和compute应为0。compute返回 0（在调用者的第 32 行，被调用者的第 23 行），这意味着我们已经在第 22 行执行了赋值——因为它在第 21 行被保护并检查是否为status0。所以我们在传入的指针q，无论存储在变量中res。该指针指向用于执行索引的变量 - 假定的越界索引。data，该 被定义为恰好包含两个元素，我们必须将一个既不是 0 也不是 1 的值写入res。res通过for循环写入；这将有条件地分配到res; 如果它确实分配了，它将写入的值将是两个有效索引 0 或 1 之一 - 因为这些是for循环允许通过的值（它与 绑定i<2）。status第 12 行的初始化，如果我们确实到达第 12 行，我们肯定会至少进入循环一次。如果我们确实写入res，我们将写入一个很好的有效索引。status检查 - 在第 11 行或第 21 行失败，我们将返回一个非零值status；所以我们在传入的值中写入（或没有写入，并且未初始化）的任何值q都无关紧要；由于第 33 行的检查，调用者不会读取该值。因此，要么我遗漏了某些东西，并且确实存在导致第 34 行索引 2 越界访问的情况（如何？），要么这是主流形式验证限制的一个示例。
帮助？
== 0和!= 0范围内的案例时[INT_MIN; INT_MAX]，您需要告诉 Frama-C/Eva 拆分案例。通过//@ split在适当的位置添加注释，您可以告诉 Frama-C/Eva 保持单独的状态，从而防止在status评估之前合并它们。
在这种情况下，您的代码如下所示（由 @Virgile 提供）：
extern int checker(int id);
extern int checker2(int id);
int compute(int *q)
{
int res = 0, status;
status = checker2(12);
//@ split status <= 0;
//@ split status == 0;
if (!status) {
status = 1;
*q = 2;
for(int i=0; i<2 && 0!=status; i++) {
if (checker(i)) {
res = i;
status=checker2(i);
}
}
}
//@ split status <= 0;
//@ split status == 0;
if (!status)
*q = res;
return status;
}
int someFunc(int id)
{
int p;
extern int data[2];
int status = checker2(132);
//@ split status <= 0;
//@ split status == 0;
status |= compute(&p);
if (status == 0) {
return data[p];
} else
return -1;
}
在每一种情况下，第一个split注解告诉伊娃考虑案件status <= 0和status > 0分开; 这允许将间隔“分解”[INT_MIN, INT_MAX]为[INT_MIN, 0]and [1, INT_MAX]；第二个注释允许分离[INT_MIN, 0]为[INT_MIN, -1]和[0, 0]。当这 3 个状态分别传播时，Eva 能够精确区分代码中的不同情况，避免虚假警报。
您还需要为 Frama-C/Eva 留出一定的余量来保持状态分离（默认情况下，Eva 会优化效率，稍微积极地合并状态）；这是通过添加来完成的-eva-precision 1（您的原始场景可能需要更高的值）。
-eva-domains sign以前-eva-sign-domain）和-eva-partition-history NFrama-C/Eva 还有其他与分裂状态相关的选项；其中之一是符号域，它计算有关变量符号的信息，可用于区分 0 和非零值。在某些情况下（例如稍微简化的代码版本，其中status |= compute(&p);替换为status = compute(&p);），符号域可能有助于拆分而无需注释。使用-eva-domains sign(-eva-sign-domain对于 Frama-C <= 20)启用它。
另一个相关选项是-eva-partition history N，它告诉 Frama-C 将状态分区保持更长时间。
请注意，就分析而言，保持状态分离的成本有点高，因此，如果它包含更多分支，则在应用于“真实”代码时可能无法扩展。增加赋予-eva-precision和的值-eva-partition-history可能会有所帮助，以及添加@ split注释。
我想添加一些评论，希望将来有用：
Frama-C 包含多个插件和分析。特别是在这里，您使用的是Eva插件。它基于抽象解释执行分析，报告程序中所有可能的运行时错误（未定义行为，正如 C 标准所说）。-rte因此使用是不必要的，并且给结果增加了噪音。如果 Eva 不能确定没有警报，它会报告它。
将-val选项替换为-eva。这是同样的事情，但前者已被弃用。
如果要提高精度（以消除误报），请添加-eva-precision N，其中0 <= N <= 11。在您的示例程序中，它没有太大变化，但在具有多个调用堆栈的复杂程序中，额外的精度将需要更长的时间，但会最大限度地减少误报的数量。
此外，请考虑为外部功能提供最低限度的规范，以避免警告；此处它们不包含指针，但如果包含指针，则您需要提供一个assigns子句来明确告诉Frama-C 函数是否修改了此类指针（或任何全局变量，例如）。
借助 Frama-C 图形界面和 Studia 插件（可通过右键单击感兴趣的表达式并选择弹出菜单 Studia -> Writes 访问），并使用GUI 中的“值”面板，您可以轻松跟踪分析内容推断，并更好地了解警报和值的来源。唯一的缺点是，它没有准确报告合并发生的位置。为了尽可能获得最精确的结果，您可能需要添加对 Eva 内置 的调用Frama_C_show_each(exp)，并将其放入循环中，以使 Eva 在其分析的每次迭代中显示 中包含的值exp。
有关更多详细信息，请参阅Eva 用户手册的第 9.3 节（显示中间结果），包括类似的内置函数（例如Frama_C_domain_show_each和Frama_C_dump_each，它们显示有关抽象域的信息）。您可能需要#include "__fc_builtin.h"在您的程序中。#ifdef __FRAMAC__当包含这个特定于 Frama-C 的文件时，您可以使用来允许原始代码编译。
Frama-C 是一个基于语义的工具，其主要分析是详尽的，但可能包含误报：Frama-C 可能会在警报未发生时报告警报，但它不应忘记任何可能的警报。这是一种权衡，您不可能在所有情况下都拥有精确的工具（尽管在此示例中，具有足够的 -eva-precision，Frama-C 是精确的，因为仅报告可能实际发生的问题）。
从这个意义上说，错误意味着 Frama-C“忘记”指出某些问题，我们会非常关注它。指示可能不会发生的警报对用户来说仍然是个问题（我们正在努力改进它，因此这种情况应该更少发生），但不是Frama-C 中的错误，因此我们更喜欢不准确地使用该术语，例如“Frama-C/Eva 不准确地报告越界访问”。