c - 使用Frama-C检查C代码的无效内存访问

我得到了这个C代码（代码的细节，包括可能的bug，并不十分相关）：

int read_leb128(char **ptr, char *end) {
  int r = 0;
  int s = 0;
  char b;
  do {
    if ((intptr_t)*ptr >= (intptr_t)end) (exit(1));
    b = *(*ptr)++;
    r += (b & (char)0x7f) << s;
    s += 7;
  } while (b & (char)0x80);
  return r;
}

我想用一些正式的方法来排除危险的bug。
特别是，我想保证这个函数不会修改除*ptr之外的任何值，只从*ptr到end读取内存（不包括）。
看起来Frama-C是一个很好的验证框架，所以我开始添加注释：

/*@
  requires \valid(ptr);
  requires \valid_read((*ptr) + (0 .. (end-*ptr)));
  assigns *ptr;
 */

似乎检查无效内存访问的Frama-C插件Eva，但在这些文件上运行它仍会打印：

[eva:alarm] foo.c:33: Warning:
  out of bounds read. assert \valid_read(tmp);
                      (tmp from *ptr++)

我只是对工具期望太高，还是Frama-C有办法验证这一点？
这是Frama-C 19.0（钾）。

最佳答案

你已经走上了良好的轨道，但ACSL合同通常不是向Eva解释分析初始状态应该是什么的最佳方式通常，您会为此使用包装函数（请参见Eva manual的第6.3节）例如，在您的示例中，可以使用以下代码：

#include <stdint.h>
#include <stdlib.h>

/*@
  requires \valid(ptr);
  requires \valid_read((*ptr) + (0 .. (end-*ptr)));
  assigns *ptr;
 */
int read_leb128(char **ptr, char *end) {
  int r = 0;
  int s = 0;
  char b;
  do {
    if ((intptr_t)*ptr >= (intptr_t)end) (exit(1));
    b = *(*ptr)++;
    r += (b & (char)0x7f) << s;
    s += 7;
  } while (b & (char)0x80);
  return r;
}

#define N 4

char test[N];

int main() {
char* beg = &test[0];
char* end = &test[0] + (N-1);
read_leb128(&beg, end);
}

现在，由于您似乎对输出（分配的位置）和输入（读取初始值的位置）感兴趣，您需要从Inout插件激活一些选项（请参见Eva manual的第7章）：

frama-c -eva -eva-slevel 20 res.c -lib-entry -out-external -input

会给你：

...
[inout] Out (external) for function read_leb128:
    beg
[inout] Inputs for function read_leb128:
    test[0..2]; beg

这确实表明只有beg（其地址被传递到read_leb128）被修改，并且它的值来自数组的内容和自身（因为您增加了它，它的最终值显然取决于它的初始值）。

关于c - 使用Frama-C检查C代码的无效内存访问，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/57114424/