Проверка кода C на недопустимый доступ к памяти с помощью 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 может это проверить?

Это Фрама-С 19.0 (Калий).


c static-analysis memory-access frama-c
person Joachim Breitner    schedule 19.07.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вы на правильном пути, но контракт ACSL часто не лучший способ объяснить Еве, каким должно быть начальное состояние анализа. Обычно для этого используется функция-оболочка (см. раздел 6.3 Eva руководство. В вашем случае вы можете, например, использовать следующий код:

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

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], содержимого массива и самого себя (поскольку вы увеличиваете его, его конечное значение, очевидно, зависит от его начального значения) .

person Virgile    schedule 19.07.2019
comment
Спасибо, отлично! Можно ли как-то закодировать ожидаемый результат анализа в файле, чтобы легко интегрировать проверку со своим набором тестов? (т. е. чтобы мне не приходилось искать текстовый вывод отчета?) - person Joachim Breitner; 20.07.2019
comment
К сожалению, ничего не доступно, хотя небольшой скрипт OCaml должен быть в состоянии убедить Frama-C предоставить информацию в более подходящей форме. Это маршрут, который использовали Airbus и Atos, как описано в этой статье: di.ens.fr/~delmas/papers/erts12.pdf - person Virgile; 20.07.2019
comment
Кстати, то, как это настроено (с #define N 4), проверка не предупредит меня, если код получит доступ, скажем, ко второму байту, не проверяя, находится ли он за пределами буфера. Есть ли способ иметь буфер неопределенной длины и содержимого? - person Joachim Breitner; 23.07.2019
comment
Я бы сказал, что это требует совершенно нового вопроса, но краткий ответ для всех практических целей — нет. По сути, если N — это переменная, абстрактное значение которой не сводится к единственному элементу, в Eva нет доменов, которые бы отслеживали связь между N и длиной массива test. Следовательно, любой доступ будет потенциально недействительным, и вы в конечном итоге получите стог сена (надеюсь) ложных тревог, среди которых может (или нет) скрываться иголка (то есть истинная тревога). Однако вы можете абстрагироваться от контента (на самом деле это то, что там делается через -lib-entry). - person Virgile; 23.07.2019
comment
Вы абсолютно правы насчет нового вопроса: stackoverflow.com/q/57168439/946226. Может там можно поподробнее? - person Joachim Breitner; 23.07.2019