静态程序分析方法和工具

高婉玲，赵鹤

（四川大学计算机学院，成都 610065）

静态程序分析方法和工具

高婉玲，赵鹤

（四川大学计算机学院，成都 610065）

综述静态程序分析的方法和工具。采用系统化文献评价方法和文献计量分析方法，通过论文的收集、筛选、内容提取等过程，对大量论文的信息进行总结分析。通过文献管理工具Endnote、数据分析软件SPSS和文献分析工具RefViz，统计分析论文数据库的基本信息，包括年代分布、作者分布、关键词和热点分析。通过阅读大量相关论文，静态程序分析方法可分为模型检测、符号执行、定理证明、抽象解释等。静态程序分析工具包括形式化验证工具、模型检测工具等。最后，总结静态分析方法和工具的不足。

程序分析；静态分析方法；静态分析工具；系统化文献评价

0 引言

（1）研究背景

程序分析是计算机科学与技术领域的经典和核心内容，主要是对某种语言编写的程序的内部流程进行分析[1]。根据程序是否需要运行，分为静态程序分析与动态程序分析。静态程序分析（Static Program Analysis）是在不运行代码的条件下，通过某些分析技术扫描程序，验证程序是否满足某些性质。动态程序分析（Dynamic Program Analysis）是在真实环境或模拟环境中执行程序进行分析。静态分析方法和工具对提高软件的质量非常有帮助，所以得到越来越多的重视。本文对近10年来静态程序分析领域的研究现状进行了总结，综述了部分静态程序分析的方法和工具，总结了静态程序分析的不足，可为研究领域的学者提供综合性的参考。

静态分析和动态分析的过程[2]如图1。

（2）研究方法

采用系统性文献评价方法[3]，对有关静态程序分析的综述，其步骤如下：

①研究问题

问题1：静态程序分析的方法有哪些？

问题2：采用静态程序分析方法的工具有哪些？

问题3：静态程序分析中有哪些未解决的问题？

图1 静态分析和动态分析过程图

②搜索策略

以static software analysis、model checking、formal verification、static program analysis、静态程序分析及其组合为关键词，在数据库、会议论文集中进行检索，年限为2004年至2016年。共搜集篇数1604篇，其中394篇用于文献计量分析，最终采用17篇用于文献综述。

③筛选方案

长文优于短文；博士学位论文；EI或SCI期刊；国内和国外国际会议论文。

④数据提取和分析对于检索到的有关静态程序分析的论文，根据需要解决的问题对论文进行分类和总结。

④完成报告

在完成上述工作的基础上，完成论文的编写。

1 文献计量分析结果

1.1 年代分布

图2 Endnote年代统计分布图

通过Endnote工具分析，文献的年代分布和趋势如图2。该领域直到2011年文献呈现递增趋势，大致可分为四个阶段：2007年之前为起步阶段，2007年-2011年为高速增长阶段，2011年-2013年下降趋势明显，2013年之后文章数量平稳上升。

1.2 作者分布

采用SPSS分析作者在该领域内发表论文数占总体篇数的频率（见图3），每种颜色代表一个作者，颜色的宽度表示了其发表的文章的频率，宽度越宽，则文章数量越多。

结论：近年来编写该领域相关文献的作者较多，但是产量都不是很大，高产作者较少。

图3 SPSS作者统计图

1.3 关键词和热点分析

RefViz工具中的Matrix视图（见图4）是关键词相似性排列后生成的图形，横、纵坐标轴上表示的关键词距离越近，表示关键词之间的相似度越高，坐标轴交汇点红色越深，代表含有横、纵坐标对应的关键词的文献越多。

图4 Matrix视图

结论：RefViz分析结果显示文献一级关键词为：software、analysis、technique、model、program、method等，它们是与文章关联性最强的关键词。RefViz揭示的文献的热点为：software、verfication、program、static等。

2 静态程序分析方法

2.1 形式化验证（Formal Verification）基本概念

形式化验证采用数学方法证明某些形式的规范或属性的正确性。模型检测、符号执行、定理证明、约束求解等多种程序分析方法都属于形式化验证技术。近年来形式化验证技术已经有了显著的提高和进步，但验证过程的低可预测性、缺乏显示验证进展的指标等因素，阻碍了形式化验证成为主流验证技术[4]。

2.2 模型检测（Model Checking）

模型检测是检测给定结构是否符合给定的逻辑公式的技术，是一种很重要的自动验证技术[5]。首先要对有限状态的系统构造状态机或有向图等模型，再通过遍历模型来验证系统的性质。模型检测成功应用于协议验证和硬件检测方面，由于软件自身的复杂度，软件模型检测只检测抽象模型[6-7]。

模型检测技术存在两大问题：建模和状态空间爆炸。由于抽象模型与实际系统存在差异，在验证模型的过程中找到的漏洞不一定与代码中真正的错误一致。解决建模问题，可以结合模型检测和软件测试各自的优势[5]。针对状态爆炸的问题，符号化模型检测（Symbolic Model Checking）和有界模型检测（Bounded Model Checking，BMC）可以有效缓解。将两者交叉存取的技术，可以在有限的存储空间和时间中，不需要存储全部可达状态，即可有效地探索状态空间[8]。

2.3 符号执行（Symbolic Execution）

符号执行中采用抽象符号代表变量的值来模拟程序的执行过程。优点是能够精确地模拟程序执行过程，缺点是不能处理指针对象及代码中的循环。符号执行与约束求解方法相结合，是一种精确的判定方法。约束条件的集合和求解的能力决定了约束求解工具分析和发现错误的效率。如果有足够的时间和空间资源，上述方法可以正确判定路径是否可行[9]。但如果需要枚举所有可能的路径，路径个数会随程序规模的增大呈指数级增长，出现状态爆炸的问题[6]。

2.4 定理证明（Theorem Proving）

定理证明是程序验证中经常用到的一种基于语义的分析方法[2，6]。它将验证的问题转换为数学问题,来分析程序的指定属性是否满足，所以它比很多分析方法复杂但更准确。定理证明适用于静态代码，缺点是程序员的工作增多，而且这种验证方法难以应用于大规模程序。目前此方向研究较热门的是基于逻辑推理自动证明程序的性质，但由于自动化的定理证明难度系数太大，所以还没有产品可供工业界使用。

2.5 抽象解释（Abstract Interpretation）

抽象解释由P.Cousot和R.Cousot提出，原理是采用可靠近似分析方法对数学模型进行分析，并为不同的近似分析方法创建统一的形式化框架。抽象解释本质上是在计算效率和精度之间取得均衡，通过不断迭代，抽象解释最终为程序建立抽象模型[2]，分析结果可能不够精确。抽象解释的思想和方法在各类编译器技术中得到广泛使用，它的应用范围不仅包括程序分析，还包括程序的调试、变换等。

2.6 其他程序分析技术

●类型推导（Type Inference）是自动推导变量和函数类型，适用于控制流无关的分析，可用于处理大规模程序，但是分析结果可能不够精确。

●实验程序分析方法（Experimental Program Analysis）[10]是执行目标程序过程中，在控制条件下，描述或解释对一个或多个程序的一个方面的独立变量的影响,是一种新形式的程序分析方法。

●静动态结合的混合分析技术结合了静态分析和动态分析的优点，可以提高分析结果的精度，同时降低了开销，提高了效率。主要包括两个步骤，第一步是将预处理后的程序与静态扫描字节码后的结果进行静态分析，第二步是对静态分析结果中不确定的部分进行动态分析，将动态分析和静态分析的结果结合，得到最终的分析结果[11]。

2.7 静态程序分析方法比较

模型检测、符号执行、定理证明等与形式化验证相关紧密，属于形式化验证方法。模型检测、定理证明的分析对象及处理方法不同：模型检测尽可能枚举所有状态，而定理证明是将问题转化为数学公式，采用逻辑规则推导证明。模型检测、类型推导是从不同的角度抽象程序：模型检测将程序抽象为模型，类型推导将程序抽象为变量或函数集合。符号执行、类型推导都依赖约束，但是形成约束的方法和约束的表现形式不同：类型推导的约束是一组集合关系表达式，符号执行的约束是一组以布尔表达式、线性等式和不等式。符号执行、约束求解共同的优点：对程序的执行可以进行精确的模拟。类型推导和抽象解释共同的缺点：分析结果都不够精确。定理证明是非常准确的，但是方法比较难，而且很难用于大规模程序。

3 静态程序分析工具

静态分析工具主要检查源代码中的变量、模块接口的一致性、逻辑上可能存在的错误结构和不可达的程序段等[12]。使用静态分析工具可以尽早发现程序错误，而且有助于发现编程人员的编码风格的问题。

3.1 形式化验证工具

●FindBugs工具，Java的著名现代工具，有警告提醒、错误检测的功能。在运行的过程中，将遍历并分析所有指定文件，最后将分析结果可视化。

●lint工具，在C程序中查找简单错误。lint和FindBugs的缺点是不能严格保证分析结果的正确性[13]。

●CODESONAR工具，是使用过程间分析方法来检查C或C++代码中模板错误的工具，检测范围包括缓冲区溢出、内存泄漏、冗余环路和分支条件。

●K7工具，来自KlocWork公司，可以处理由C、C++与Java组成的复合的应用程序，与CODESONAR工具有类似特点。

●Coverity prevent工具，是静态代码分析工具，被用来在开源项目中查找缺陷。它支持增式分析，可以识别死锁、空指针、未初始化变量、缓冲区溢出等问题。

●SVT(System Verification Test)，静态验证工具，模拟用户可能遇到的测试场景，以此分析可能的问题或错误，可以验证由UML类图和状态机图组成的UML模型。

●cprover工具，是一个插件，可以在C程序中进行可视化调试、错误跟踪，还具有后台验证功能。

3.2 模型检测工具

有界模型检测工具（BMC）的代表性工具是CBMC，支持C++、SpecC和SystemC语言，它主要检测C或SystemC中系统级的环路模型与Verilog提供的模板是否一致，并且可以检测C程序中断驱动程序中的数据竞争[13]。其他还有为特定属性量身定做的Saturn工具、专门捕获缺陷的EXE工具、Calysto模型检测器和可解决C程序函数指针问题的VARVEL工具。BMC是寻找浅层缺陷的最好技术，一旦发现缺陷，它会提供一个完整的反例路径，但是BMC只能分析简单的不包含深层循环的程序[7]；基于执行的工具有Verisoft、Java-PathFinder、CMC、MaceMC、Chess，许多基于执行的模型检测技术已经被结合在新版本的SPIN中[2,13]；抽象精化模型检测器的Yogi工具用于处理指针和程序，它验证有限状态机表示的无效程序的属性；SLAM主要针对C语言，不断的对抽象的程序模型进行细化和反复迭代，直至发现错误或超时；BLAST的思想与SLAM类似，BLAST可以集成到Eclipse开发环境中，可以提供一个典型的程序分析问题的断言检查；此外，还有其他模型检测工具：Java PathFinder、Modechart Toolset、CMC、PRISM、TReX、IOAToolset、MOCHA、PARAGON、SGM、Kronos、Hytech、UPPAAL、VERISOFT、HMC。

3.3 抽象解释工具

●The C Global Surveyor(CGS)，是一个针对航天任务软件开发的静态分析器，它用来分析在Mars Path-Finder Finder、Deep SpaceOne和Mars Exploration Rover中使用的软件。

●PAG，是一个程序分析器，可以分析与体系结构相关的特性，如最坏情况下的执行时间、高速缓存的性能、堆栈情况和管道的行为[13]。

●NPCA-WCET[14]，基于抽象解释的自动分析工具，主要面向高级语言和具有流水线和高速缓存的RISC处理器结构。利用静态分析方法得到程序最差情况执行时间的安全估值，再利用其词法分析和语法分析的功能获取程序的调用关系和语法结构，通过对源程序的插桩得到程序的结构及分支覆盖的情况。

●基于抽象解释分析的其他工具有Proverif和ASTREE，它们可用于大规模的硬件和软件系统的验证。

3.4 其他工具

●V-HOLT验证器，自动验证的基于高阶逻辑的定理证明工具，不需要用户手工操作[14]；

●codetest，可以对多种类型功能进行分析，包括对内存、性能、代码覆盖进行分析，也可对软件进行跟踪，可对数据的一致性提供保证[15]；

●JUTA，针对Java语言的自动化单元测试工具，将单个Java方法的源代码解析成控制流图，然后利用符号执行分析路径，可检测程序断言和特定类型的错误，并能够在可接受的时间内给出有效结果[16]；

●Tamiflex，是一个工具链，可以有效解决静态程序分析和java转换的部分问题[17]；

●Splint工具，用于检测程序风格和注释，适用于C语言，被成功用于Wu-ftp和Apache的检测中；

●PREfix采用符号执行与约束求解的方法对C/ C++程序进行静态分析。自动PAT采用了布尔逻辑可满足性算法与线性规划结合的方法，来判断路径的可满足性[9]；

●Checkstyle，是来自SourceForge的开源项目，促使开发人员遵循规范编写代码，用于检查程序的编码格式、约定的命名规则、类的设计等方面。

3.5 静态程序分析方法和工具的不足

相比动态分析，静态分析考虑执行路径更加全面，漏报率更低，可以更早的发现更多的缺陷，适用于状态有限、稳定性要求较高的软件。但是动态分析获取了程序在运行过程中的具体信息,所以发现某些性质（程序指针运算、动态存储分配等）缺陷可能更准确,误报率也较低。

静态分析的不足：

●静态分析方法的误报率很高，可能是不可达路径判断不准确或控制流与数据流聚合有问题等造成的；

●静态分析精度比动态分析低，受规模限制较大，分析面窄；

●静态分析工具一般比较庞大，对运行环境要求苛刻；

●静态分析工具采用的算法存在片面性，虽然自动化程度较高，但某些工具的结果仍需手工确认；

●静态分析工具只能检测出一部分缺陷，存在漏报。

4 未解决的问题和未来的工作

由于程序规模的增大，程序设计语言的复杂性成倍增长，而且证明程序正确与否是一个比较复杂的问题，很难达到高效率且易查错的效果，所以程序验证只应用在一部分关键模块，没有被广泛使用。另外在模型构造、路径选择方面需要开发更好的策略。

在未来的工作中，研究静态和动态结合的方向有比较高的热潮，静态分析与动态分析的分析精度、开销和适用的软件属性等方面差别很大，所以它们的结合可以平衡各自的缺点，发扬各自的优点。同时，在限制分析路径范围的条件下，将静态分析和动态测试结合也值得研究，在提高分析结果精度的同时，降低了开销，提高了效率。另外，高精度的程序分析技术、程序分析新理论和新方法的引入、基于统计挖掘的软件分析以及多核技术对软件分析技术发展的影响都是未来有潜力的研究方向。

[1]刘磊.程序分析方法[M].北京,机械工业出版社,2013.

[2]梅宏,王千祥,张路,王戟.软件分析技术进展[J].计算机学报.2009(09):1697-710.

[3]Pai M,McCulloch M,Gorman JD,Pai N,Enanoria W,Kennedy G,et al.Systematic Reviews and Meta-Analyses:an Illustrated,Stepby-Step Guide[J].The National medical journal of India.2004,17(2):86.

[4]Mitra RS,Editor Strategies for Mainstream Usage of Formal Verification.Design Automation Conference,2008 DAC 2008 45th ACM/ IEEE;2008 8-13 June 2008.

[5]Jianguo C,HangXia Z,Bruda SD,Editors.Combining Model Checking and Testing for Software Analysis.Computer Science and Software Engineering,2008 International Conference on;2008 12-14 Dec.2008.

[6]杨宇,张健.程序静态分析技术与工具[J].计算机科学，2004(02):171-4.

[7]Jhala R,Majumdar R.Software Model Checking[J].ACM Computing Surveys(CSUR)，2009,41(4):21.

[8]Ganai MK,Chao W,Weihong L,Editors.Efficient State Space Exploration:Interleaving Stateless and State-Based Model Checking. Computer-Aided Design(ICCAD),2010 IEEE/ACM International Conference on;2010 7-11 Nov.2010.

[9]张健.精确的程序静态分析[J].计算机学报,2008,09:1549-1553.

[10]Ruthruff JR,Elbaum S,Rothermel G,Editors.Experimental Program Analysis:a New Program Analysis Paradigm.Proceedings of the 2006 International Symposium on Software Testing and Analysis，2006:ACM.

[11]于利前,王林章,雷斌,赵建华,李宣东.静动态结合的Java程序不变性分析方法[J].计算机学报.2010(04):736-46.

[12]文昌辞,王昭顺.软件测试自动化静态分析研究[J].计算机工程与设计,2005,04:987-989.

[13]D'Silva V,Kroening D,Weissenbacher G.A Survey of Automated Techniques for Formal Software Verification[J].Computer-Aided Design of Integrated Circuits and Systems,IEEE Transactions on，2008,27(7):1165-78.

[14]姬孟洛,李军,王馨,齐治昌.一种基于抽象解释的WCET自动分析工具[J].计算机工程，2006,32(14):54-6.

[15]丁沂.软件分析技术与工具[J].无线互联科技，2012(04):52.

[16]严俊,郭涛,阮辉,玄跻峰.JUTA:一个Java自动化单元测试工具[J].计算机研究与发展，2010(10):1840-8.4

[17]Bodden E,Sewe A,Sinschek J,Oueslati H,Mezini M,Editors.Taming Reflection:Aiding Static Analysis in the Presence of Reflection and Custom Class Loaders.Software Engineering(ICSE),2011 33rd International Conference on，2011，21-28 May 2011.

作者简介：

高婉玲（1992-），女，河南新乡人，硕士研究生，研究方向为形式化验证、软件自动化测试

赵鹤（1992-），女，吉林长春人，硕士研究生，学生，研究方向为软件形式化验证和软件自动化测试

Static Program Analysis Methods and Tools

GAO Wan-ling，ZHAO He
（College of Computer Science,Sichuan University,Chengdu610065）

Reviews the static program analysis methods and tools.Uses systematic literature review method and bibliometric analysis method,to analyze and summarize the information in a large of papers by collecting,screening and extracting content of papers.Through Endnote,SPSS, and RefViz,the basic information in papers database is added up and analyzed,including age distribution,author distribution,keywords and hotspot analysis.By reading a large number of papers,static program analysis methods can be divided into model checking,symbolic execution,theorem proving,abstract interpretation,etc.Static program analysis tools include formal verification tools,model checking tools and so on.At last,summarizes the shortcomings of static analysis methods and tools.

Program Analysis;Static Analysis Method;Static Analysis Tool;Systematic Literature Review

1007-1423（2017）05-0038-05

10.3969/j.issn.1007-1423.2017.05.010

2016-12-01

2017-01-20