支持抽象解释的静态分析方法的形式化体系研究

《支持抽象解释的静态分析方法的形式化体系研究》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、支持抽象解释的静态分析方法的形式化体系研究张弛黄志球丁泽文南京航空航天大学计算机科学与技术学院在安全关键领域屮，如何保证软件的安全性已经成为丫一个广受关注的重要课题。静态程序分析是一类十分有效的程序自动化验证方法。棊于抽象解释的静态分析技术在验证软件的非功能性安全属性上表现十分突出。可配置程序分析（ConfigurableProgramAnalysis,CPA）是一种通用静态分析方法形式化体系，旨在用一种形式化体系对静态分析的分析阶段进行建模。使用CPA对基于抽象解释的静态分析进行建模，给出如何使用CPA形式化体系描述基于抽象解释的静态分析，给出了从待分析程序到CPA形式化体系的转

2、换规则;提供了一种在安全关键性领域中的软件正确性自动验证方法，为基于抽象解释的静态分析工具的实现提供了一种可行方案。关键词：形式化方法;静态分析;抽象解释;可配置程序分析;静态分析不需要真实执行程序，只需对程序的语法语义进行静态分析［1］。与动态测试相比，首先，静态分析能够模拟程序运行时的所有状态，能对程序中所有可能的路径进行分析;其次，静态分析的木质是分析程序所转换成的状态模型内的状态转换关系。但是，分析整个程序的全部状态空间是不现实的。因此，静态分析方法往往需要对程序的状态空间进行抽象。静态分析往往要通过损失精度來达到提高分析效率和保证分析结果可靠性的目的。在保证分析结果正确性

3、的前提下，静态分析权衡了分析过程的精度和效率。目前，静态分析的主要形式化方法有模型检测、定理证明和抽象解释。模型检测的基本思想是通过穷举系统模型的状态空间来验证该模型是杏满足吋序逻辑描述的系统属性m。模型检测的工具主要有BLAST,Spin,UPPAAL等。定理证明利用逻辑系统对软件进行描述，通过公理或者推理规则对系统具有的安全性质进行规约验证位1，其主耍工具有PVS原型验证系统、定理证明器HOL等。抽象解释理论对程序语义进行抽象，将程序的只体语义转化到抽象域中，在抽象域中的抽象语义下对程序性质进行分析Ill。主要工具有ASTRR[5],Polyspace,Fluctuat等。可配

4、置程序分析是由Beyer等人提出的用于支持模型检测和抽象解释的静态分析形式化体系，旨在用一种形式化体系同时描述模型检测和抽象解释M。其可以被用来对抽象解释的分析阶段进行建模。目前，国内抽象解释的相关工作主要集中在非凸抽象域的研究m和抽象解释在安全关键性(SafetyCriticlaSoftware)软件屮的应用本文工作主要关注于提出一种可以扩展和参数化的抽象解释分析框架，以适应各种分析场景，为抽象解释工具的设计与实现提供一个可行方案。同时，用形式化体系描述抽象解释便于对其进行扩展，如多抽象域的结合或者通过参数调节分析过程的精度和效率。本文第2节介绍基于抽象解释的静态分析的一般过程，

5、给出一个通用的分析框架;第3节具体介绍可配置程序分析的形式化体系表示方法;第4节阐述如何将程序控制流图转化到CPA形式化体系中;第5节通过实例来说明如何使用CPA对程序进行分析验证;最后总结全文。2基于抽象解释的静态分析框架抽象解释理论是Cousot和Cousot[9]于1977年提出的在保证分析程序语义可靠性的基础上对程序语言进行抽象的理论。抽象解释理论的基本思想是用抽象语义代替具体语义来描述源程序语言，以确定程序抽象语义和具体语义之间的转化关系，之后求解程序抽象语义，利用得到的抽象语义来实现具体语义的计算，程序抽象执行的结果能反映程序真实执行的部分信息。其以损失精度为代价来确保

6、计算的可行性和高效性。该理论本质上是一种在计算精度和计算效率上获取平衡的静态分析方法。目前，基于抽象解释的静态分析方法主耍用于分析和验证系统的非功能性属性[10],其中主要括运行时错误的验证(程序中是否含有除零错、是否发生数组越界、是否发生算术溢出等)、最坏情况下执行时间(Worst-CaseExecutionTime,WCET)的计算等。图1给出了一个基于抽象解释的静态分析框架，该过程主要分为3个阶段:预处理阶段、分析阶段和验证阶段。图1基于抽象解释的静态分析框架在预处理阶段，由于抽象解释的静态分析工具是一个基于程序的分析工具，其直接分析对象是源程序，因此需要在预处理阶段将源代码

7、转化成与之等价的抽象形式，即通过词法分析和语法分析器得到其抽象语法树，然后转化成便于分析的状态迁移系统。一般地，我们选择程序控制流图(ControlFlowGraph,CFG)来表示源程序的状态迁移关系。一些成熟的抽象解释工具，如ASTR6E，在这个阶段还会进行一些参数化的处理，以便在实际验证分析时通过配置不同的参数来调节分析器的效率和精度［11］。分析阶段是抽象解释理论表现的主要阶段。在该阶段，构建特定的抽象域，将程序的具体语义转化到抽象语义上，然后结合抽象域和控制