基于CPA的抽象解释分析方法研究

张弛　黄志球　丁泽文　刘林武

摘要：安全关键领域中，如何保证软件安全性已经成为了一个广受关注的重要课题。确保程序中没有运行时错误，对于软件安全性的保证十分重要。基于抽象解释的静态分析方法对程序语义进行抽象，是验证运行时错误最合适的形式化方法之一。可配置程序分析（configurable program analysis，CPA）是一种适合多种静态分析方法的通用分析框架。本文使用CPA对抽象解释分析方法进行建模，给出了使用基于CPA的抽象解释方法验证程序中的运行时错误的验证流程，并用实例说明该验证方法的有效性。为程序中运行时错误的自动化分析和验证提供了一种可行方案。

关键词：可配置程序分析；抽象解释；静态分析；运行时错误验证

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

Abstract：How to ensure software safety has become an important subject in safety critical domain.Ensuring the absence of runtime errors in the program is very important for the safety of the software.The program semantics was abstracted by the static analysis method based on abstract interpretation，and it is one of the most appropriate formal methods for validating runtime errors.Configurable program analysis is a general analytical framework for a variety of static analysis methods.The CPA is used to model the abstraction analysis method，and the validation process of using CPAbased abstract interpretation method to verify the runtime errors in the program is given.Then the effectiveness of the method is illustrated by an example.This provides a feasible solution for the automatic analysis and verification of runtime errors in the program.

Key words：configurable program analysis；abstract interpretation；static analysis；runtime error verification

1引言

近年來，随着软件在医疗、交通、航空航天等安全关键领域的广泛应用，软件已经成为决定系统安全性的主导因素，如何提高软件质量，保证系统安全性，防止灾害事故的发生，已经成为当前工业界和学术界的重要研究课题[1]。程序作为软件的核心，对于程序中运行时错误的验证是确保软件安全重要的一环。运行时错误是一类特定的软件错误，是指程序在运行时或运行后发生的错误，并不是软件需求和设计阶段引入的问题，而是在程序编写时，由于违反程序语言的安全性规范而引入的问题[2]。例如程序中出现除数为零的情况、程序中出现数组下标越界的情况等等。

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

可配置程序分析是一个形式化的进行软件验证和程序分析的通用框架。旨在用一种通用的形式化体系，通过配置不同的参数，来设计实现多种静态分析方法[7]。因此可以使用基于CPA的静态分析框架来对抽象解释的分析阶段进行建模。来对运行时错误进行分析和验证。

本文第2节简单介绍抽象解释中的基本概念和用于之后分析的区间抽象域。第3节具体介绍CPA静态分析框架的形式化体系表示方法及相应的迭代算法。第4节给出运行时错误的具体验证流程。第5节用一个实例来解释说明如何使用该方法，来对程序中的运行时错误进行分析和验证。第6节，结束语。

2相关理论

21基于格的抽象解释

抽象解释理论是P.Cousot和R.Cousot于1977年提出的对程序语义进行可靠近似理论[8][9]。其基本思想是用抽象语义代替具体语义来描述源程序语言，利用得到的抽象语义来实现具体语义的计算，程序的抽象执行的结果能反映程序真实执行的部分信息。抽象解释本质上是一种基于格的程序分析方法，下面给出一些相关的基础概念。

定义2.1偏序：如果≤是p上的二元关系，如果p中所有元素都具有自反性、传递性和反对称性，则称≤为p上的偏序关系，称为一个（p，≤）偏序集。

定义2.2格：对于偏序集（P，≤），若P中任意两个元素都存在上确界和下确界，则称（P，≤）是格，为方便，这样的格称为偏序格。

定义2.3完备格：对于格（P，≤）如果存在最小元素和最大元素，则称其为完备格，完备格可以用一个六元组来（P，≤，∪，∩，⊥，T）表示，其中∪表示最小上届，∩表示最大下界，⊥表示集合P中最小元，T表示集合P中最大元。

定义2.4伽罗瓦（Galois）连接[10]：如果两个偏序集（P，≤）和（P*，≤*）之间存在转化函数α：P→P*和逆向转化函数Y：P*→P，当对x∈P，x*∈P*，α（x）≤*x*x≤γ（x*）则称转化函数构成的函数对（α，γ）为集合P和P*之间的伽罗瓦连接，记作：

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

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

22区间抽象域

区间抽象域在静态分析过程中，主要用于表示某程序点处某一变量可能取到的最小值和最大值所构成的区间来近似[11]。具体域和抽象域之间的关系可以通过下面一个Galois连接来表示：

（R，≤）αγ（Itvs，i）

区间抽象域可以用一个完备格来表示，即（Itvs，i，∪i，∩i，⊥i，Ti），其中，Itvs是实数R上的区间的集合，其形式化的表示为：

{[a，b]|a∈R∪{-∞}，b∈R∪{+∞}，a≤b}∪{⊥i}。

i是Itvs上的偏序关系，形式化定义为：[a，b]i[a′，b′]当且仅当[a，b]=⊥i或者a≥a′^b≤b′，⊥i为集合上的最小元，满足γ（⊥i）Δ，（-∞，+∞）为集合上的最大元，满足对I∈Itvs，Ii[-∞，+∞]。通过这样的方式可以将程序中变量的取值抽象成形如a≤x≤b的约束，可以用于与分析变量取值范围相关的程序属性验证，例如除零错或数组越界的验证。"

3基于CPA的抽象解释分析方法

CPA是一个形式化的软件验证和程序分析的通用框架，可以通过配置参数来实现不同静态分析方法。基于CPA的抽象解释静态分析方法以程序控制流图为分析对象，选择不同抽象精度的抽象域来决定分析过程的抽象层次，选择不同的merge操作和stop操作来配置不同的迭代分析算法。其配置分析过程如图1所示。

在CPA配置分析过程中，将程序控制流图信息结合抽象域的定义，得到抽象状态的迁移关系；根据抽象域中域操作的定义配置CPA迭代算法中的merge操作和stop操作。根据抽象状态的迁移关系，执行CPA迭代算法来求解不动点抽象值，抽象状态之间通过merge操作来合并形成新的抽象状态，直至stop操作为真，则可判断没有新的抽象状态产生，迭代结束。

下面介绍CPA的形式化体系的表示方法和相应的CPA迭代算法。

31CPA形式化体系

CPA形式化定义为ID=（D，∽，merge，stop）， 其中包括抽象域D，抽象状态迁移关系∽，合并操作merge，终止判断操作stop。 CPA通过配置这四部分来完成一次静态分析的分析阶段，通过选择不同的配置来实现不同精度和效率的静态分析。下面具体说明这四部分

（1）抽象域D=（C，ε，[·]），其中C为程序具体状态的集合，其中一个具体状态c为程序运行到某一状态时变量在不同程序结点处的实际值，即X∪{Pc}，其中X为变量集合，{Pc}为程序结点集合。ε是用于描述抽象环境的完备格ε=（E，，∩，∪，⊥，T），其中E是抽象状态集合，E×E是抽象状态间的偏序关系，∩表示最大下界，∪表示最小上界，⊥∈E表示集合中的最小元素，T∈E 表示集合中的最大元素。具体化方法[·]：E→2c賦予抽象状态其对应的具体状态集，即一个抽象状态可能对应多个具体状态。为了保证分析可靠性（soundness），我们要求[T]=C，[⊥]=；e，e′∈E，[e∪e′][e]∪[e′]。

（2）抽象状态迁移∽E×G×E其中E是抽象状态集合，G是控制流图的边的集合。∽表示一个抽象状态e通过一个CFG的边g到达一个新的抽象状态e′记为e∽e′。为了保证分析过程的可靠性，我们要求e∈E：e′∈E：e∽e′，e∈E，g∈G：Uegete′[e′]UC∈[e]{C′|CgC′}。

（3）合并操作符merge：E×E→E将两个抽象状态的信息进行合并。为了保证分析的可靠性，我们要求

e′merge（e，e′）。

（4）终止判断操作stop：E×2E→B表示某一个抽象状态是否被一个抽象状态集合所覆盖，为了保证分析的可靠性，我们要求

stop（e，R）=true→[e]∪e′∈R[e′]。

32CPA迭代算法

CPA的迭代算法是可达性计算算法。其输入为一组配置完成的CPAID=（D，∽，merge，stop），以及一个初始抽象状态e0∈E，其中E是抽象域D中的抽象状态的集合。CPA执行算法不断更新两个存放抽象状态的集合。一个是reached集合，用来存放所有可以到达的抽象状态。一个是waitlist集合，用来存放所有还未被执行过的抽象状态。对于某一状态e，根据抽象状态迁移关系∽可以找到其对应的一个或多个后继结点，对于任意后继结点e′，用其与目前reached集合中所有的抽象状态进行merge操作。然后判断是否有新的结点产生，即是否没有被reached集合中所有抽象状态所覆盖。如果产生新的抽象状态，则将其加入reached集合和waitlist集合中。重复执行算法，直至所有的抽象状态进行merge操作后都无法找到新的结点，即此时找到的程序的不动点。具体的执行算法流程详见表1。

4程序运行时错误的验证方法

图2给出了一个基于CPA的抽象解释方法的分析框架，用于对程序的运行时错误进行分析和验证。该过程主要分为三个阶段：预处理阶段、分析阶段和验证阶段。

在预处理阶段。由于抽象解释方法是一个基于状态迁移系统的分析方法，因此需要在预处理阶段，将待分析系统转化成与之等价的抽象表示，即通过词法分析和语法分析器得到其抽象语法树，然后转化成便于进行分析的状态迁移系统。之后，我们将状态迁移系统转化到程序控制流图（control-flow graph，CFG）[12]。

分析阶段是抽象解释理论表现的主要阶段。在这个阶段，CPA静态分析框架需要以程序控制流图、抽象域的域元素、配置的merge操作和配置的stop操作为输入。其中程序控制流图由预处理阶段生成。其中抽象域中的域元素以完备格的形式提供输入，在相应的域操作中提取merge操作和stop操作，以完成CPA形式化体系的输入。相应的CPA迭代算法运用抽象解释中的迭代策略，计算程序控制流图中所有结点的不动点抽象值，从而完成分析。

在验证阶段，将得到的程序结点上的不动点抽象值转化为程序具体的变量约束关系，根据系统的需求文档和设计说明文档对程序的变量数值性质进行分析，判断变量的数值性质是否满足规约，得到分析结果，从而完成整个抽象解释静态分析的过程。图3以除零错为例，说明如何对运行时错误进行验证。根据分析阶段得到的不动点抽象值，结合源程序中与除数变量相关的代码，得到变量的约束关系，然后判断在各个程序结点，是否存在除数为零的情况，完成分析验证。

4CPA的分析实例

本章用一个实例来说明如何使用可配置程序分析CPA来对基于抽象解释的静态分析的分析阶段进行建模。以图4中代码为例，使用区间抽象域进行分析，以期得到各个程序結点处变量的取值范围。

根据第四章分析框架，首先在预处理阶段，根据相关词法分析和语法分析，将源程序转化到其控制流图，转化结果如图5所示。

在分析阶段，根据程序控制流图和抽象域的定义，配置CPAID=（D，∽，merge，stop），即分别配置抽象域D，抽象状态迁移关系∽，抽象状态的合并操作merge，终止判断操作stop。下面给出具体过程：

（1）配置抽象域D=（C，ε，[·]）为区间抽象域。其中C为程序具体状态的集合C{pc，x}，其中pc∈{s1，s2，…，s11}，X={x，y}；描述抽象环境的完备格

ε=（E，，∩，∪，⊥，T），其中E是抽象状态集合，具体状态和抽象状态通过一个Galois连接彼此关联

（R，≤）αγ（Itvs，）

其中R是实数域，Itvs是实数域上的区间集合。例如程序具体状态c（pc=s3，{x=0，y=0}）转化成的抽象状态是e（pc=s3，{x∈[0，0]，y∈[0，0]}）。

（2）抽象状态迁移关系∽，一个抽象状态通过图2程序控制流图上连通的一边到达一个新的状态。例如抽象状态e（pc=c，i∈[1，1]）通过边（pc=c，i=i+1，pc′=d）到达抽象状态e′（pc=d，i∈[2，2]）；抽象状态e（pc=c，i∈[1，11]通过边（pc=b，assume（i<=10），pc′=c）到达抽象状态e′（pc=c，i∈[1，10]）。以此类推来遍历寻找所有可能达到的抽象状态。

（3）合并操作符merge用以表示两个抽象状态的合并，在经典区间抽象域的抽象解释中，表示两个区间抽象域的合并，即mergejoin（e，e′）=e∪e′。

两个区间的合并如下：

例如抽象状态e（pc=s3，{x∈[0，0]，y∈[0，0]}）与抽象状态

e′（pc=s3，{x∈[1，1]，y∈[1，1]}）进行merge操作形成新的新的抽象状态

e″（pc=s3，{x∈[0，1]，y∈[0，1]}）。

（4）终止判断操作stop用以判断某一个抽象状态是否被一个抽象状态集合所覆盖，在区间抽象域的抽象解释中表示是否产生了之前所达到的抽象状态集合没有覆盖到的抽象状态，即程序是否到达了不动点，如果经过所有的迁移关系，都没有新抽象状态的产生，则整个抽象解释的分析就到达不动点。其配置为

stopjoin（e，R）=e∪e′∈Re′。

在完成配置CPA之后，执行CPA迭代算法。算法输入ID=（D，∽，merge，stop），初始状态

e0=（pc=s1，{x=⊥，y=⊥}），经过表1的CPA的迭代算法之后，各个程序结点处的不动点抽象值如表2所示：

根据算法结果，得到变量x和变量y在全部程序结点处的取值范围，可以对一些变量数值相关的运行时错误进行分析和验证。证明了该分析方法的有效性和可行性。

5结束语

针对程序中的运行时错误，本文提出了一种基于CPA的抽象解释的分析方法。首先介绍了一种支持抽象解释的静态分析框架，即可配置程序分析；然后给出了具体的静态分析流程，如何从源程序出发，转化成与之等价的控制流图，再转化到CPA形式化体系中进行迭代计算，最后根据得到的不动点抽象值进行相关运行时错误的分析验证；最后给出一个实例的分析过程，说明该静态分析方法的可行性和有效性。

接下来的工作中，我们将进一步扩展CPA支持的抽象域，如八边形抽象域、多面体抽象域，甚至一些非凸抽象域。并给出一个自动化的对运行时错误进行分析和验证的工具，来对研究工作进行完善。

参考文献

[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]计算机科学技术百科全书 ：选编本[M].北京：清华大学出版社，2002.

[4]CLARK E M，GRUMBERG O，PELED D.Model checking[M].MIT press，1999.

[5]L Hai，S Jigui，Z Yimin.Theorem Proving Based on the Extension Rule.[J].Journal of Automated Reasoning，2003，31（1）：11-21.

[6]COUSOT P，COUSOT R.Basic concepts of abstract interpretation[M]//Building the Information Society.Springer US，2004：359-366.

[7]BEYER D，HENZINGER T A，Théoduloz G.Configurable Software Verification：Concretizing the Convergence of Model Checking and Program Analysis[C]// International Conference on Computer Aided Verification.2007：504-518.

[8]COUSOT P，COUSOT R.Abstract Interpretation：A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.[C]// ACM SigactSigplan Symposium on Principles of Programming Languages.1977：238-252.

[9]COUSOT P，COUSOT R，Feret J，et al.The ASTRE Analyzer[J].Lecture Notes in Computer Science，2005，3444：140-140.

[10]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.

[11]COUSOT P，COUSOT R.Static determination of dynamic properties of programs[J].Proceedings of the Second International Symposium on Programming，1976.

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