目前在对C/C++漏洞的检测,研究比较深入的是针对源代码静态扫描技术,主要的静态分析方法有以下几类。

  词法分析:是早被用来进行缓冲区溢出漏洞检测的方法。这种方法是对软件源程序进行扫描分析,同时与特征库进行匹配,进而找出软件程序中可能存在的溢出漏洞。这种方法的局限性在于容易产生漏报或误报,并且它也不能理解软件程序的语义。因此需要进一步的进行上下文分析

  约束分析:通过产生、求解程序的约束条件,约束分析即可确定程序的性质。约束分析方法建立的局部化约束产生的规则能清楚的描述指令副作用乃至控制条件。但是,这种方法不容易处理精确循环:程序中存在循环,且循环控制条件之间存在依赖关系时,则建立的约束条件可能无解。

  抽象解释:抽象解释把程序代码的执行过程看成各种抽象状态的迁移过程,并通过对抽象状态进行分析来确定程序的性质。初始抽象状态必须是初始实际状态的安全近似,而且每次状态迁移需要保持正确的关系,这样才能保证分析结果的正确。理论上,正确的抽象能够找出程序中所有可能的缓冲区溢出漏洞。但也相应的带来较多的误报。在实际使用中,为降低误报率,用户应当根据被测程序的特性,选择合适的解释函数抽象域等。

  类型推导:将安全属性看成一种类型,则通过类型检查找出发现源代码中不安全的类型。这种方法利用定型规则确定代码中部件的的类型,不考虑代码执行条件和顺序,故处理速度很快。但由于约束变量取值为无穷,所以这种方法也只能用来检测特定类型的缓冲区溢出漏洞。

  数据流分析:数据流分析方法基于这样一个事实,数据流沿程序控制图传播。当所有程序点的分析状态达到不动点时,传播停止,同时得到程序性质的解。但是数据流分析方法不能精确跟踪指令的控制条件,所以这种检测方法得到的结果不够精确。

  模型验证:模型验证用状态迁移来描述程序的行为,是一种形式化的验证技术。这种方法用时序逻辑和计算树逻辑等来表示程序系统的性质,于是将系统属性(安全与否)的检验问题变换为搜索不符合逻辑公式的状态问题。模型验证要遍历程序的所有状态空间,于是它只能分析那些有限状态的系统,有较大的局限性。

  其中词法分析是基础也是应用广泛的分析方法,下面是以词法分析为基础,并结合了上下文分析的一个模型,如图:

  描述:

  对C/C++代码进行检查,首先需描述出代码应满足的属性,再通过对源代码的分析判断它们同相应属性是否一致,如果不一致则表示代码中存在错误。按照这一方法,在对源代码中存在的漏洞进行检测之前,首先需要对可能存在的漏洞进行形式化的描述,然后判断代码中是否存在所描述的漏洞。

  如何形式化的描述:

  1、该漏洞涉及到程序中哪些方面的属性,即分析缓冲区溢出漏洞在程序中的表现,建立程序模型和漏洞模型。

  2、使用什么方法判断源代码同相应属性的一致性,即将漏洞模型转化为程序可达性判定问题。

  具体过程如下:

  (1)建立程序模型,从程序中抽象出漏洞相关变量的属性,并抽象出这些属性变化的过程

  (2)建立安全漏洞模型,描述所关心变量的属性应该满足的约束条件

  (3)将漏洞模型的检测转化为可达性判定问题,使用安全漏洞模型检测方法进行检测