Казалось бы, неверный доступ к памяти не сообщен CMBC

Question

У меня есть следующий фрагмент кода.

#include<stdio.h>
#include<stdlib.h>
int main()
{
        char *c = malloc(1);
        printf("%p\n", c);
        c = c + 20;

        printf("%p\n", c);
        printf("%d\n", *c);

        free(c - 20);
        return 0;
}

В этом коде я выделяю 1 байт памяти для указателя. Затем я обращаюсь к ячейке памяти, которая через 20 единиц после выделенной памяти. Когда я разыменую этот указатель, я ожидаю получить ошибку нарушения доступа к памяти, ошибку сегментации или что-то в этом роде. Я не получаю такой ошибки.

Давайте предположим, что это случай неопределенного поведения. Поэтому я попытался проверить эту программу с помощью CBMC, хорошо известного средства проверки моделей, с помощью следующей команды.

cbmc test01.c --pointer-check

CBMC сообщает, что программа безопасна. Это проблема с CBMC или я что-то упустил?

Answer 1

Как вы сказали в своем вопросе, заявление printf("%d\n", *c); выставляет неопределенное поведение. Будучи неопределенным, любое ожидание против вас ложно. Это включает в себя получение конкретной ошибки или любой ошибки вообще.

Библиотека времени выполнения C не проверяет, как ваша программа обращается к памяти. Если это будет сделано, программа будет работать намного, намного медленнее. Что касается кучи, библиотека времени выполнения C выполняет некоторые базовые проверки; например, он помещает определенное значение по адресу 0 во время запуска программы и проверяет, остается ли значение до завершения программы. Если значение изменилось, для записи была отменена ссылка на нулевой указатель, и он может предупредить вас об этом.

После c = c + 20;, c Скорее всего, указывает на блок памяти, который принадлежит вашей программе. Это может быть свободная область в куче, она может находиться внутри структур данных, используемых менеджером кучи для обработки кучи, но есть большие шансы, что она все еще находится на той же странице памяти.

Если у вас есть (плохая) удача и c + 20 приземляется за страницу памяти, которая хранит c тогда происходит исключительная ситуация, которая обрабатывается операционной системой. Он завершает работу программы и отображает сообщение об ошибке, подобное тому, которое вы указали в вопросе (идея та же самая, слова и представление отличаются в каждой ОС).

---

Обновить

Выделение памяти - это не какая-то магия. Программа запускается с блока памяти (называемого "куча"), который назначается операционной системой для этой цели.

Библиотека времени выполнения C содержит код, который управляет кучей. Этот код использует небольшую часть этой памяти для своей бухгалтерии. Обычная реализация использует двойные связанные списки, причем полезная нагрузка каждого узла из списка представляет собой блок памяти, "выделенный" программой с использованием функций, объявленных в <memory.h> (malloc(), calloc() так далее). Когда звонок в malloc() случается, этот код выполняется, создает новый узел в списке и возвращает адрес полезной нагрузки узла (адрес внутри кучи).

Программа использует этот указатель так, как хочет. Ваша программа может свободно писать на c-1, например. На самом деле, внутри malloc() он на самом деле написал информацию там. После malloc() возвращается c, ваш код также можно написать на c-1, От OS С точки зрения, нет никакой разницы между этими двумя операциями записи. И потому что C не является управляемым или интерпретируемым языком, в вашу программу не включен код, который следит за тем, что делает код, который вы написали, или держит его за руку, чтобы не писать не в том месте.

Если вы напишите в c-1 есть большая вероятность, что вы повредите структуры данных, используемые менеджером кучи. Ничего плохого не происходит сразу. Сообщение об ошибке не отображается, и ваша программа продолжает работать нормально. Но при следующем вызове функции, которая обрабатывает кучу (будь то выделение памяти или освобождение), программа начнет сеять хаос. Повреждение структуры данных кучи может произойти все, что угодно.

---

Что касается CBMC, я не знаю, как это работает. Может быть, он не может обнаружить такие ситуации. Или, может быть, он сообщает, что ваша программа безопасна, потому что не пишет в c после того, как он был увеличен.

Answer 2

КСТАТИ. gcc -fsanitize=address компилирует этот файл без предупреждения, но когда вы запустите код, вы получите сообщение с адреса sanitzer

=================================================================
==24198==ERROR: AddressSanitizer: heap-buffer-overflow on address 0x60200000f004 at pc 0x400921 bp 0x7ffe1e66b900 sp 0x7ffe1e66b8f0
READ of size 1 at 0x60200000f004 thread T0
    #0 0x400920 in main (/home/ingo/test/c/sanitize_address+0x400920)
    #1 0x7fdd9ddca7af in __libc_start_main (/lib64/libc.so.6+0x207af)
    #2 0x4007d8 in _start (/home/ingo/test/c/sanitize_address+0x4007d8)

0x60200000f004 is located 19 bytes to the right of 1-byte region [0x60200000eff0,0x60200000eff1)
allocated by thread T0 here:
    #0 0x7fdd9e19c7b7 in malloc (/usr/lib/gcc/x86_64-pc-linux-gnu/4.9.3/libasan.so.1+0x577b7)
    #1 0x4008b7 in main (/home/ingo/test/c/sanitize_address+0x4008b7)
    #2 0x7fdd9ddca7af in __libc_start_main (/lib64/libc.so.6+0x207af)

SUMMARY: AddressSanitizer: heap-buffer-overflow ??:0 main
Shadow bytes around the buggy address:
  0x0c047fff9db0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff9dc0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff9dd0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff9de0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff9df0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa 01 fa
=>0x0c047fff9e00:[fa]fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff9e10: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff9e20: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff9e30: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff9e40: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff9e50: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
Shadow byte legend (one shadow byte represents 8 application bytes):
  Addressable:           00
  Partially addressable: 01 02 03 04 05 06 07 
  Heap left redzone:       fa
  Heap right redzone:      fb
  Freed heap region:       fd
  Stack left redzone:      f1
  Stack mid redzone:       f2
  Stack right redzone:     f3
  Stack partial redzone:   f4
  Stack after return:      f5
  Stack use after scope:   f8
  Global redzone:          f9
  Global init order:       f6
  Poisoned by user:        f7
  Contiguous container OOB:fc
  ASan internal:           fe
==24198==ABORTING

такой вывод может быть весьма полезен для обнаружения таких утечек и переполнений.

Но компилятору непросто найти такие ошибки, которые возникают во время выполнения.