使用 Frama-C 检查 C 代码的无效内存访问 [英] Checking C code for invalid memory access with Frama-C

问题描述

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

I am given this C code (the details of the code, including possible bugs, are not very relevant):

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

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

and I want to throw some formal methods at it to rule out dangerous bugs.

特别是，我想保证这个函数不会修改除 *ptr 之外的任何值，并且只读取从 *ptr 到 end(不包含).

In particular, I would like a assurance that this function does not modify any value besides *ptr and only reads memory from *ptr to end (not inclusive).

看起来 Frama-C 是一个很好的验证框架，所以我开始添加注释:

It looked like Frama-C is a good framework for such verification, so I started to add annotations:

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

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

It seems that the Frama-C plugin that checks for invalid memory access is Eva, but running it on these files still prints:

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

我只是对这个工具期望过高，还是有办法让 Frama-C 验证这一点?

Am I just expecting too much of the tool, or is there a way for Frama-C to verify this?

这是 Frama-C 19.0(钾).

This is Frama-C 19.0 (Potassium).

推荐答案

您的工作进展顺利，但是 ACSL 合同通常不是向 Eva 解释分析的初始状态应该是什么的最佳方式.通常，您为此使用包装函数(请参阅 Eva手册.就您而言，您可以使用以下代码:

You're on the good track, but an ACSL contract is often not the best way to explain to Eva what the initial state of the analysis should be. Usually, you use a wrapper function for that (see section 6.3 of the Eva manual. In your case, you could for instance go with the following code:

#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 手册):

Now, as you seem to be interested by the outputs (locations that are assigned) and the inputs (locations whose initial value is read), you need to activate some option from the Inout plugin (see chapter 7 of the 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]，数组的内容，以及它本身(因为你递增它，它的最终值显然取决于它的初始值).

which indeed indicates that only beg (whose address is passed to read_leb128) is modified, and that it gets its values from test[0 .. 2], the content of the array, and itself (since you increment it, its final value obviously depend on its initial value).

这篇关于使用 Frama-C 检查 C 代码的无效内存访问的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！