C程序分析工具中程序切片的设计与实现

蒋 刚,李兆鹏

1(中国科学技术大学 计算机科学与技术学院,合肥 230026) 2(中国科学技术大学 先进技术研究院 中国科大—国创高可信软件工程中心,合肥 230027)

1 引 言

随着当今计算机技术的飞速发展,在航空航天、医疗等安全攸关领域高可信软件的需求与日俱增,提高软件的可靠性和安全性是软件开发中所追求的目标之一,目前确保软件安全质量的方法有程序验证,动态测试和静态分析.程序验证作为保证程序正确性的严格手段,通过形式化方法如霍尔逻辑[1]、分离逻辑[2]等对程序中的各种性质给出严格的数学证明,从而保证程序的高可靠性,程序验证目前还未实现完全的自动化证明,需要大量的人工辅助证明,因此未能在工业界得到广泛应用.程序动态测试在实践中具有广泛的应用,它提供了程序运行时的检查,但是其精确性和覆盖率依赖于给定的测试集,缺少良好的测试集,将导致高漏报率和低覆盖率,而且运行时的检查成本和风险相对较高.静态分析技术不需要运行程序,是对代码进行分析,与形式化验证相比,静态分析能自动分析程序中的相关信息,与动态测试相比,静态分析可以以较低的成本更早地发现程序中的缺陷.

目前较为成熟的静态分析技术有模型检测[3]、抽象解释[4]、数据流分析[5]和符号执行[6].其中符号执行被广泛用于测试例的自动生成[7],它的主要思想是对代码中变量的取值进行符号化,使用一定的执行策略,以带约束的符号值代替程序变量运行时的具体值,较为精确地模拟程序的执行过程,从而达到分析的高覆盖率,得到较精确的分析结果.符号执行技术对路径敏感,模拟执行程序时会尝试所有可能的路径,因此比动态测试的覆盖率高.另一方面,符号执行随着程序中控制结构的增加,所需执行的状态数目呈指数级增长,会带来路径爆炸问题,这严重制约了使用符号执行技术的分析工具的可伸缩性.

随着软件的规模越来越大,要使符号执行技术依然保持低漏报率、低误报率并且具有良好的性能和可伸缩性成为一大挑战.目前笔者所在的课题组已实现一个基于开源编译框架LLVM[8]的符号执行分析工具ShapeChecker[9],它的总体框架如图1所示.

ShapeChecker是一个C程序静态分析工具,首先源代码经由Clang编译器翻译成LLVM的中间表示(Intermediate Representation,简称IR),ShapeChecker符号执行引擎通过解析IR字节码来分析程序,分析完毕后生成bug报告.

图1 ShapeChecker的总体框架Fig.1 Framework of ShapeChecker

由于分析工具中的执行引擎采用的是符号执行的方法,在分析大规模程序时,会降低工具的运行效率.针对工具中符号执行技术的不足,可采用程序切片的方法来提高工具的时间性能,即根据用户的兴趣点来专门检测某一类或几类缺陷,与关心的缺陷无关的代码可被切除不分析,这样在一定程度上缓解了状态爆炸问题.

本文的组织结构如下:第2节介绍切片准则生成模块,根据各类缺陷分析IR生成切片准则;第3节介绍切片模块,分析IR得到程序依赖图,再根据切片准则进行切片,得到切片后的程序,最后将切片后的程序交给符号执行引擎分析;第4节介绍程序切片的实验结果;第5节是相关工作和总结.

2 生成切片准则

切片准则生成模块的输入是LLVM IR,根据用户指定的缺陷分析IR产生切片准则,下面简要介绍LLVM IR的核心语法,如图2所示.编译过程中的每个翻译单元对应IR的一个模块(module),包含函数声明、函数定义和全局变量.

LLVM IR以函数为单位,每个函数包含若干基本块b,每个基本块包含若干条指令c,指令有函数调用指令,栈变量分配指令,算术运算指令,load与store指令,getelementptr指令等.其中getelementptr指令用于获取聚合数据类型中子元素的地址,如获取数组元素或结构体成员.

本系统共设计了针对八类缺陷的切片准则,分别是内存泄漏、文件描述符未释放、除零、整数溢出、悬空指针或空指针解引用、缓冲区溢出、使用未初始化的变量、返回栈变量的地址,下面是由各类缺陷生成切片准则的设计.

图2 LLVM IR的核心语法
Fig.2 Core grammar of LLVM IR

1)内存泄漏:检测指令是否是malloc,realloc,calloc或free四种函数调用指令中的一种,如果是则将该条指令加入切片准则.

2)文件描述符未释放:检测指令是否是fopen,freopen,fclose,open,openat,creat,close函数调用指令中的一种,如果是则将该条指令加入切片准则.

3)除零:检测指令是否是无符号除法,有符号除法,浮点数除法,无符号取模,有符号取模,浮点数取模运算中的一种,如果是则将指令加入切片准则.

4)整数溢出:将截断指令,加减乘除指令,取余指令,求绝对值的函数调用指令加入切片准则,之所以加绝对值函数是为了检测求最大负数的绝对值导致溢出的缺陷.

5)悬空指针或空指针解引用:在C语言上表现为对指针解引用和对数组作下标访问操作,它们分别有取值和赋值两种操作.比如对指针解引用的取值操作是*p,它的LLVM IR是

%1 = load i32*,i32** %p,align 8

%2 = load i32,i32* %1,align 4

检测load指令的操作数是否来自上一条load指令,是则将其加入切片准则,此例中第二条load指令的操作数%1来自上一条load指令,故将第二条load指令加入切片准则;对数组取元素的取值操作,比如p[0],它的IR是

%0 = load i32*,i32** %p,align 8

%arrayidx = getelementptr inbounds i32,i32* %0,i64 0

%1 = load i32,i32* %arrayidx,align 4

检测load指令的操作数是否来自getelementptr指令,满足则加入切片准则;同理,赋值操作如*p = 2,它的IR是

%1 = load i32*,i32** %p,align 8

store i32 2,i32* %1,align 4

检测store指令的操作数是否来自load,满足则加入切片准则;对数组元素赋值,如p[0] = 2的IR是

%0 = load i32*,i32** %p,align 8

%arrayidx = getelementptr inbounds i32,i32* %0,i64 0

store i32 2,i32* %arrayidx,align 4

检测store指令的操作数是否来自getelementptr指令,是则加入切片准则.

6)缓冲区溢出:缓冲区溢出的缺陷在C上表现为数组解引用,如arr[1],它的IR是

%arrayidx3 = getelementptr inbounds [3 x i32],[3 x i32]* %arr,i64 0,i64 1

%2 = load i32,i32* %arrayidx3,align 4

检测load指令的操作数是否来自getelementptr指令,是则加入切片准则;同理,arr[1] = 0这样的对数组元素赋值则检测store指令是否来自getelementptr指令;最后,对C库函数中与操作缓冲区相关的函数调用也加入切片准则,有memset、memcpy、memmove、strcpy、strncpy、strcat、strncat、wmemset、wmemcpy、wmemmove、wcscpy、wcsncpy、wcscat和wcsncat.

7)使用未初始化的变量:第一种情况是使用未初始化变量的值本身,如int a;printf(“%d ”,a);它的IR是

%a = alloca i32,align 4

%0 = load i32,i32* %a,align 4

%call = call i32(i8*,...)@printf(i8* getelementptr inbounds([4 x i8],[4 x i8]* @.str,i32 0,i32 0),i32 %0)

如果load指令的操作数来自alloca,则将load指令加入切片准则;第二种情况是将未初始化的变量的地址赋给指针,如int a;int *p = &a;它的IR是

%a = alloca i32,align 4

%p = alloca i32*,align 8

store i32* %a,i32** %p,align 8

因此若store指令的值操作数来自alloca,则将store指令加入切片准则.

8)返回栈变量的地址:这类缺陷分三种情况.第一种是将栈变量的地址赋值给指针类型的全局变量;第二种情况是将栈变量的地址赋值给二级指针的形参指向的区域,可通过形参传回主调函数,这两种情况都是将栈变量的地址赋给某变量,如store i32* %a,i32** %p,align 8,检测store指令的值操作数的类型是否是指针,是则将store指令加入切片准则;第三种情况是在被调函数中返回指针或变量的地址,如ret i32* %p,所以检测return指令的类型是否是指针,是则将它加入切片准则.

以上缺陷模式的检测均是作保守分析,只要指令符合缺陷的特征,就将它加入切片准则,这样保证了分析过程中与所关注的缺陷相关的程序语义的完备性.用户可以指定多种缺陷,根据每一种缺陷获取相应的切片准则,最后合并再交给切片模块.

3 程序切片模块

程序切片模块根据切片准则,对LLVM IR做切片,由于C代码的结构与IR等价,为便于图示,下面的分析基于C代码.本模块分两步,先构建程序依赖图,然后根据程序切片准则在程序依赖图上标记节点,计算反向可达性,所有可达的语句即是程序切片.

3.1 构建程序依赖图

程序依赖图表示程序中各语句间的依赖关系,包括数据依赖和控制依赖,程序依赖图由数据依赖图和控制依赖图构成,依赖图中的每个节点是一条语句.

3.1.1 构建数据依赖图

定义1.数据依赖.语句p中定值的变量可能会在语句q中被使用,称语句q数据依赖于语句p.

如图3的示例程序所示,用户在循环后动态分配了i个字节的内存,后续程序未释放堆内存.

1 intmain(){2 void∗p；3 intsum=0；4 inti=1；5 while(i<11){6 sum=sum+i；7 i=i+1；8 }9 p=malloc(i)；10 printf(″%d ″，sum)；11 }

图3 示例程序
Fig.3 Sample program

第4条语句int i=1定义了变量i,在循环的判断语句while(i< 11)中使用了i,所以while(i< 11)这条语句数据依赖于int i=1.LLVM在IR级别上提供了变量的DEF-USE信息,可得到语句间的定值和使用的关系,由此构建出图3程序的数据依赖图,如图4所示,其中entry节点表示程序的入口,语句间的指向表示数据依赖.

图4 图3程序的数据依赖图Fig.4 Data dependence graph of program in Fig.3

3.1.2 构建控制依赖图

定义2.控制依赖.语句p的直接后继至少有两个,从其中一条路径出发可到达语句q,从另外的一条路径出发可能不会到达q,则称语句q控制依赖于语句p.

通俗地说,语句p能决定语句q能否被执行,如图3中的第6条语句sum = sum + i控制依赖于判断条件while(i< 11).一定会被执行的语句控制依赖于程序的入口点entry.图3示例程序的控制依赖图如图5所示,其中的虚线箭头表示语句间的控制依赖关系.

最后,将数据依赖图与控制依赖图合并,构成程序依赖图,图6是图3示例程序的程序依赖图.

3.2 计算反向可达性

假设用户关心内存泄漏的缺陷,由切片准则生成模块分析图3得到切片准则是malloc函数调用语句,如图7中的深灰色节点所示,以它为起始点,对程序依赖图反向遍历,所能到达的所有节点即为程序切片,如灰色节点所示.

图5 图3程序的控制依赖图Fig.5 Control dependence graph of program in Fig.3

图6 图3程序的程序依赖图Fig.6 Program dependence graph of program in Fig.3

图7 图3程序的反向可达性Fig.7 Inverse reachability of program in Fig.3

由此得到源程序中与内存泄漏缺陷相关的语句,图8是程序切片的源代码表示,它的规模较原有程序要小,最后将切片交给分析工具ShapeChecker检测.

1 intmain(){2 void∗p；3 inti=1；4 while(i<11){5 i=i+1；6 }7 p=malloc(i)；8 }

图8 图3程序的切片结果
Fig.8 Result of slicing program in Fig.3

4 实验结果

实验的硬件平台是Intel(R)Core(TM)i7-4790 CPU @ 3.60GHz 4核8线程,20G内存;操作系统是Ubuntu 16.04.1 LTS64位.被测程序采用美国国家安全局的Common Weakness Enumeration(CWE)公共测试集*The MITRE Corporation.Common Weakness Enumeration [EB/OL].http://cwe.mitre.org/data/definitions/1000.html, 2017.,选取其中八类缺陷目录,分别是内存泄漏(CWE401)、文件描述符未释放(CWE773、775)、除零(CWE369)、整数溢出(CWE190、191)、悬空指针或空指针解引用(CWE476、690)、缓冲区溢出(CWE121、122、124、126、127)、使用未初始化的变量(CWE457)、返回栈变量的地址(CWE562),用静态分析工具ShapeChecker检测缺陷,加程序切片功能前后的时间对比如表1所示,其中切片后的分析时间包括切片本身的耗时.

表1 程序切片前后的分析时间比较
Table 1 Analysis time of before and after slicing

分析时间(s)切片前切片后时间减少的百分比内存泄漏603．87253．0558．10%文件描述符泄漏71．0539．5444．35%除零625．27363．2741．90%整数溢出3565．41911．2346．40%空指针解引用432．54172．9560．02%缓冲区溢出17036．1212915．6824．19%用未初始化变量2622．662403．798．35%返回栈变量地址0．890．4153．93%

从测试结果来看,程序切片减少了分析工具的运行时间,平均减少了27.64%.CWE的每种测试目录专门针对某种缺陷,在用户指定检测相应缺陷时,程序切片可将无关的控制结构删除,减少了程序的规模和符号执行中的状态数目,在一定程度上提高了静态分析的性能.表2是加程序切片功能前后的平均漏报率和误报率.

表2 程序切片前后的精度比较
Table 2 Precision of before and after slicing

切片前切片后漏报率1．86%3．73%误报率15．75%18．77%

加程序切片之后,分析工具的漏报率和误报率有略微的上升,这是由于静态分析本身是不完备的,将切片后的程序交给符号执行引擎执行时可能会影响它的分析策略.程序切片剔除的是与所关心的缺陷无关的代码,不会改变与缺陷相关的程序语义,因此漏报率和误报率只是有略微上升,相比工具在时间性能上的提升,精度损失在可接受的范围之内.

5 相关工作和总结

程序切片的思想由Weiser[10]提出,最初用于调试程序[11],程序中某一条语句出错后,为了找到影响该语句的所有前面的语句,只关注出错部分,方便程序员的调试.这一思想也可用于程序分析领域,用户想专门检测某种缺陷,这种缺陷关联的语句即是兴趣点.

Swarup等[12]用一组自动生成的近似满足程序不变量的输入来检测软件缺陷,之后用动态后向切片技术逐步过滤输入集以提高分析精度.

Marek[13]等开发的Symbiotic静态分析工具将指令制导、程序切片和符号执行工具KLEE[7]组合起来,其中切片部分使用数据流方程迭代方式计算.

赵云山等[14]使用有限状态自动机描述的缺陷模式和路径条件来生成切片准则,并有选择地对控制流图中的汇合点进行缺陷状态合并以减少误报率及提高分析效率.

本文在LLVM中间语言上提出针对缺陷的程序切片方法,笔者所在的课题组目前仍在改进静态分析工具ShapeChecker,下一步是支持C++的分析,C++有继承、多态和异常等独有的特性,在LLVM中间语言级别上会生成新的指令,可以将程序切片扩展成对C++中异常安全、线程安全等缺陷的处理.程序切片技术也可用于逆向分析中,逆向分析关心软件的基本原理和算法,可通过切片技术去除GUI和输入输出等部分,这样减少了我们理解程序的负担.

[1] Hoare Charles Antony Richard.An axiomatic basis for computer programming [J].Communications of the ACM,1969,12(10):576-580.

[2] Reynolds John C.Separation logic:a logic for shared mutable data structures[C].Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science,IEEE,2002.

[3] Clarke Edmund,Allen Emerson.Design and synthesis of synchronization skeletons using branching time temporal logic[M].Workshop on Logic of Programs,Springer Berlin Heidelberg,1981.

[4] Cousot Patrick,RadhiaCousot.Abstract interpretation:a unified lattice model for static analysis of programs by construction or approximation of fixpoints [C].Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,ACM,1977.

[5] Kildall Gary.A unified approach to global program optimization[C].Proceedings of the 1st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,ACM,1973.

[6] King James C.Symbolic execution and program testing [J].Communications of the ACM,1976,19(7):385-394.

[7] Cristian Cadar,Daniel Dunbar,Dawson Engler.KLEE:unassisted and automatic generation of high-coverage tests for complex systems programs[C].Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation,2008:209-224.

[8] Lattner Chris,VikramAdve.LLVM:a compilation framework for lifelong program analysis & transformation [C].Proceedings of the International Symposium on Code Generation and Optimization:Feedback-directed and Runtime Optimization,IEEE Computer Society,2004.

[9] Liang Jia-biao,Li Zhao-peng,Zhu Ling,et al.Symbolic execution engine with shape analysis [J].Computer Science,2016,43(3):193-198.

[10] Weiser Mark.Program slicing [C].Proceedings of the 5th International Conference on Software Engineering,IEEE Press,1981:439-449.

[11] Weiser Mark.Programmers use slices when debugging [J].Communications of the ACM,1982,25(7):446-452.

[12] Swarup Kumar Sahoo,John Criswell,Chase Geigle,et al.Using likely invariants for automated software fault localization[J].ACM SIGARCH Computer Architecture News,2013,41(1):139-152.

[13] Marek Chalupa,Martin Joná?,Jiri Slaby,et al.Symbiotic 3:new slicer and error-witness generation[R].International Conference on Tools and Algorithms for the Construction and Analysis of Systems,Springer Berlin Heidelberg,2016.

[14] Zhao Yun-shan,Gong Yun-zhan,Liu Li,et al.Improving the efficiency and accuracy of path-sensitive defect detecting [J].Chinese Journal of Computers,2011,34(6):1100-1113.

附中文参考文献：

[9] 梁家彪,李兆鹏,朱 玲,等.支持形状分析的符号执行引擎的设计与实现 [J].计算机科学,2016,43(3):193-198.

[14] 赵云山,宫云战,刘 莉,等.提高路径敏感缺陷检测方法的效率及精度研究 [J].计算机学报,2011,34(6):1100-1113.