软件学报  2014, Vol.25 Issue (2): 357-372   PDF    
基于区域内存模型的C程序静态分析
董玉坤1,2, 金大海1, 宫云战1, 邢颖1    
1 网络与交换技术国家重点实验室(北京邮电大学),北京 100876;
2 中国石油大学(华东)计算机与通信工程学院,山东 青岛 266580
摘要:为了提高程序的静态分析精度,提出了一种应用基于区域的符号化三值逻辑(region-based symbolic threevaluedlogic,简称RSTVL)的静态分析方法.RSTVL能够描述C程序运行时内存中数据结构的形态信息与变量的存储状态,以及可寻址表达式间的各种关系,包括指向关系、层次关系与取值逻辑关系.为了提高静态分析的精度,提出了一种基于RSTVL的流敏感、域敏感的过程内分析与基于符号化函数摘要的上下文敏感的过程间分析,能够精确地分析出每个程序点上的形态信息、数据流信息与指针指向关系.实验结果表明,相对于基于符号化三值逻辑的方法,该分析方法在保证一定分析效率的前提下,能够实现较高准确度的分析.
关键词可寻址表达式     内存模型     静态分析     符号化函数摘要     缺陷检测    
Static Analysis of C Programs via Region-Based Memory Model
DONG Yu-Kun1,2, JIN Da-Hai1, GONG Yun-Zhan1, XING Ying1    
1 State Key Laboratory of Networking and Switching Technology (Beijing University of Posts and Telecommunications), Beijing 100876,China;
2 College of Computer and Communication Engineering, China University of Petroleum, Qingdao 266580, China
Corresponding author: DONG Yu-Kun, E-mail: dongyk@upc.edu.cn
Abstract: In order to improve the precision of static analysis for C procedures, this paper introduces a static analysis method applying region-based symbolic three-valued logic (RSTVL). RSTVL can describe shape of data structures, all kinds of memory states and relations of addressable expressions including alias relations, hierarchical relations and logic relations. To improve precision, a RSTVLbased analysis method is proposed to analyze the shape, dataflow and point-to relationship at every procedure point. The method facilitates flow-sensitive and field-sensitive intra-procedure, and context-sensitive inter-procedure analysis based on symbolic function summary. Experimental results validate that the porposed static analysis method offers higher precision on the precondition with no efficiency loss.
Key words: addressable expression     memory model     static analysis     symbolic function summary     defect detection    

C语言能够作为嵌入式软件开发的主导语言,主要是因为C语言作为高级语言提供了指针与位操作,又具有可以直接对硬件进行操作等低级语言的特性,但这些特性难免也会造成程序中存在一些代码级别的缺陷.代码级别缺陷会导致运行时程序状态违背程序安全属性的要求,例如数组越界、空指针引用、非法计算、缓冲区溢出等,引发不可预测的异常.为了检测程序的代码级别的缺陷,通常进行静态分析,静态地获得程序运行时状态,判断运行时状态是否满足程序安全属性从而判断是否存在缺陷.但静态分析无法分析程序的所有非平凡属性,只能获得近似的结果,而静态分析的精度决定着缺陷检测结果的准确度.尽管过去的研究提出了一些静态分析的方法并开发了相应的工具,但依然有两个核心问题影响分析的精度:一是如何准确地表示内存对象的存储以及全面描述变量间的各种关联;二是如何用抽象的方法精确地处理各种程序语义.

C程序包含指针、结构体、数组等复杂数据类型,引发可寻址表达式[1]间主要有指向关系、层次关系、取值逻辑关联这3种关系.全面地静态分析需要考虑分析这3种关系,否则会导致分析精度的下降.对C程序的分析研究主要有数据流分析、指针分析、形态分析.数据流分析主要用于分析程序运行时变量的取值情况;指针分析用于分析程序运行时的指针指向信息;形态分析主要用于判断程序运行时内存中数据结构的形态信息,能够精确地分析出变量间的指向关系与层次关系.为了全面地表示程序中可寻址表达式间的3种关联关系,首先需要以某种方式对内存存储进行抽象.基于不同的静态分析目的与精度的需要,一种方法是只描述内存对象间的一部分关系,例如,大数组模型[2]难以描述内存对象间的层次关系,形态图[3]与TVLA[4]未考虑内存单元上存储信息间的关联,指向图[5]只描述指向关系,基于区域的模型[6]是未考虑取值的逻辑关联,STVL[7]考虑了取值的逻辑关联但不能描述复合数据类型的层次关系;另一种方法是对被测程序进行限制[8],例如,要求被分析程序没有动态内存分配,并且是完全的类型安全.

为了保证静态分析的精度,需要进行敏感的分析.例如,流敏感[9]考虑语句的执行顺序,域敏感[10]考虑复合数据类型与成员的关系,上下文敏感[5]考虑函数调用上下文信息,路径敏感[11]考虑路径条件.敏感的分析方法会提高分析的精度,但分析的代价随之升高,分析的效率也随之下降.为了平衡分析的精度与效率,大多数静态分析方法是流敏感与上下文敏感的.

因为静态分析的两个核心问题的困扰,导致目前对C程序的静态分析主要存在3点不足:(1) 未能全面地描述变量的存储状态;(2) 对域敏感分析考虑得不够,导致对复合数据结构的处理不够精确;(3) 未将数据流分析与指针分析、形态分析有效地结合起来.

鉴于上述问题,本文试图从3个方面进一步提高静态分析的精度:一是给出一个能够更准确地描述运行时程序状态的内存模型;二是有机地结合各种敏感分析方法;三是在一个统一的框架下进行数据流分析、指针分析与形态分析.为此,本文提出了一种应用RSTVL(region-based symbolic three-valued logic)的C程序静态分析方法.RSTVL能够全面地描述内存对象的存储状态以及可寻址表达式间的各种关联,基于RSTVL的分析将对变量的操作映射到对区域的操作.基于RSTVL的过程内分析是流敏感与域敏感的,过程间分析是上下文敏感与域敏感的.

本文第1节介绍RSTVL.第2节介绍基于RSTVL的过程内分析.第3节介绍基于RSTVL的过程间分析.第4节通过实验对本文方法进行评估.第5节介绍相关工作.第6节对全文进行总结.

1 基于区域的符号化三值逻辑

静态分析的主要任务是分析程序的具体语义,即,获得程序的存储状态.存储状态是内存对象在程序点上状态的集合,存储状态包括左值表示的内存单元的地址信息与右值表示的值信息.

一个程序P可表示为六元组(V,L,S,t,init,end),其中,VVars,为程序P的变量集合;L为程序点集合;SStmts,为程序语句集合;tLxSxL,表示迁移关系;initL,为程序P的起点;endL,为程序P的终点.Worklist[12]算法作为迭代算法的一种实现,从程序的起点init开始,基于迁移关系t,分析出在每个程序点lL上的变量vV的状态信息,直至程序的终点end结束.如果有一种静态分析方法A对一种语言L开发的任一程序P,如果在P的任一程序点l上计算出的内存单元取值都包括实际运行时可能的取值,则称A为可靠的.

C程序包含指针、结构体、数组等复杂数据类型,可寻址表达式间可能存在指向关系、层次关系、取值逻辑关联等多种关系,而且提供了指针算术、动态内存分配、强制类型转换等操作,这都增加了对C程序进行静态分析的难度.

1.1 引 例

图 1为3个C程序的例子.对于程序片断图 1(a),L9语句处的指针引用表达式*pst[i]→m的引用路径上还隐含着3个表达式:pst,pst[i],pst[i]→m;而L7语句处的表达式pst[i]与L9处的表达式pst[i]虽然名称一样,但其实是两个不同的表达式.

对于程序片断图 1(b),当L6语句处的取地址操作执行完以后,L7语句处的sppddata.d具有别名关系,导致L7语句处的赋值操作后data.d的值也为-10.而经过L9的分支语句,L10语句处的j的值为1或0,若采用路径不敏感的分析,则被赋值的a[j]可能是a[1],也可能是a[0],只能进行弱更新操作.

对于程序片断图 1(c),L10语句处的实参s将会受到被调用函数f3的副作用影响,s.a的指向信息将会发生改变.而调用函数f3的返回值也由传递的参数决定,需要分析实参与形参的对应关系才能获得更精确的结果.

Fig. 1 Motivating examples 图 1 程序示例

图 1的3个程序片断可以看出:C程序中具有复杂的表达式,而且这些表达式间可能存在多种关联,函数调用更加剧了分析的复杂性.为了实现对C程序较精确的分析,静态分析方法需要能够对C语言的各种类型的表达式进行准确的描述,并能对程序运行时的内存状态进行描述,以获得相关变量间的各种关联,对函数调用需要考虑调用点的上下文环境.

1.2 可寻址表达式

在程序中,表达式是一个由操作符与操作数组合的序列,规定了对一个值的计算.表达式的值有左值与右值之分,表达式的左值是指它代表的内存对象的地址,表达式的右值是指对表达式求值所得到的值.

定义1(内存对象). 程序运行时所分配内存对应的表达式,包括顶级变量v、复合类型内存对象的成员、动态分配的内存块.C99所支持的内存对象var的语法可归纳为

其中,v为顶级变量,exp表示参数.

定义2(可寻址表达式). 内存对象与具有左值且可被赋值的表达式.

对可寻址表达式进行操作,将影响内存单元的存储状态.C99所支持的可寻址表达式e的语法可归纳为:

e::=var|e.f|ef|e[exp]|(e)|*e|m(exp),其中,m为函数指针,exp表示参数;

*e::=*e'|*(++e')|*(--e')|*(e'++)|*(e'--)|*(e' op exp'),其中,e'为指针,op=+|-,exp'为整型表达式.

C程序中的数据类型可分为标量类型与复合类型:标量类型包括基本类型、指针类型;复合类型包括数组、结构体、联合.因为联合已较少使用,本文不再对联合类型进行分析.下面给出父变量的概念.

定义3(父变量). 复合类型变量为其成员的父变量.ee.f,e[exp]的父变量.

虽然每个可寻址表达式在运行时会对应一块内存区域,但是某些可寻址表达式在不同的执行上下文环境下,它们所对应的内存区域可能会不一样.例如程序片断图 1(a)中的L9语句处的pst[i].程序运行时只为内存对象分配区域,内存对象包括声明的顶级变量、复合类型变量的成员、动态分配的内存块等.在程序片断图 1(a)中的可寻址表达式中,sst,i,pst,j等是内存对象,但*sst,**sst,pst[i]→m,*pst[i]→m等不是内存对象.

可寻址表达式因为内存单元间的左值或右值间的关联而存在以下3种关联:

(1) 左值与右值间的关联,称为指向关系,是由指针与所指向的变量产生的关系.指向关系会引发多个可寻址表达式对应同样一块内存区域,这些可寻址表达式之间具有别名关系.

(2) 左值间的关联,称为层次关系,是指复合类型可寻址表达式与其成员的关系.

(3) 右值间的关联,称为取值逻辑关系,是指基本类型的可寻址表达式在取值上的线形关系或逻辑关系.

1.3 基于区域的符号化三值逻辑

要全面并精确地分析出所有内存对象的存储状态,需要考虑可寻址表达式间的各种关联.文献[6]构建了基于区域的三元模型<Var,Region,Value>,考虑了指向关系与层次关系,但Value只能表示具体的值或区域编号,未考虑取值逻辑关系,而且该模型只适用于单路径的分析.文献[7]的STVL是一个三元模型<Var,SExp,Domain>,考虑了取值逻辑关系,但未能很好地处理层次关系与指向关系.本文结合文献[6]基于区域的三元模型与文献[7]的STVL的优点,提出了基于区域的符号化三值逻辑——一个基于区域的内存模型.

定义4. 基于区域的符号化三值逻辑RSTVL定义为四元组,RSTVL=áVar,Region,SExp,Domain∇,其中,Var表示内存对象,Region表示区域,SExp表示符号表达式,Domain表示取值区间.

基于RSTVL的静态分析构成一个三值逻辑命题3vl,即áVar,Region,SExp,Domain∇→{0,1,1/2},3vl→0表示Var取值为未知区间,3vl→1表示Var取值为具体区间值,3vl→1/2表示Var取值为符号值.

四元组RSTVL用来描述标量类型的内存对象.复合类型的内存对象可分解为标量类型成员的组合,用三元组áVar,Region,c∇表示.c的含义由Var的类型决定:如果Var是数组类型,则c是{ái,Region∇},iN是数组Var的下标;如果Var是结构体,则c是{áf,Region∇},f是结构体Var的成员.

对不同类型的内存对象,RSTVL用不同类型区域对其存储状态进行抽象描述:PrimitiveRegion描述基本类型的内存对象,PointerRegion描述指针,ArrayRegion描述数组,StructRegion描述结构体.每个区域都有唯一的编号:PrimitiveRegion的编号形式为bm_i(iN),PointerRegion的编号形式为pm_i,ArrayRegion的编号形式为am_i, StructRegion的编号形式为sm_i.对动态分配的无名内存,用mxm_i_n(x表示区域的类型,取值为“b”,“p”,“a”,“s”)编号的区域描述,其中,n为该无名内存的字节数.空地址的区域编号为null,野地址的区域编号为wild.规定参数与全局变量的区域编号额外设置首字母“u”与“g”.

定义5. 将对内存对象分配的区域称为安全区域,将动态分配的区域称为动态区域.对这两种区域统称为可操作区域.将nullwild标志的区域称为不可操作区域.

动态区域经过非空判断后变为安全区域,动态区域经过是空判断后变为不可操作区域.

定义6. 符号表达式SExp由符号通过数学运算与关系操作构成,递归定义如下:

其中,符号表达式SExp由逻辑表达式RelExp通过关系操作构成;RelExp由数学表达式Exp通过逻辑操作构成;Exp由项Term通过加减运算组成;Term由多个因子Power通过乘除运算组成;每个Power由1个或多个原子Factor通过幂运算组成;原子Factor是符号表达式的最基本元素,它可以是一个数值常量Constant、符号变量Symbol或者符号表达式,其中,每个Symbol均对应着一个可寻址表达式.

对于取值区间,采用区间抽象域[13]的方法,每个Symbol的取值用区间表示.区间分为数值型区间与指针型区间两大类,其中,指针型区间PointerDomain是指向集合PointTos标识所指向的区域,PointTos的元素即为区域的编号.RSTVL的区间及其上的操作构成完备格áL,≤,ò,ó,^,"∇,其中,^为空集,数值型区间的"为[-∞,+∞],指针型区间的"为空地址、野地址与所有可操作区域编号的并,ò为集合的并运算,ó为集合的交运算.虽然区间抽象域是非关系型的,但通过符号表达式可实现逻辑关联描述.基于RSTVL的静态分析可被映射为在格上的操作.

RSTVL可描述可寻址表达式间的3种关联,可满足流敏感、域敏感、路径不敏感的静态分析.因为路径不敏感,导致一个可寻址表达式可能对应多个区域.

RSTVL将内存划分为离散的区域,能够描述区域间的指向关系、层次关系以及取值的逻辑关联.基于RSTVL的区域抽象包括:

(1) 对每个程序点l,Rl表示在l处能够被访问的区域集合,Sls,domain∇表示在l处使用的符号集合.

(2) 对每个程序点l,有一个抽象存储:其中,

Rl,映射一个内存对象到一个区域;

⇀Rl,表示区域间的指向关系;

Rl,映射一个复合类型变量的成员到一个区域;

(3) RSTVL描述的抽象存储的信息间关联可表示为一个四元组ssr,ss,sf,sd∇,其中,

sr:V⇀R,表示可寻址表达式与区域的关系,是一个多对多的关联,一个可寻址表达式可能对应多个区域,一个区域也可能描述多个可寻址表达式的抽象存储;

ss:RSExp,表示区域与符号表达式映射;

sf:SExp⇀S,表示符号表达式与符号的关系,是一个多对多的关联,一个符号表达式由若干个符号通过逻辑运算及数学运算构成;

sd:SD,表示符号与区间的映射,每个符号都有一个区间.

对可寻址表达式的各种操作,都首先需要获得所对应的区域.定义Rl§e¨表示在程序点l上,抽象存储rl中, 可寻址表达式e对应的区域集合.下面给出获得各种类型的可寻址表达式对应的区域的策略:

下面给出关于RSTVL的其他相关操作:

Cl§v¨:在程序点l上,为内存对象v生成一个区域r.若v为标量类型,为v生成一个符号s,并根据v的数据类型为s指定一个初始区间(若v是基本类型,初始区间设置为[-∞,+∞];若v是指针类型,指向集合为{wild}),v的区域r的符号表达式sexp即由单一符号s构成;若v为结构体或数组的成员,父变量是fv,建立fv的区域与r的层次关系.

:在程序点l上,获得区域r的符号化表达式.每个PrimitiveRegionPointerRegion类型的区域均有唯一的符号化表达式.

:在程序点l上,获得可寻址表达式e的符号化表达式,(||表示或操作).

:在程序点l上,获得符号s的取值区间;

:在程序点l上,获得符号化表达式sExp的取值区间.根据sExp中每个符号的取值进行区间运算[13]得到.

:在程序点l上,获得标量类型的可寻址表达式e的取值区间.

:在程序点l上,获得编号为name的区域.

:获得符号表达式sExp中出现的所有符号.

:获得区域r对应的内存对象表达式.

:获得符号s对应的可寻址表达式.

:获得区域r的编号.

2 过程内分析

本文的过程内分析采用经典的数据流迭代算法[12],基于控制流图进行流敏感的分析,对复合数据类型变量进行域敏感的分析.对控制流图上的每个节点n,定义两个程序点:gn表示n前的程序点,ng表示n后的程序点.数据流计算方程如下:

其中,n为控制流图当前节点,pn的前驱节点.公式(1)中in(n)为计算的n的汇入信息,也就是程序点gn的抽象存储R·ninit表示对函数入口处的全局变量与参数进行初始化操作.公式(2)中out(n)为计算的n的出口信息,也就是程序点ng的抽象存储;gen(n)表示n中新产生的数据流信息;kill(n)表示n中注销或被改变的数据流信息;pred(n)表示n的所有前驱节点集合.

相对于流不敏感分析,本文采用的流敏感分析能够实现强更新操作,kill(n)能够计算出更多的数据流信息.相对于域不敏感的分析,本文采用的域敏感分析将会更准确地计算复合类型变量及其成员的数据流信息,本文的RSTVL也能更全面地描述抽象存储,这都将保证本文的分析所获得的每个程序点上的抽象存储更接近真实运行时的内存状态.因为本文对变量的取值通过区间抽象域进行抽象表示,满足在格上的操作.例如,在进行循环处理时,可采用加宽/收窄算子,通过迭代快速地达到不动点.

2.1 赋值语句的迁移操作

程序语句中最核心的语句是赋值语句,C程序中有各种类型的赋值语句,包括拷贝赋值(x=y)、加载赋值(x=*y,x=y.f,x=yf)、存储赋值(*x=y,x.d=y,xd=y)、取地址赋值(x=&y)等各种基本赋值操作以及更加复杂的赋值操作.本文将赋值操作统一表示为el=er,并在一个统一的分析框架进行分析.如果er是&e、数组arr、指针算术p+i,其对应的区域分别表示为:

C语言通过malloc,free进行动态内存分配与释放的操作.对malloc分配内存的赋值语句:

其中,v是临时变量,类型为指针el所指向的类型.当在程序点l上对动态分配的内存通过free进行释放时,假设描述该动态内存的区域编号mx,从Rl获得取值区间的指向集合PointTos包含mxPointerRegion,将mx除去;如果指向集合PointTos不包括wild,则添加wild,标识相应的指针指向一个野地址.

因为任何一个表达式都规定了对一个值的计算,每个表达式也都具有一种数据类型.如果一个表达式是指针、数组或结构体,则该表达式肯定为可寻址表达式,可在所在的程序点上基于RSTVL获得该表达式对应的区域.如果一个基本类型的表达式不是可寻址表达式,则本文直接用符号表达式表示该表达式的值.

假定赋值操作语句el=er对应着控制流图的节点n,分析时首先需要确定在程序点gnel对应的区域数目.如果Rn§el¨是一个单例集,且为一个可操作的区域r,则对区域r进行强更新操作.如果Rn§el¨对应多个区域,则对每一个可操作的区域r进行弱更新操作.基于RSTVL的赋值语句的迁移操作如算法1所示.

算法1. 赋值语句的迁移操作.

作为被赋值的可寻址表达式,el不可能是数组.辅助函数combine(n,r1,r2),在控制流图节点n上,如果r1是为标量类型分配的区域,则将区域r1与区域r2的值进行合并,合并后的值赋给区域r1.如果r1是为复合类型分配的区域,则分解为标量类型再进行combine操作.

2.2 分支语句与合并语句的分析

如果条件判断语句节点为n,则进入n的其中一个出边e的条件约束通过符号集zs,domain∇描述,流向e的抽象存储表示为的运算规则如算法2所示.

算法2. 分支语句迁移操作.

汇聚节点的抽象存储为各个入边流入的抽象存储的并.如果程序点l1的抽象存储是程序点l2l3的并,合并操作如算法3所示.

算法3. 合并操作的迁移操作.

2.3 循环语句的分析

本文对循环语句的分析采用加宽/收窄算子理论[14, 15].对循环语句的抽象存储迭代求精,直到达到循环内外的抽象存储的不动点.该技术通过加宽算子使得迭代运算快速收敛,得到精确解的一个上界,通过收窄算子使得加宽后的结果尽量逼近精确解.基于RSTVL的加宽/收窄算子运算规则见表 1.

Table 1 Widening/narrowing operator’s rules 表 1 加宽/收窄算子运算规则

假定一个循环将被执行若干次,循环块的直接前驱节点为n1,包含循环条件的循环头节点为n2,循环语句块真分支内的第1个节点为n3,循环语句块真分支内的最后一个节点为n4.n1n4都是n2的前驱节点,每次迭代运算过程中通过的并是否发生变化来判断抽象存储是否稳定.应用加宽/收窄算子理论的循环语句分析如算法4所示:先执行一遍循环体,再迭代执行加宽操作(第4行~第7行),最后迭代执行收窄操作(第9行~第12行).

算法4. 循环语句的分析.

2.4 实例分析

考虑程序片断图 1(b),L5处通过malloc动态分配了一块内存,根据被赋值对象sp的数据类型,生成了一个类型为struct s2的临时变量m_mVar1,为其分配一个编号为“msm_8_4”的区域.指针sp对应的指针型区间的PointTos的值为“msm_8_4”,表明sp指向了m_mVar1.

处理语句L6前,data的区域的编号为“sm_2”.分析L6的赋值语句时,对右边的取地址操作,首先生成一个类型为struct s1*类型的临时指针m_mVar2,为其分配一个编号为“mpm_9_10”的区域,并设置其对应的指针型区间的PointTos为{“sm_2”}.对于被赋值表达式spp,首先分析得到指针sp对应的指针型区间的PointTos,PointTos为单例集,只有1个元素“msm_8_4”,即,m_mVar1的区域编号.因为采取“晚初始化”(lazy initialization)的处理方式,在L5处并未对m_mVar1的成员p生成一个临时变量,而L6的被赋值变量为m_mVar1.p,这种情况下,需要识别出可寻址表达式m_mVar1.p,并为其分配一个编号为“mpm_10_4”的区域.因为spp只对应1个区域,对其进行强更新操作,即,将编号是“mpm_10_4”的区域的符号化表达式,更新为编号是“mpm_9_10”的区域的符号化表达式.

对于循环语句L8,经过加宽/收窄的处理,循环体内j的取值区间为[0, 5],数组a的所有成员的取值区间都被更新为[0, 5],该区间是实际取值区间的上近似.处理语句L10时,因为本文采取的是路径不敏感的分析,i的取值区间为[0, 1],a[i]对应的区域可能是a[0]的区域,也可能是a[1]的区域,需要执行弱更新操作.即,a[0],a[1]的值为其原来值与data.d的值的并,均为[-10, -10]È[0, 5].

3 过程间分析

函数调用对调用点上下文抽象存储的影响可分为3种:(1) 函数副作用,函数调用对全局变量与指针类型参数抽象存储的更改;(2) 函数返回值;(3) 控制流中断.

同一函数在不同的调用点被调用,上下文环境不同,将导致函数返回结果及对上下文环境的影响不同.为适应不同上下文环境的函数调用,本文的过程间分析采用基于符号化函数摘要的方法[16, 17],实现在不同上下文环境下对同一函数调用得到不同结果,达到上下文敏感分析.本文的符号化函数摘要的创建以及实例化将充分利用RSTVL的优点,主要关注函数副作用与返回值对调用点抽象存储的影响.

本文的符号化函数摘要的基本思想是:首先,对全局变量与形参进行初始化;然后,根据过程内分析的结果,计算返回语句的符号表达式;最后,将函数退出节点的各个前驱节点的全局变量及形参的抽象存储信息添加到函数摘要中.符号化的函数摘要存放于一个全局环境中,在每个函数调用点,取出被调用函数的符号化函数摘要,并根据调用点处的上下文信息对符号化函数摘要进行实例化,实现对调用点处的抽象存储更新.

3.1 符号化函数摘要生成

同一函数在不同的上下文环境下被调用,指针类型的实参与全局变量的指向信息可能不同.在对被调函数分析时,为了能使不同调用点的指针指向信息方便地映射到被调函数上,引入扩充变量[18]来抽象地表示指针类型的形参和全局指针表达式的指向信息.扩充变量的引入规则为:(1) 对于n级指针p,扩充出*p,**p,***p,…共n个变量;(2) 对于结构体s,如果对应的结构体类型有f1,f2,…,fnn个成员,则扩充出s.f1,s.f2,…,s.fnn个变量.例如,对程序片断图 1(c)函数f3的形参ps,ps为一级指针,引入扩充变量*ps,*psstr类型可寻址表达式,再扩充出变量(*ps).a.对一个函数基于控制流图进行分析时,首先获得该函数的参数,基于定义-使用链获得该函数使用的全局变量,对指针类型的参数与全局变量引入扩充变量,对参数、该函数内使用的全局变量及生成的扩充变量,均创建一个区域.

定义7. 基于RSTVL的符号化函数摘要SPSRSTVL(symbolic procedure summary using RSTVL),应用RSTVL描述一个函数的行为,共包括4类信息:

对参数与全局变量及它们的扩充变量初始化之后,便进行过程内分析.根据过程内分析的结果,计算返回语句的符号表达式,并将函数退出节点的各个前驱节点的全局变量及形参的符号化表达式添加到函数摘要中.生成的函数摘要将作为函数的一个属性.算法5是生成函数摘要的算法.

算法5. 函数摘要生成算法.

3.2 符号化函数摘要实例化

在函数调用点:首先,获得被调用函数的函数摘要;其次,基于形参与实参及其父变量的关系,获得每个形参对应的实参可寻址表达式集合;然后,将函数摘要中指针类型的区间进行实例化,将PointTos的区域编号映射为调用点处的区域编号;再将符号化表达式中的符号用调用点处的符号替代;对于被函数副作用影响的全局变量与实参,基于实例化后的符号表达式对其进行过程内的赋值语句分析;最后,基于实例化后的符号计算出函数返回值.

假定函数p在其控制流图节点n调用函数q,即函数摘要的实例化操作如算法6所示.其中,

mappingToArguments(var):获得形参var与其对应的实参集合;

initializingPointerDomain(d):将指针型区间dPointTos的区域编号实例化为调用点处对应的区域 编号;

fVarAVarsSet(fVarAVarsSet,varp):从描述形参与实参对应关系的fVarAVarsSet中获得varp对应的实参 集合.

算法6. 函数摘要实例化算法.

3.3 实例分析

考虑程序片断图 1(c),函数f3的函数摘要中:

对于函数调用形参ps,(*ps).a,p,*p,**p分别对应着实参集合{annoyPtr0},{s.a},{annoyPtr1}, {x0},{x}.annoyPtr0为生成的临时指针变量,指向s;annoyPtr1为生成的临时指针变量,指向x0.SymbolDomainSet中的“upm_4”,“ubm_5”被实例化为“bm_2”,“bm_1”,其中,“bm_2”是为x0分配的区域编号,“bm_1”是为x分配的区域编号.而(*ps).a_1是为(*ps).a生成的符号,(*ps).a只对应着s.a,则s.a对应的指针型区间的PointTos被更新为{“bm_1”},表明经过函数调用的副作用,s.a指向了x.对于SRetSet中的**p_5是为**p生成的符号,**p只对应着x,而x取值为常量1,则符号表达式2+**p_5被实例化为3,即,函数返回值为[3, 3].

4 实验结果及其分析

基于RSTVL的静态分析方法已经在缺陷检测工具DTSC中实现,DTSC的执行步骤包括:抽象语法树生成、符号识别、全局调用函数分析、生成控制流图、生成定义-使用链、数据流分析、缺陷检测.为了验证本文方法的效果,本文选取了5个C开源工程进行分析,并与STVL方法进行了对比.实验采用的硬件环境为:双核1.33G U5600处理器,3GB物理内存,Windows XP操作系统.

4.1 可寻址表达式间关联

通过本文方法识别出5个C工程的可寻址表达式及分析出的关联关系,见表 2.从表 2可以看出:将近50%的可寻址表达式存在层次关系,将近40%的可寻址表达式存在指向关系,将近10%的可寻址表达式间具有取值的逻辑关联关系.在进行静态分析时对这些关联关系考虑得不全面,势必导致分析精度的下降.

Table 2 Association of addressable expressions 表 2 可寻址表达式间关联统计
4.2 效率分析

为了验证分析方法的效率,通过实验与基于STVL的静态分析方法[7, 17]的DTSC进行对比.因为RSTVL比STVL能够描述更多的关联信息,在分析时将不可避免地导致分析效率的下降.为此,本文选取了5个C开源工程进行分析,比较两种分析方法在进行数据流分析时分析时间的差异.分析效率结果对比见表 3.

Table 3Efficiency comparision of two strategies 表 3 两种策略的效率对比

表 3可见:STVL方法的分析效率是30行代码/秒;RSTVL方法的分析效率是23行代码/秒,即,万行代码大约需要7分钟.RSTVL方法比STVL方法的分析效率略有下降,主要有3个方面的原因:

(1) RSTVL采用的是四元组模型,比STVL增加了区域的概念,在对可寻址表达式进行分析时,映射到对应的区域上进行分析,增加了计算量.

(2) RSTVL方法对指针类型与复合类型的参数与外部变量生成了扩充变量,导致参与运算的变量比STVL方法增多.

(3) 实现了域敏感的过程间分析,在函数摘要生成与实例化时都考虑了域成员.其中,工程antiword-0.37只有30%的可寻址表达式是基本类型的内存对象,另70%的可寻址表达式是指针、复合类型或复合类型的成员,分析时需要考虑区域间的关联耗时较多,从而导致基于RSTVL的分析比基于STVL的分析时间增加了49%.

STVL方法与RSTVL方法对循环均采取了加宽/收窄的分析策略,为了分析得到不动点,循环体将会分析若干次.因此,当被分析的程序循环过多,特别是嵌套循环过多时,将会严重影响分析的效率.uucp-0.98工程的分析效率偏低,主要原因是个别文件具有复杂的循环,例如分析uucp\uuconf\hsinfo.c文件,STVL方法耗时968s,RSTVL方法耗时1342s.原因是_uuconf_ihdb_system_internal方法内有多个循环,特别是行号在111~356间的循环,而且该循环又嵌套多个循环,需要经过若干次迭代才能达到数据流的稳定,严重影响了分析效率.

因为本文的分析是以预编译后的中间文件为分析单元,数据流分析是以函数为分析单元的,分析时间与被分析程序的规模具有线性关系,所以本文的方法也适用于对大规模程序的分析.

4.3 空指针引用检测

将本文静态分析的结果应用于空指针引用缺陷的检测.对于一个指针p,当其在程序点l上被引用时,令p对应的PointTos为集合Listpt.如果Listpt只包括“null”一个元素,则判为肯定空指针引用;如果Listpt的元素均为安全区域的编号,则为安全指针引用;其他情况判为可疑指针引用.空指针引用包括肯定空指针引用与可疑指针引用.对部分库函数,人工生成了摘要;对于没有函数摘要的函数,采取保守的策略,其返回值为抽象域的最大区间.表 4为应用STVL方法与RSTVL方法检测空指针引用缺陷的结果,其中,缺陷检测点(inspection point,简称IP)为经人工确认得到的有效缺陷(BUG).

经过人工判定,RSTVL方法所检测出的BUG包括STVL方法所检测出的所有BUG.因为RSTVL考虑了复合类型变量的层次关系,且过程间分析时实现了域敏感的过程间分析,因此RSTVL方法与STVL方法相比能够检测出更多的对复合类型变量的成员引用的缺陷.图 2是RSTVL方法检测出的一个空指针引用,STVL方法漏报了该缺陷.被调函数usGetNextByte可能在530行为pInfoCurrentpBlockCurrent赋值为空,当函数usGetNextChar在595行调用usGetNextByte后,pReadinfopBlockCurrent受函数调用的副作用影响可能为空,这将导致在602行对pReadinfopBlockCurrent的引用可能是空指针引用.

Table 4 Detecting results of null pointer dereference defects 表 4 空指针引用检测结果

Fig. 2A null pointer dereference defect detected by our strategy图 2本文方法发现的空指针引用缺陷

表 4的检测结果中,RSTVL方法比STVL方法所报IP稍有增多,主要有3点原因:(1) 对于没有函数摘要的函数,RSTVL采取了保守的策略,默认其返回值为返回类型对应的最大格值;(2) 如果被调用函数没有函数摘要,对于所传递的指针类型实参,如果不是安全指针则判断为空指针引用;(3) 对于过程间引用的指针,因为没有考虑路径条件,导致对一些复合类型变量的指针类型成员的引用被误报为空指针引用,而STVL方法不对此类指针的引用进行检测.

图 3是RSTVL方法产生的一个空指针引用误报.对于uucp\uuconf\strip.c第44行被引用的指针qglobalqprocess,通过分析实际是对扩充变量(*pglobal).qprocess的引用,因此,将(*pglobal).qprocess不能为空作为函数uuconf_strip的前置约束.而对于uucp\uuchk.c的函数调用根据被调函数uuconf_strip 的前置约束,需要判断puuconfqprocess是否为空.而puuconfpuuconfqprocess是通过函数调用的副作用被赋值的,如果puuconfqprocess为空指针,将导致uucp\uuchk.c第146行的条件iret!=UUCONF_SUCCESS成立,程序将终止,这样将保证在uucp\uuchk.c第146行传递给uuconf_strippuuconfqprocess不为空,不会产生空指针.而RSTVL方法未考虑puuconfqprocessuuconf_init返回值的关系,导致误判了传递给uuconf_strippuuconfqprocess可能为空,产生了误报.STVL方法虽然未产生该误报,原因是其对qglobalqprocess既未进行检测也未建立为前置约束.

Fig. 3A null pointer dereference false positive caused by our strategy图 3本文方法产生的空指针引用误报
5 相关工作

基于不同的静态分析方法以及针对不同应用,已提出了若干种描述运行时内存状态的模型.最简单的是名-值对[19],未考虑内存单元间的任何关联.较直观的是数组模型,但难以表示内存单元间的层次关系.别名对集合、指向关系集合、二元决策图[20]能够表示别名关系,适用于指针分析.形态图与TVAL适用于形态分析,主要用于判断程序运行时内存中数据结构的“形态”信息.区域的概念应用于内存的管理[21, 22],在静态分析领域,基于区域的模型是用一个区域表示为一个内存对象分配的一块连续内存块[6, 23].文献[23]提出了基于区域的形态分析,将全局的堆空间分解为独立的地址集合,并应用于内存泄露的检测,但不支持数据流分析.文献[6]提出了基于区域的三元模型,未用抽象域描述内存中的值,未考虑取值的逻辑关联关系,且只适用于单路径的分析.在静态分析中,用抽象域的域元素近似地表示变量取值,抽象域分为关系型与非关系型、八边形抽象域[24]、多面体抽象域[25]等,本文采用了非关系型的区间抽象域,但通过符号表达式可表示变量间的逻辑关联关系.

为了提高静态分析的精度,通常采用敏感的分析方法,主要包括流敏感、域敏感、上下文敏感、路径敏感.流敏感的分析在每个程序点计算并保存程序状态.其中,Worklist算法作为最典型的迭代算法,是最典型的一种流敏感分析算法.为了提高分析的效率,有些研究针对指针分析提出了稀疏的流敏感分析[26, 27].对于C程序中存在的复合类型变量,域敏感能够保证分析的精度,域敏感分析可分为基于数值偏移[10]与基于符号偏移[4],基于数值偏移的方法因为能够描述连续内存,能够更准确地描述强制类型转换、指针算术,但分析的效率也会下降.上下文敏感的过程间分析主要采用函数摘要[16, 17]的方法,基于函数摘要的方法可以避免在每个调用点处重复分析该函数的行为,具有较高的分析效率.

大部分的函数摘要采用基于á输入,输出∇映射表[28],也有一些符号化函数摘要[16, 17],符号化的函数摘要在捕获信息时将具体的程序状态表示为符号化抽象取值,具有较高的分析效率.

6 结束语

本文可被看作以前工作[7, 13, 17]的进一步扩展,更深入、全面地研究了C程序的静态分析.一方面,在对内存对象存储的描述上,本文提出了RSTVL,通过抽象区域模拟实际分配的内存区域,能够更全面地表示运行时内存对象的存储信息,并可以描述内存对象间的指向关系、层次关系和取值逻辑关联信息;另一方面,在基于RSTVL的流敏感、域敏感和上下文敏感的分析时,因为能将对可寻址表达式的值修改反映到对抽象区域的状态修改,在分析的各个环节采取了保守的分析策略,这能保证分析结果是实际可能运行情况的上近似,进而保证了分析的可靠性.应用本文分析方法进行代码级别的缺陷检测,将会大大降低检测的漏报率.

因为本文方法是路径不敏感的,在提高分析效率的同时也降低了分析的精度,也导致了对空指针引用检测的可疑指针引用比例偏高.本文的下一步工作是考虑路径的约束条件,特别是生成函数摘要时考虑路径的约束信息,并将静态分析的结果应用于内存泄露、缓冲区溢出、非法计算等更多源代码级别的缺陷的检测.

参考文献
[1] Dong YK, Xing Y, Jin DH, Gong YZ. An approach to fully recognizing addressable expression. In: Proc. of the 13th Int’l Conf. on Quality Software. Washington: IEEE Computer Society, 2013.149-152 .
[2] Zhang J. Symbolic execution of program paths involving pointers and structure variables. In: Proc. of the 4th Int’l Conf. on Quality Software. Washington: IEEE Computer Society, 2004.87-92 .
[3] Mooly S, Thomas R, Reinhard W. Solving shape-analysis problems in languages with destructive updating. ACM Trans. on Programming Languages and Systems, 1998,20(1):1-50 .
[4] Lev-Ami T, Sagiv M. TVLA: A system for implementing static analyses. In: Proc. of the 7th Int’l Static Analysis Symp. LNCS 1824, Berlin: Springer-Verlag, 2000.280-301 .
[5] Robert P. Wilson, Monica S. Lam. Efficient context-sensitive pointer analysis for C programs. In: Proc. of the ACM SIGPLAN 1995 Conf. on Programming Language Design and Implementation. New York: ACM Press, 1995. 1-12 .
[6] Xu ZX, Kremenek T, Zhang J. A memory model for static analysis of C programs. In: Proc. of the Leveraging Applications of Formal Methods, Verification, and Validation. LNCS 6415, Berlin: Springer-Verlag, 2010.535-548 .
[7] Zhao YS, Wang YW, Gong YZ, Chen HH, Xiao Q, Yang ZH. STVL: Improve the precision of static defect detection with symbolic three-valued logic. In: Proc. of the 8th Asia-Pacific Software Engineering Conf. Washington: IEEE Computer Society, 2011.179-186 .
[8] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X. A static analyzer for large safety-critical software. In: Proc. of the ACM SIGPLAN 2003 Conf. on Programming Language Design and Implementation. San Diego: ACM Press, 2003.196-207 .
[9] Choi JD, Burke M, Carini P. Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects. In: Proc. of the 20th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. New York: ACM Press, 1993.232-245 .
[10] Miné A. Field-Sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Proc. of the 2006 ACM SIGPLAN/SIGBED Conf. on Language, Compilers, and Tool Support for Embedded Systems. New York: ACM Press, 2006.54-63 .
[11] Hampapuram H, Yang Y, Das M. Symbolic path simulation in path-sensitive dataflow analysis. In: Proc. of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering. New York: ACM Press, 2005.52-58 .
[12] Kam JB, Ullman JD. Global data flow analysis and iterative algorithms. Journal of the ACM, 1976,23(1):158-171 .
[13] Wang YW, Gong YZ, Xiao Q, Yang ZH. A method of variable range analysis based on abstract interpretation and its applications. Acta Electronica Sinica, 2011,39(2):296-303 (in Chinese with English abstract).
[14] Cousot P, Cousot R. Static determination of dynamic properties of programs. In: Proc. of the 2nd Int’l Symp. on Programming. 1976. 106-130. http://www.di.ens.fr/~cousot/COUSOTpapers/ISOP76.shtml
[15] Li MJ, Li ZJ, Chen HW. Program verification techniques based on the abstract interpretation theory. Ruan Jian Xue Bao/Journal of Software, 2008,19(1):17-26 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/19/17.htm
[16] Gulwani S, Tiwari A. Computing procedure summaries for interprocedural analysis. In: Proc. of the 16th European Conf. on Programming. LNCS 4421, Berlin: Springer-Verlag, 2007.253-267 .
[17] Zhao YS, Gong YZ, Liu L, Xiao Q, Yang ZH. Context-Sensitive interprocedural defect dection based on a unified symbolic procedure summary model. In: Proc. of the 11th Int’l Conf. on Quality Software. Barcelona: IEEE Computer Society, 2011.51-60 .
[18] Huang B, Zang BY, Wei JY, Zhu CQ. Context-Sensitive interprocedural pointer analysis. Chinese Journal of Computers, 2000, 23(5):477-485 (in Chinese with English abstract) .
[19] King JC. Symbolic execution and program testing. Communications of the ACM, 1976,19(7):385-394 .
[20] Berndl M, Lhoták O, Qian F, Hendren L, Umanee N. Points-To analysis using BDD. In: Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation. New York: ACM Press, 2003.103-114 .
[21] Berger ED, Zorn BG, McKinley KS. Reconsidering custom memory allocation. In: Proc. of the ACM SIGPLAN Conf. on Object Oriented Programming, Systems, Languages, and Applications. New York: ACM Press, 2002 .
[22] Lattner C, Adve V. Automatic pool allocation: Improving performance by controlling data structure layout in the heap. In: Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation.2005 .
[23] Hackett B, Rugina R. Region-Based shape analysis with tracked locations. In: Proc. of the 32nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. New York: ACM Press, 2005.310-323 .
[24] Mine A. The octagon abstract domain. Higher-Order and Symbolic Computation, 2001,19(1):31-100 .
[25] Clarisó R, Cortadella J. The octahedron abstract domain. In: Proc. of the ACM SIGPLAN Conf. on Int’l Static Analysis Symp. LNCS 1824, London: Springer-Verlag, 2004.312-327 .
[26] Hardekopf B, Lin C. Semi-Sparse flow-sensitive pointer analysis. In: Proc. of the 36th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. New York: ACM Press, 2009.226-238 .
[27] Oh H, Heo KH, Lee WC, Lee WS, Yi KK. Design and implementation of sparse global analyses for C-like languages. In: Proc. of the 33rd ACM SIGPLAN Conf. on Programming Language Design and Implementation. New York: ACM Press, 2012.229-238 .
[28] Sharir M, Pnueli A. Two approaches to interprocedural data flow analysis. In: Proc. of the Program Flow Analysis: Theory and Applications. Upper Saddle River: Prentice-Hall, 1981. 189-233.
[13] 王雅文,宫云战,肖庆,杨朝红.基于抽象解释的变量值范围分析及应用.电子学报,2011,39(2):296-303.
[15] 李梦君,李舟军,陈火旺.基于抽象解释理论的程序验证技术.软件学报,2008,19(1):17-26. http://www.jos.org.cn/1000-9825/19/17.htm
[18] 黄波,臧斌宇,韦俊银,朱传琪.上下文敏感的过程间指针分析.计算机学报,2000,23(5):477-485 .