静态分析C程序的内存模型

矫情吗；* 2022-10-04 13:56 80阅读 0赞

> 代码静态分析必须可以准确地追踪不同内存对象的值，这篇论文描述了一种适用于C程序静态分析的内存模型。此模型特别适合于那些精确地路径敏感分析，例如：符号执行技术。它可以处理各种类型的C程序表达式，包括多级指针解引用，指针算数运算，复合数组和结构体类型，各种类型转换以及动态内存分配等等。它将各种左值表达式映射为不需要额外分析别名的相同对象，在 Clang static analyzer 中已经实现了这个模型，并且大大增强了精确追踪的能力。

## 1. 引言 ##

在符号执行技术中，追踪单一路径中不同内存对象的值是一通用要求，一种方式是通过实际地编译和执行程序从而得到内存对象的运行时地址，这是一种动态执行技术，程序必须要实际地执行。另外一种方式是通过静态分析技术，最简单的方式就是通过变量名追踪单一变量，忽略多级指针，数组元素和结构体字段。这无疑会牺牲很多分析资源。

这篇论文阐述的一种内存模型特别适合于C程序的符号执行技术，它使得符号执行可以准确地标识和追踪每个内存对象。此模型在分析时将C程序左值表达式映射为内存对象，因而也不需要单独的别名分析。内存模型是分析工具对代码运行时机器的存储进行的建模，它是语言语义模拟的基础和代码静态分析工具的关键组成部分。内存模型直接决定了工具模拟语言语义的准确度并影响工具发现缺陷的能力。

和其它高级语言不同，C语言模拟了一种相对低级的内存模型并且提供了各种扩展的内存访问操作，比如多级指针，指针运算，内置数组和结构体类型。C中的指针可以内存任意地址，并且可以在不同类型间自由转换，这些特性使得精确模拟C语义比较困难。

## 2. 名称绑定模型 ##

名称绑定模型在语义文本中是最基础的存储模型代表。在此模型中，计算机内存被看做 name-value 对，当赋值表达式被调用，将表达式左边的name绑定到右边表达式的值，虽然这个模型非常通用，但它不足以模拟C语义，考虑以下代码：

int x, y;
    int *p = &x;
    x = 3;
    *p = 4;
    y = x;

在这个例子中，p是一个指向变量x的指针变量。指针的存在会导致别名混淆问题，即一片内存地址有超过两个的名称。例如，\*p和x是同一片内存地址的不同别名。

名称绑定模型无法处理别名混淆问题，当我们修改一个变量的值时，需要同步修改所有此变量对应别名的值，但是在内存模型中我们无法知道某片内存地址的所有别名。

## 3. 数组模型 ##

名称绑定模型的一个缺点是缺少内存地址的概念，然而，C中的指针设计就是用来操作内存的。数组模型的提出动机很简单：直观地将内存看作一个大数组，如果我们在一个数组上分配各个变量的内存，变量上的所有操作都可转化为相应的数组元素的操作，更重要的是，数组元素的索引可以看作是变量的内存位置。将名称绑定模型转化为数组内存模型：

Assume mem[] is the memory simulation array.
    Memory allocation:
    	x: mem[1], y: mem[2], p: mem[3]
    mem[3] = 1; // p = &x; mem[3] is ’p’,
    						// 1 is x’s simulation location.
    mem[1] = 3; // x = 3;
    mem[mem[3]] = 4; 	// dereference ’*’ means
    									// we have to nest mem[]’s
    mem[2] = mem[1]; // y = x;

数组模型在一定程度上优于名称绑定模型，它可以解决程序分析中的一些问题，但是它的缺点也是显而易见的。

数组模型要求每个变量要有确定的位置，这就要求我们知道每个内存对象的确切大小，一旦我们有一个不知道大小的内存对象，例如可变长度数组或者不确定大小的堆对象，数组模型将无法使用。

对内存模型的一个有效改进就是不适用单一数组，而是使用多种数组类型，每一种内存对象都有相关的数组类型。但是复合内存对象在数组模型中很难展现，例如，对于结构体数组`struct s { int d; } sa[2]`，如果我们用单一数组去实现，它也会存在单一数组模型的缺点，如果用多级数组去实现，我们将丢失内存对象间的层次关系。

## 4. 三元组区域模型 ##

正规语义模型程序状态有两组映射：Env和Store，如下：  
 E n v = V a r → L o c S t o r e = L o c → V a l u e Env = Var \\rightarrow Loc \\\\ Store = Loc \\rightarrow Value Env=Var→LocStore=Loc→Value  
第一组映射，Var表示源码中的变量，Loc表示对变量对应得内存区域；第二组映射，Loc表示一块内存区域，Value表示内存区域对应的值。名称绑定模型缺少位置的概念，数组模型确实有位置的概念，它用精确地整数表示位置，但这种具体化的位置限制了数组模型的应用。在本节中，我们开发了一种新的位置表示：region。在C程序中，一个region与左值表达式相对应的一片抽象内存块。根据C标准，左值是具有类型的表达式。也就是说，左值表达式和内存对象相关，我们用一抽象的region去表示内存对象。在基于内存模型的region中，每个左值表达式都有对应的region。

### 4.1 Region 层次 ###

我们定义了各种类型的region。对于现实生声明的变量，有 VarRegion 标识变量的声明。每个变量都有唯一的 VarRegion。如果变量是数组或者结构体类型，它含有子对象数组元素或者字段。为了表示内存对象之间的层次关系，定义了subregions。一个region可以是另外一个region的subregion，superregion指针指向subregion的super region。数组元素，有对应的 ElementRegion，它的super region 指针指向对应数组region。此外，对于结构体字段，有 FieldRegion，其super region指针指向对应结构体region。ElementRegions 通过数组regions和数组索引标识，FieldRegions由结构体regions和字段声明标识。

在C中，有三种存储类型：局部的（stack），全局的（static）以及动态分配的（heap）。region模型也有对应的 MemSpaceRegion 表示这种不同的存储类型。stack MemSpaceRegion 是所有局部变量的super region，static MemSpaceRegion为全局变量的super region，以及动态分配类型对应的 heap MemSpaceRegion。在静态分析中，有时需要符号值。假设函数参数和局部变量在函数入口处带有符号值，如果这个符号值为一个指针，它可能指向一些未知的内存块，对于这种情况，用 SymbolicRegion 表示符号指针指向的内存块。

### 4.2 Region属性 ###

除了存储类型，内存对象有大小，有些对象的大小是显式的，例如一个字符变量占一个字节大小。但是动态分配的对象可以有不确定的范围。用region-extent映射对象的region和对应大小。这个大小可以是精确的整数类型，也可以是未知的符号值。

内存状态由region的绑定操作决定，由两种类型的绑定，直接绑定和默认绑定。在一赋值语句中，例如 x = 3，我们直接将3绑定到x对应的region。默认绑定通常发生在super regions中，如果一个subregion没有绑定，可以通过它的super region的默认绑定作为它的值，例如，存在函数调用`bzero(buf);`，我们只需要设置默认绑定到buf，如果没有默认绑定，我们必须去绑定数组中的每个元素，这显然是极为不方便的。

### 4.3 Region 视图 ###

C程序允许各种类型指针任意转换。考虑以下代码：

void* p = malloc(10);
    char* buf1 = (char*)p;
    buf1[0] = 'a';
    
    int* buf2 = (int*)p;
    buf2[0] = 0;
    
    char c = buf1[0];

这是一个指针转换的例子，这种代码写法在系统程序中比较常见。程序员通常分配一块通用的内存块，然后根据不同的用法将它转换为不同的类型，那如何处理这种情况呢？

我们建立一个从region映射到它各种类型的视图：一些匿名类型region，将一个通用内存块转化为其它类型等价与给这个内存块新增一个视图。我们创建一个匿名类型的region去表示这个视图。如下图所示：

![image-20210715140301121][]

一个region可以有多个不同类型的视图。但是同一时间只能有一个视图起作用。当这个region在其它视图上被操作之后，对应其它视图应该被置为无效状态。

## 5. C语义模拟 ##

基于内存模型的region，我们可以准确地模拟C程序语义。程序状态通过两组映射建模：Environment和Store。定义Environment为表达式到值的映射：  
 E n v : E x p r → S V a l Env: Expr \\rightarrow SVal Env:Expr→SVal  
其中，Expr是C表达式的元素。SVal是各种抽象值。定义Store是从Region到值的一组映射：  
 S t o r e : R e g i o n → S V a l Store: Region \\rightarrow SVal Store:Region→SVal  
Region是内存对象的抽象表示

### 5.1 抽象值 ###

我们将符号模拟中出现的值分为两种：loc和non-loc。loc是一个region或者是unknown，loc表示一个抽象内存地址。C中的指针具有loc值。non-loc可以是一个整数，或者是一个符号整数等等。

### 5.2 左值和右值 ###

C语言标准中将表达式分为左值和右值类型。引用到内存对象视为左值表达式，其余的则为右值表达式。为了计算表达式，我们必须区分左值和右值。

### 5.3 计算规则 ###

左值表达式返回值为左值，视为一个loc

右值表达式返回一个右值，可以为loc亦可以为non-loc

C中各种主要类型的表达式计算规则如下表所示：

![image-20210715142254271][]

对于指针运算，我们假设只可能出现在元素regions中，我们获得元素region的索引，使用偏移得到下一个元素。对于动态分配的内存，我们创建一个 MallocRegion，用大小和计数区分同一语句分配的不同内存块。下面是一个计算规则应用的实例：

struct s1 { 
    	int d;
    };
    
    struct s2 { 
    	struct s1 *p;
    };
    
    void foo(void) { 
    	struct s1 data;
    	struct s2 *sp;
    	int a[2];
      
    	sp = malloc(sizeof(struct s2));
    	sp->p = &data;
    	sp->p->d = 3;
    	a[1] = data.d;
    }

当我们处理完函数foo中的三个变量声明后，程序状态如下所示：

![image-20210715143239405][]

当处理完动态内存分配后，程序状态中将新增一个region。

![image-20210715143351074][]

接下来处理 sp-> = &data，计算表达式 &data 需要data为左值，其region为1，然后我们得到sp的右值为region 7，继续更新：

![image-20210715143653607][]

处理 sp->p->d = 3，假设我们得到了sp->p的右值，为region1，还有sp->p->d的左值，为region2.更新如下：

![image-20210715143837678][]

接着处理 a\[1\] = data.d，data.d的左值为region2，右值为3，a\[1\]左值为region6，程序状态如下：

![image-20210715144127505][]

![image-20210715144635448][]

## 6. 一个实例 ##

在下面将用一个实例展示基于内存模型的region的强大之处，考虑以下代码片段：

struct s { 
      int data[2];
    };
    
    void f(struct s buf) { 
      int i = 3, *q = NULL;
      struct s *p;
    
      if (buf.data[1] == 1) { 
        q = &i;
      }
      p = &buf;
      if (p->data[1] == 1) { 
        p->data[0] = *q;
      }
      return;
    }

在这段代码中，如果我们不追踪字段 buf.data\[1\]，有一条路径将会产生空指针解引用。有了region内存模型，我们可以准确地知道 buf.data\[1\] 和 p->data\[1\] 引用同一内存对象，因而路径条件不能同时满足。当 buf.data\[1\] 被计算后，我们得到相关的region，buf, buf.data以及buf.data\[1\]。得到buf.data\[1\]的值，是一个符号值 $1，当 p->data\[1\] 计算时，我们首先得到p的右值，是内存区域buf，沿着相同的路径，得到buf.data\[1\]的值 $1。所以此段代码并不会产生空指针解引用问题。

![image-20210715153647663][]

原文链接：[A Memory Model for Static Analysis of C Programs][]

[image-20210715140301121]: /images/20221004/7c94bbd21bc04a0eba6b699b86a0f270.png
[image-20210715142254271]: /images/20221004/58d0df88261847ac84bef32106870597.png
[image-20210715143239405]: /images/20221004/fa63c766fdc841dbaa6c85d4b85f84c7.png
[image-20210715143351074]: /images/20221004/7a3bf948814c4ac081340d7b7450418d.png
[image-20210715143653607]: /images/20221004/92c7de2fc15a4fa1b76f14eef72eb208.png
[image-20210715143837678]: /images/20221004/c7f499fa14154a1fb91269092dae499a.png
[image-20210715144127505]: /images/20221004/6272b5f8024f46d3b36c3ad6f45eb09b.png
[image-20210715144635448]: /images/20221004/b368fd007ec64e93b2d2cfe0c5f7a221.png
[image-20210715153647663]: /images/20221004/bf59f4b89c8e4ceebaeeab5091d83be4.png
[A Memory Model for Static Analysis of C Programs]: http://lcs.ios.ac.cn/~xzx/memmodel.pdf