基于约束分析和模型检验的代码安全漏洞检测方法

摘要

基于模型检测和约束分析的源代码漏洞检测方法，可以对C程序的源代码进行约束提取，使用模型检测来检测程序的安全漏洞。主要内容包括：利用约束分析技术对C程序源代码中涉及到得缓冲区属性信息进行提取，并利用这些缓冲区属性信息，在变量声明、变量赋值、函数调用点插入相应的属性生成、属性传递、属性约束的ASSERT语句信息；经过插装后的代码，可以作为模型检测的输入，对其进行可达性判定，找到程序中的危险点是否真正存在一条可达性路径，进而发现源代码中的安全漏洞。单独的模型检测目前还不能对缓冲区等安全漏洞进行检测，本方法结合约束分析的静态检测技术和模型检测技术实现了对缓冲区溢出等安全漏洞的检测，并且检测精度比一般的静态检测技术要高。通过对源代码其他危险函数信息的提取，进行相应的插装过程，本方法还可以对格式化字符串、代码注入、权限提升等安全漏洞进行检测。

说明书

技术领域：

本发明涉及一种源代码漏洞检测的静态检测方法。

背景技术：

随着信息技术的发展，计算机软件已经渗透到国民经济的各个领域中，并与人们的生产生活息息相关。软件的安全问题也越来越凸显其重要性，一些关键软件一旦遭到破坏，将会造成行业性乃至全国性的瘫痪。恶意的用户可以针对特定软件的bug，运行恶意的代码从而得到访问非法数据的权限。缓冲区溢出漏洞是目前这类安全漏洞中最主要的一种。恶意的用户可以通过分析程序的输入数据格式，并确定这些数据存放在程序的缓冲区中，这样用户就有可能通过特殊的输入数据，将栈空间的敏感数据覆盖掉，特别的将保存的返回地址替换为用户自己定义的非法代码的地址，这样非法用户就可以控制程序流程、执行非法操作。

软件的漏洞可以通过静态方法和动态方法进行检测。静态方法分为一般的静态检测方法和基于完备理论的形式化验证方法，第一类主要是基于程序分析的方法检查代码中可能存在的漏洞；第二类方法则以形式逻辑、自动机理论为基础，验证程序是否具有某种性质。程序分析的方法不能够对程序的所有状态进行穷举，因此精确度欠佳，模型检测可以对所有程序的状态进行穷举，然而为了验证一个短小程序的性质，需要搜索的程序状态可能就非常庞大，因此纯模型检测的方法不能有效地进行漏洞检测。目前比较有效的一种模型检测方法是基于抽象-验证-细化范例的软件模型检测方法，代表工具是加州大学伯克利分校研制的Blast，这种方法能够适当忽略与安全漏洞属性不相关的代码，从而简化了整个验证过程。这不仅可以增加检测出的漏洞数目而且可以减小误报率，提高检测精度。与静态检测方法不同的是，动态检测技术对程序的规模没有限制，可以对大型程序进行检测，然而明显的不足是动态检测技术对输入的依赖性，只有当特定的输入使程序执行到危险点时，漏洞才会被发现，从而导致误报率较高。

单纯的模型检测方法一般不能直接检测程序的漏洞，比如Blast曾借助于Securd检测程序中空指针的引用问题，但是不能检测更复杂缓冲区操作的安全性。而关系到系统安全的漏洞检测用单纯的模型检测方法就更加困难，所以一般都需要借助于其他的程序分析方法来配合模型检测对这类的缓冲区溢出漏洞进行检测。

发明内容：

本发明要解决的技术问题是：针对单纯的模型检测难以检测安全漏洞的问题，提出一种结合约束分析的模型检测的方法来对缓冲区溢出漏洞进行验证，目前该方法能够实际地应用于中小规模的程序中，并且具有低误报率的优点。

本发明采用的技术方案是：基于约束分析和模型检测的漏洞检测方法，其特征在于：利用模型检测所具备的可达性分析，对经过约束分析提取后的约束模型进行可达性判定，将安全漏洞检测问题转变为可达性判定问题，利用一阶谓词公理系统进行模型求解，从而判断和分析出安全漏洞以及引发路径。

本发明采用语法制导的方法，在GCC的抽象语法树上进行约束分析，建立了一套针对缓冲区溢出漏洞的约束分析机制，为缓冲区增加属性长度信息，不同的缓冲区操作语句对应于不同的属性约束生成。为描述整个约束分析过程，首先对C语言进行抽象，分析过程非流敏感的，不会处理控制流信息，为简化分析本发明将所关心的C语言语法进行抽象，包括指针变量、整型变量、函数调用、内存分配以及赋值语句。根据这些语法抽象对缓冲区的操作，生成相应的属性处理语句，而生成规则是由xml配置文件给出，该文件将直接指导缓冲区属性模型的建立。

整个约束分析过程主要分如下几个部分：

(1)将每个缓冲区与包含最大长度(max_length)和已用长度(used_length)的整数值对相关联，本发明称此整数值对为相应缓冲区的属性或属性信息；

(2)将与缓冲区相关的语句和函数调用抽象为对缓冲区属性信息的操作，包括属性传递(更新)和属性验证；

(3)通过(1)(2)的分析建立关于缓冲区属性的约束模型，用模型检测算法对属性约束模型进行求解，最终确定程序是否存在安全漏洞。

模型检测是一种验证给定的系统是否满足特定的性质的技术。给定一个待检测的系统和系统相关的性质描述，通过模型检测算法的执行，算法可以证明此系统是否满足给定的性质，如果系统不满足给定的性质，系统会给出以一个包含反例的错误报告。以安全漏洞的检测为例，模型检测算法的输入是程序代码或系统和一阶谓词类型的性质或性质描述，如果给定的性质P满足，表明对于给定缓冲区的操作或变量的访问是安全的。通过标准的编译器前端分析，将针对指针、数组的定义、指针引用、数组访问以及危险函数的调用等都添加了缓冲区属性约束的更新与断言信息，如果属性断言或属性性质不成立那么程序流会到达错误标签，从而检测出一个安全漏洞，所以安全漏洞问题已经成功转化为对错误标签ERROR的可达性问题。

本发明首先将缓冲区抽象为包含缓冲区最大长度和已用长度的整数值对，并称其为对应缓冲区的属性，且将对缓冲区的各种操作(包括指针赋值，函数调用等)抽象为对缓冲区属性长度的操作，因此程序是否存在安全漏洞需要验证的性质P是：对于所有的缓冲区的操作，需验证s_max＞＝s_used是否成立，同时更新缓冲区的属性信息。

附图说明

图1为本发明方法实施的结构图解；

图2为约束分析的具体实施方式，利用xml配置文件对GCC指导进行插装；

图3a为插装前和插装后的代码之间的对比，图3b中虚线标出的为插装代码；

图4为将属性模型中的断言信息转变为用于Blast检测的错误标签；

图5为Blast对属性约束模型检测的结果，图中所示文件路径可显示漏洞的实际路径，方便程序人员手工查找和确认。

具体实施方式

本发明首先通过静态分析，用约束分析的方法追踪程序中变量信息的变化，为缓冲区添加属性信息并记录缓冲区的范围，在变量声明、变量赋值、函数调用点插入相应的属性生成、属性传递、属性验证的语句信息，构建一个缓冲区属性约束模型，然后通过Blast来验证属性模型中的危险点是否可达，将安全漏洞检测问题转化为对程序某个位置的可达性判定问题，从而保证了对源代码漏洞的精确检测。结构图如图1。

1.约束分析

首先将缓冲区抽象为包含缓冲区最大长度和已用长度的整数值对，并称其为对应缓冲区的属性，且将对缓冲区的各种操作(包括指针赋值，函数调用等)抽象为对缓冲区属性长度的操作，因此程序是否存在安全漏洞需要验证的性质是：对于所有的缓冲区的操作，需验证s_max＞＝s_used是否成立，同时更新缓冲区的属性信息。在这里用基于格的程序分析框架对此进行建模：

令代表整数集合，并令是的扩展，并假定整数集合对有如下形式：下面定义上的一个完全格：

其中⊥，T是中的幺元，是集合上的偏序关系，min和max是上的操作，+，-，×是上二元运算，运算法则是一般算术运算的简单扩充。

对于每个字符串S的操作定义需要满足如下约束断言：assert(S.max＞＝S.used)。如果赋值操作满足一个约束系统，换句话说待检测的系统是安全的，必须满足当赋值操作完成，缓冲区属性信息更新后，每个约束断言必须是成立的。约束系统的极小解是满足此系统的最小赋值，其中极小解的求解是通过模型检测算法进行的。

2.属性模型

在上一步的基础上对缓冲区的属性进行建模，需要建立一个可以使用模型检测工具进行验证的属性模型，对属性的不同操作行为是构建模型的依据，由此可以将这个建模的过程分成三个部分：属性初始化、属性传递和属性验证。当缓冲区建立时，如在数组定义、malloc类内存分配函数的调用点会伴随缓冲区的建立，此时对相应缓冲区的属性进行初始化；在指针赋值操作、字符串相关的库函数等位置处理缓冲区属性的传递，相应更新缓冲区的属性；在对缓冲区的访问点需要对缓冲区访问是否越界进行验证。

现在漏洞检测问题也就变成了判断危险点出处属性性质是否满足，即自程序入口到危险点的可达性问题，约束系统的求解可用完备的模型检测算法来完成，利用模型检测算法对约束系统进行求解，最终确定漏洞。

整个分析过程是基于GCC的抽象语法树进行的，通过遍历抽象语法树，首先生成缓冲区的属性信息，对于涉及缓冲区操作的语法树结点生成相应的属性约束和属性更新表达式，属性信息的初始化、传递、断言构成了整个约束系统。不同属性信息的生成，由漏洞配置文件具体指导，对于不同的语法树结点，在配置文件中匹配合适的属性生成规则，最终生成整个缓冲区属性约束模型，如图2所示。

(1)属性初始化

对于数组定义char a[n]，有type(a)＝ref，对a所指向缓冲区的属性max(a)和used(a)分别初始化为n和0，可以用公式(1)来表示。

$\frac{\mathrm{type}\left(a\right)=\mathrm{ref},\mathrm{type}\left(n\right)=\mathrm{int}}{\mathrm{inta}\left[n\right]}\Rightarrow \left(\begin{array}{c}\max \left(a\right)=n\\ \mathrm{used}\left(a\right)=0\end{array}\right)---\left(1\right)$

在malloc内存分配类函数的调用点，也会伴随缓冲区属性的初始化，max属性初始化为malloc函数的参数，而used属性则初始化为0。值得说明的是malloc参数可能是变量或表达式，属性初始化可以用公式(2)来表示。

$\frac{\mathrm{type}\left(p\right)=\mathrm{ref},\mathrm{type}\left(\exp \right)=\mathrm{int}}{p=\mathrm{malloc}\left(\exp \right)}\Rightarrow \left(\begin{array}{c}\max \left(p\right)=\exp \\ \mathrm{used}\left(p\right)=0\end{array}\right)---\left(2\right)$

(2)属性传递

对于赋值语句p＝q，如果p和q的类型是指针类型，即type(p)＝ref，type(q)＝ref，这里q并不单纯指指针变量，可能是结构体内的指针变量、返回值是指针的函数调用或指针运算等，此语句执行完后p放弃原先的内存指向，转为指向q所对应的内存，指针赋值语句对应的属性变化规则是：max(p)＝max(q)，used(p)＝used(q)，可以用公式(3)来表示。

$\frac{\mathrm{type}\left(p\right)=\mathrm{ref},\mathrm{type}\left(q\right)=\mathrm{ref}}{p=q}\Rightarrow \left(\begin{array}{c}\max \left(p\right)=\max \left(q\right)\\ \mathrm{used}\left(p\right)=\mathrm{used}\left(q\right)\end{array}\right)---\left(3\right)$

指针算数运算也会影响指针缓冲区的属性，如果p是指针，n是整型变量，则p＝p+n执行完后p所指向的缓冲区属性也会相应改变，属性变化规则是：max(p)＝MAX{max(q)-n，0}，used(p)＝MAX{used(q)-n，0}，可以用公式(4)来表示。

$\frac{\mathrm{type}\left(n\right)=\mathrm{int},\mathrm{type}\left(p\right)=\mathrm{ref}}{p=p\pm n}\Rightarrow \left(\begin{array}{c}\max \left(p\right)=\mathrm{MAX}\{\max \left(q\right)\overline{+}n,0\}\\ \mathrm{used}\left(p\right)=\mathrm{MAX}\{\mathrm{used}\left(q\right)\overline{+}n,0\}\end{array}\right)---\left(4\right)$

为支持过程间分析，本发明也对函数和函数调用语句进行了抽象。在涉及过程间缓冲区传递的函数调用点，引入与函数相关的缓冲区属性。例如，在调用函数fun时，如果fun有指针类型的参数，则将实参p的max属性max(p)传递给函数fun形参的max属性，同样将used属性也进行传递。在函数fun返回前，如果返回值是指针类型，则需要将返回的缓冲区属性传递给max(fun_ret)和used(fun_ret)，在调用fun程序点将max(fun_ret)和used(fun_ret)传递给相应的左操作数(如果有的话)。

缓冲区相关的最重要的一类操作是库函数，比如strcpy、strcat等，这些字符串库函数的操作也伴随缓冲区属性的改变，我们目前可以处理40多个库函数，不同的库函数对缓冲区的影响也各不相同，下面以strcpy和strcat为例说明属性传递规则，我们已将这些规则描述为XML文档，此文档直接指导整个分析过程。

当遇到strcpy(p，q)语句时，p和q的类型均为指针，此语句执行完后p指向的缓冲区内容被q所指向的缓冲区内容所覆盖，所以会有：max(p)＝max(q)，used(p)＝used(q)，可以用公式(5)来表示。

$\frac{\mathrm{type}\left(p\right)=\mathrm{ref},\mathrm{type}\left(q\right)=\mathrm{ref}}{\mathrm{strcpy}(p,q)}\Rightarrow \left(\begin{array}{c}\max \left(p\right)=\max \left(q\right)\\ \mathrm{used}\left(p\right)=\mathrm{used}\left(q\right)\end{array}\right)---\left(5\right)$

当遇到strcat(p，q)语句时，p，q的类型均为指针，此语句执行完后q缓冲区内容被连接在p所指向的缓冲区内容的后面，所以会有：max(p)＝max(p)，used(p)＝used(p)+used(q)，分析过程可以用公式(6)来表示。

$\frac{\mathrm{type}\left(p\right)=\mathrm{ref},\mathrm{type}\left(q\right)=\mathrm{ref}}{\mathrm{strcat}(p,q)}\Rightarrow \left(\begin{array}{c}\max \left(p\right)=\max \left(p\right)\\ \mathrm{used}\left(p\right)=\mathrm{used}\left(p\right)+\mathrm{used}\left(q\right)\end{array}\right)---\left(6\right)$

(3)属性验证

本发明将访问缓冲区的语句定义为危险点。在危险点需要对缓冲区属性进行验证，比如遇到p＝’a’时，需要验证max(p)是否大于0，如果max(p)大于0，则对缓冲区的写入是安全的，否则该危险点是一个漏洞，实际的验证是由模型检测算法来完成。

目前处理的危险点包括数组的引用、指针的引用和缓冲区相关的库函数三类，前两类都可以归为一类。

当遇到数组和指针引用是比如*p＝’a’，我们需要对p所指向缓冲区的大小进行验证，验证max(p)是否大于等于1，可以用公式(7)来表示。

$\frac{\mathrm{type}\left(p\right)=\mathrm{ref}}{*p{=}^{\prime }{a}^{\prime }}\Rightarrow \mathrm{assert}(\max \left(p\right)\ge 1)---\left(7\right)$

当遇到字符串相关的的危险函数(strcpy，strcat等)时，也需要对目标缓冲区的大小进行验证，同样以strcpy和strcat为例进行分析。当遇到strcpy时，目标缓冲区的最大长度必须大于原操作数字符串的长度，可以用公式(8)来表示。

$\frac{\mathrm{type}\left(p\right)=\mathrm{ref},\mathrm{type}\left(q\right)=\mathrm{ref}}{\mathrm{strcpy}(p,q)}\Rightarrow \mathrm{assert}(\max \left(p\right)\ge \mathrm{used}\left(q\right))---\left(8\right)$

类似的，strcat的处理方式可以用公式(9)来表示。

$\frac{\mathrm{type}\left(p\right)=\mathrm{ref},\mathrm{type}\left(q\right)=\mathrm{ref}}{\mathrm{strcat}(p,q)}\Rightarrow \mathrm{assert}(\max \left(p\right)\ge \mathrm{used}\left(p\right)+\mathrm{used}\left(q\right))---\left(9\right)$

以上的分析过程实际上是将缓冲区的属性看作一个整数区间：[used(buf)，max(buf)]，随着程序的执行，整数区间也在不断变化，实际上建立的模型是关于整数区间的属性模型。分析过程会以插装代码的方式返回，插装之前和插装之后的代码对比如图3所示，插装后的代码包括所有需要的属性信息，可以用于后端的模型检测进行可达性分析。

3.模型检测

在上一步所建立的属性模型下，使用模型检测工具Blast来进行漏洞验证。在上一步中，我们通过增加缓冲区属性信息，并根据不同的C语言语法抽象对属性信息进行初始化更新等操作，增加对缓冲区属性的验证信息，通过约束分析将程序建立成缓冲区属性模型，使得模型检测工具Blast能够对该模型中的验证信息进行分析。

Blast是一个控制流敏感、且支持过程间分析的模型检测工具。由University ofCalifornia的Thomas A.Henzinger等人开发。Blast对C语言代码的空指针引用错误进行了精确的检查，误报率很低；另外Blast可以进行代码的可达性分析，也就是判断程序是否可以从入口出开始执行并到达某个指定的位置。

使用Blast对上一步中所建立的属性模型进行可达性分析。对于属性模型中所生成的属性约束，通过宏替换转变为Blast需要验证的标签(图4)，如果该标签可达，则表明该处存在一个安全漏洞。Blast使用反例制导的方法进行可达性分析，可以将从程序入口到该标签的执行路径记录下来，通过对路径跟踪可以分析出产生安全漏洞的执行路径，方便程序人员手工查找和确认。图5示意所得到的漏洞检测结果，在该结果中显示漏洞路径文件的所在位置及文件名，打开该文件即可看到漏洞路径的具体信息。