使用 Frama-C 检查 C 代码是否存在无效内存访问

Checking C code for invalid memory access with Frama-C

我得到了这个 C 代码(代码的细节,包括可能的错误,不是很相关):

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;
}

我想用一些正式的方法来排除危险的错误。

特别是,我想保证此函数不会修改 *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 插件中激活一些选项(参见第 7 章) Eva manual):

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)被修改,并且它从test[0 .. 2],数组的内容中获取它的值,并且本身(因为你递增它,它的最终值显然取决于它的初始值)。