似乎无效的内存访问没有由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运行时库进行一些基本检查；例如，在程序启动期间，它在address 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确实在没有警告的情况下编译了这个文件，但是当您运行代码时，您将从address获得一条消息。

=================================================================
==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

这样的输出对于发现这样的漏洞和溢出非常有帮助。

但是，对于编译器来说，查找在运行时发生的此类错误并不是一项简单的任务。