基于抽象解释的迹划分技术研究

张弛+丁泽文+刘林武

摘 要：确保程序中没有运行时错误，对于软件安全性的保证十分重要。基于抽象解释的静态分析方法对程序语义进行抽象，是验证运行时错误最合适的形式化方法之一。然而抽象解释对于程序语义的抽象可能导致过近似问题，从而引发误报，降低了分析精度。因此提出了迹划分的技术，根据程序的迹对程序控制流图进行划分，对静态分析过程进行局部细化，减少了抽象解释过程中过近似引发的误报。迹划分技术以局部分析效率降低为代价换来了分析精度的提高。

关键词：抽象解释；迹划分；静态分析；运行时错误；软件安全性

中图分类号：TP311 文献标志码：A

Research on Trace Partitioning Based on Abstract Interpretation

ZHANG Chi，DING Ze-wen，LIU Lin-wu

（College of Computer Science and Technology，Nanjing University of Aeronautics and Astronautics，Nanjing，Jiangsu 211106，China）

Abstract：Ensuring the absence of run-time errors in the program is important for the software safety.The program semantics was abstracted by the static analysis method based on abstract interpretation.It is the most appropriate formal method for validating run-time errors.However，the over-approximation of program semantics by the abstract interpretation may lead to false alarms，which reduce the accuracy of analysis.So the technology of trace partitioning was proposed.The control-flow-graph was partitioned according to the trace，and then the process of static analysis can be local refinement.The method reduced the false alarms caused by over-approximation.Trace partitioning obtains higher analytical accuracy at the cost of reduction of local analysis efficiency.

Key words：abstract interpretation；trace partitioning；static analysis；run-time error；software safety

1 引 言

近几年来，安全关键领域中，如何保证软件安全性已经成为了一个广受关注的重要课题，如何提高软件质量，保证系统安全性，防止灾害事故的发生，已经成为当前工业界和学术界的重要研究课题[1]。程序的运行时错误是一类特定的软件错误，是指程序在运行时或运行后发生的错误，并不是软件需求和设计阶段引入的问题，而是由于违反程序语言的安全性规范而引入的问题[2]，例如某条程序执行路径可能存在除数为零或者数据越界的情况。

对于运行时错误，工业界常用的仿真、模拟、测试等手段可以发现大部分错误，但却无法保证软件中没有运行时错误。形式化分析与验证方法是保障软件安全性和可靠性的一种重要方法[3]。目前常用的形式化静态分析方法有模型检测[4]、定理证明[5]和抽象解释[6]。模型检测需要穷举所有状态空间，存在状态空间爆炸的问题；定理证明需要大量人工参与，难以自动化。抽象解释对程序语义进行抽象，将程序的具体语义转化到抽象域中对程序的性质进行分析。其根据需求对程序语义进行近似，调节静态分析的精度和效率，是目前对运行时错误进行分析和验证十分有效的方法。

抽象解释方法通过将程序的具体执行过程转化到状态迁移系统，在抽象环境中分析状态的可达性，用以验证实际执行时是否满足某一性质。在以程序控制流图表示程序具体的执行过程时，该过程本身可能导致过近似问题，导致在验证某些程序性质时引发误报。例如，我们考虑图1中C程序片段。

可以看出来，在执行y=1/y这行代码之前，变量y的取值只可能是1或者-1，语句y=1/y这行语句不可能发生除零错误。然而在使用基于区间抽象域的抽象解释方法对于示例程序进行分析时，将变量的单个取值抽象成区间表示，分析结果为变量的取值范围。在执行第一行语句前，变量y的取值是[- SymboleB@ ，+ SymboleB@ ]，在執行左侧分支y=-1后再S4处y的取值是[-1，-1]，在执行右侧分支y=1后，根据区间抽象域的定义，在S4处y的取值是区间[-1，-1]和1，1的最小上界，即[-1，1]，即此时执行语句y=1/y可能发生除零错误，而这个错误在实际执行时是不可能发生的，属于误报。对于此类问题，即使使用更加复杂的抽象域，例如八边形抽象[7]和多面体抽象[8]，也无法解决这类问题。事实上，在S4处变量y的取值只可能是-1或者1，分别通过两条执行路径得到，，即S1-S2-S4-S5和S1-S3-S4-S5，都不会出现除零错误。如果按照如图2所示的细化后的控制流图进行分析，就不会发生除零错误。endprint

迹划分的方法最早被提出用于数据流分析（data-flow analysis）[9]，这里使用迹划分方法改进抽象解释的静态分析方法，根据反映程序具体执行过程的迹，对程序控制流图进行局部细化，以分析效率为代价，提高分析的精度，减少误报。

本文主要工作如下：

首先介绍了迹划分技术的理论框架，说明如何使用迹划分对程序控制流图进行划分；之后说明在具体的基于抽象解释的静态分析过程中，如何使用迹划分来提高分析进度，降低误报率。

2 迹划分的理论框架

本章主要介绍迹划分的理论框架，其用于对抽象解释的分析过程进行改进以调高分析精度。抽象解释是一种可以验证程序变量性质的形式化静态分析方法，有许多国内外相关文章[10-11]对抽象解释的基本概念进行介绍，本文不再赘述，下面主要介绍迹划分技术的相关概念[12]。

2.1 相关概念

定义1（程序）：我们定义一个程序P为一个迁移系统（S，→Sl），其中S是一个一个程序状态的集合，→是描述程序可能的基本执行步骤的迁移关系，Sl表示初始状态的集合。

定义2（迹trace）：迹是一个用于描述程序所有运行状态的非空的有限状态序列的集合S*。其中σ是其中一个有限状态序列，我们称σi是该序列的第i+1个状态，σ0和σ-1分别为该序列的第一个状态和最后一个状态。

因此基于迹的程序的形式化定义为[P]Δ{σεS*|σ0∈Sl∧i，σi→σi+1}，即程序可以定义为许多条迹的集合，每条迹反映程序的一条实际执行路径。

2.2 迹划分的形式化定义

在进行静态程序分析过程中，抽象解释方法通过将程序从具体域转化到抽象域中，极大的加快了分析过程的效率，与模型检测相比，大大缩减了状态空间的数目，避免了状态空间爆炸的问题。然而其对于具体执行环境的抽象可能导致过近似的问题，引发实际运行中不会出现的虚假反例。抽象解释中具体域与抽象域之间的转化通过一个Galois连接[13]来表示：

α（P，≤）（P*，≤*）γ

其中（P，≤）称为具体域，（P*，≤*）称为抽象域，α和γ分别称为抽象函数和具体化函数。

迹划分是一种将分析过程细化的方法，根据不同的迹将控制流图划分成更多状态，牺牲分析效率以换得分析精度的调高。迹划分的本质上是一种具体化的过程，可以通过一个具体化函数δ来实现，我们有如下形式化定义。

定义3（迹划分trace partition）：一个具体化函数δ：E→P（F）称为迁移系统F的划分，当且仅当∪x∈E（δ（x））=F并且x，y∈E，x≠yδx∩δy=。

也就是说，迹划分过程将一个迁移系统分成若干个子分区，各个分区的合集与原迁移系统等价，并且分区之间互不相交。迹划分可以保证抽象解释分析过程的可靠性（soundness），不会为分析过程带来额外的误报或者漏报。

2.3 程序控制流图的迹划分方法

程序控制流图（control-flow graph）[14]是程序的一种重要的表示形式，其反应了程序中语句之间的执行先后顺序和程序运行过程中的所有可能执行流向。抽象解释方法一般以控制流图为分析对象，在抽象环境中迭代计算不动点，以验证变量的数值性质。具体的，对于程序控制流图的迹划分主要有条件判断语句的迹划分、循环语句的迹划分、变量取值的迹划分三种情况，下面具体进行说明。

（1）条件判断语句的迹划分

对于条件判断语句，可以根据条件判断语句的分支数对程序控制流图进行划分，在抽象解释的静态分析过程中，由于部分结构的细化，导致分析效率的下降。具体的迹划分过程如图3所示。

（2）循环语句的迹划分

对于循环语句，可以根据循环体的执行次数对程序控制流图进行划分，每条迹分别代表程序循环体执行1次、2次…的执行路径。为了保证分析过程的可终止性，划分过程不能无限进行，根据实际情况设置循环划分上限n，将循环语句划分成n部分。具体的迹划分过程如图4所示。

（3）变量取值的迹划分

在抽象解释过程中，有些变量的取值是离散的几个点，例如变量x的值可能为-100和100，此时对其取值范围进行抽象表示的精度很差，此时x的区间抽象域表示为[-100，100]，有极大的可能导致虚假反例的产生。根据变量取值遍历迹，对程序控制流圖进行划分。具体的迹划分过程如图5所示。

为了保证迹划分方法所带来的时间和空间开销是局部的，需要在变量性质得到验证之后，对迹划分后的程序控制流图进行合并（merge）。否则，程序控制流图的迹划分会导致分析过程的复杂度据划分点的数目成几何倍数上升，此时付出的分析效率代价对于验证变量性质没有价值。对于控制流图的合并过程如图6所示，图6以条件判断语句为例，说明了如何对于划分的控制流图进行合并，其他类型迹划分就不在赘述。

3 迹划分技术的应用

上文提到了迹划分技术的理论框架，指出了迹划分可以对哪几类程序控制流图进行划分，从而将分析过程细化，以期可以减少抽象解释分析过程由于过近似产生的误报。当然的，我们可以在实际分析过程中遇到误报时，根据遇到的具体问题，手动对控制流图进行迹划分，在程序性质得到验证后，即找到真实错误或者排除了虚假反例，则可以对迹划分后的控制流图进行合并，继续进行静态分析，直至所有程序分析完毕。

然而对于静态分析而言，自动化分析能力的强弱十分重要，还是需要一些自动的策略来自动地进行控制流图的划分和合并，经过大量的实验，对以下三类程序片段进行迹划分时效果十分显著，可以加入自动的策略中，提高分析精度。

3.1 变量间存在线性关系的情况

很多情况下待变量的之间是存在线性关系的，而传统的非关系型抽象域却无法表达变量之间的关系，导致分析精度大大下降。若为了解决部分程序分析过程的误报而引入关系型抽象域，如八边形抽象域，全局的时间复杂度会由O（n）提高到O（n3），极大地降低了分析效率。此时可以使用迹划分技术对程序控制流图进行划分，只会在局部提高分析复杂度。endprint

如果發生存在线性关系变量发生算术运算，例如：如果整数x∈[-1，1]，那么根据区间抽象域的计算结果，则有x-x∈[-2，2]，可能发生误报，此时采用变量取值的迹划分，根据x=1和x=-1两条迹对程序控制流图进行划分，都有x-x=0的结果，之后再对控制流图进行合并，可以得到x-x∈[0，0]。

3.2 变量为除数的情况

当变量作为除数时，即使变量的取值范围的区间很小，其算术运算结果也肯能在较大范围内变动，导致分析结果精度下降，有误报产生的可能。当变量除数的取值区间较小时（例如小于1000），可以根据变量的所有可能取值，对控制流图进行迹划分，当所有计算结果全部计算完毕后，对控制流图进行合并，可以极大增加分析的精度。考虑如下的程序。

int r=0；float x=0.0；

while（true）{

r=random（0，50）；

x=（x*r+random（-100，100））/（r+1）；}

若使用区间抽象域分析变量x的取值范围，当迭代到不动点时，有x∈[-5100，5100]，若根据变量r的取值将控制流图划分成r=0、r=2…r=50的51条迹，在合并后得到x∈[-100，100]，即对所有的r∈[0，50]都有x∈[-100，100]。提高了分析精度。

3.3 循环中存在算术运算的情况

当循环中存在算术运算时，特别存在数组运算时，大部分抽象域的近似过程都会导致循环变量无法参与循环体内的算术运算，例如对于i∈[0，3]，xi=-10，0，3，7，yi={-1，2，3，4}，如果循环体内存在算术运算xi×yi，根据区间抽象域的定义，其结果取值范围是所有可能结果的最小上界，即xi×yi∈[-40，28]。实际上，若根据循环语句将控制流图划分成四个部分，其结果只可能是10、0、9和28，因此有xi×yi∈[0，28]，同样提高了分析过程的精度。由于编程习惯，许多循环体中都会在第一次循环时对变量进行初始化，因此可以将循环语句的控制流图划分成第一次循环和剩余循环两条迹来进行分析，也可以提高分析精度。

4 结束语

基于抽象解释的迹划分技术是一种提高分析精度的方法，其根据程序运行的迹对程序控制流图进行了划分，以局部分析复杂度上升为代价，提高了全局分析精度，可以减少许多误报，增加了基于抽象解释的静态分析方法在实际应用过程中的适用性。介绍了基于抽象解释的迹划分技术的理论框架，说明了其如何对程序控制流图进行划分；之后解释了在实际分析过程中，在哪些情况下使用迹划分技术可以显著提高分析精度，降低分析过程中由于抽象解释的过近似而产生的误报。在之后的工作中，可以对迹划分可以应用的场景进行扩展，以期其可以具备更高的适用性。

参考文献

[1] 黄志球，徐丙凤，阚双龙，等.嵌入式机载软件安全性分析标准、方法及工具研究综述[J].软件学报，2014，25（2）：200-218.

[2] DELMAS D，SOUYRIS J.Astrée： from research to industry[C]//International Static Analysis Symposium.Springer Berlin Heidelberg，2007： 437-451.

[3] 黄传林，黄志球，胡军，等.基于扩展SysML 活动图的嵌入式系统设计安全性验证方法研究[J].小型微型计算机系统，2015，36（ 3） ： 408-417.

[4] 侯刚，周宽久，勇嘉伟，等.模型检测中状态爆炸问题研究综述[J].计算机科学，2013，40（S1）：77-86.

[5] JHALA R，MAJUMDAR R.Software model checking[J].ACM Computing Surveys （CSUR），2009，41（4）： 21.

[6] COUSOT P，COUSOT R，MAUBORGNE L.Theories，solvers and static analysis by abstract interpretation[J].Journal ofthe ACM （JACM），2012，59（6）： 31.

[7] MINE A.The octagon abstract domain[J].Higher-Order and Symbolic Computation，2006，19（1）：31-100.

[8] COUSOT P，HALBWACHS N.Automatic Discovery of Linear Restraints Among Variables of a Program[C]// 2001：84-97.

[9] NIELSON F，NIELSON H R，HANKIN C.Principles of program analysis[M].Springer，2015.

[10] COUSOT P，COUSOT R.Abstract interpretation： past，present and future[C]//Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic （CSL） and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science （LICS）.ACM，2014：2.

[11] 陆陈，黄志球，阚双龙，等.基于八边形抽象域的襟缝翼控制系统安全性分析[J].小型微型计算机系统，2016，37（5）：902-907.

[12] HOLLEY L H，ROSEN B K.Qualified Data Flow Problems[J].IEEE Transactions on Software Engineering，1981，SE-7（1）：60-78.

[13] COUSOT P，COUSOT R.Comparing the Galois connection and widening/narrowing approaches to abstract interpretation[C]// Programming Language Implementation and Logic Programming，International Symposium，Plilp92，Leuven，Belgium，August 26-28，1992，Proceedings.1992：269-295.

[14] HARROLD M J，MALLOY B，ROTHERMEL G.Efficient Construction of Program Dependence Graphs[J].AcmSigsoft Software Engineering Notes，2000，18（3）：160-170.endprint