静态程序分析过程中形式化验证工具Frama-C的应用

崔少轩 喻壵慎

摘要：軟件的静态程序分析是确保软件安全可靠的一种有效手段。常见的形式化的静态分析工具一般是基于模型检测，定理证明或抽象解释理论来对软件进行分析验证。然而，基于单一理论的验证工具具有一定的局限性。介绍了一个开源的静态分析平台Frama-C，根据该工具的特点，分别使用不同的插件对一小段代码进行静态分析，有助于将不同的程序分析方法相结合。最后对如何使用Frama-C工具解决航空控制软件等安全关键软件的执行时间分析问题的过程进行了演示。

关键词：静态程序分析;形式化验证;Frama-C

中图分类号：TP391

文献标识码：A

随着计算机技术在安全关键领域的广泛应用，计算结果的准确性和产生计算结果的时间属性称为人们关注的焦点。一般采用软件测试的方法来保证程序的正确性。但是在测试过程中又不可能将程序所有的输入情况和执行条件覆盖在内。为了对软件的质量进行更加完备的评估，现在学术界正在广泛地研究使用形式化的静态分析方法来对软件的性质进行分析验证。但是形式化验证方法在实际应用中使用程度不高。一方面是一些形式化的验证工具的自动化程度不高，需要用户有较高的理论基础才能使用，因而难以被推广。另一方面，许多形式化验证工具的只是基于一种形式化验证方法，难以兼顾不同形式化验证方法的优点。

第1节简单描述了模型检测，定理证明和抽象解释理论的基本原理，并且对这3中形式化的分析方法进行比较。第2节介绍了一种自动化程度较高的开源的软件静态分析平台Frama-C以及基于该平台的常用插件。第3节结合Frama-C平台上插件之间的特点，分别使用程序切片，程序标注和基于Widening算子的值分析插件对一段循环程序中的变量的运行结果进行计算。第4节就航空发动机等一系列控制软件所要面临的程序执行时间分析过程中对循环结构的迭代次数的估算问题，使用Frama-C工具的应用过程进行了简单的演示。最后在第5节中对本文的工作以及研究现状进行了总结。

1 相关工作

静态程序分析是指在不实际执行程序的情况下对计算机软件进行分析[1]。它常常作为动态测试的补充来保证程序的正确性。目前主要的静态分析方法主要有模型检测，定理证明和抽象解释。

1.1 模型检测

模型检测是一种探测系统所有可能的状态的验证技术[2]。模型检测通过遍历迁移系统所有状态空间，对遍历到的系统进行自动验证，并且对不满足验证性质的情况自动构造反例。模型检测的本质是验证一个给定的系统的形式化模型满足规约条件。其基本思想是使用迁移系统（S）表示系统的行为，用模态逻辑或时序逻辑公式（F）描述系统的性质。将“系统是否具有所期望的性质”的问题转化为“状态迁移系统S是否是满足公式F的一个模型”的问题[3]。早期的模型检测技术被广泛应用于抽象系统模型以及硬件系统的模型，但最近模型检测技术已经被广泛应用与诸如C程序或Java程序的软件系统中[4][5]。

1.2 定理证明

定理证明是一种证明逻辑公式有效性的演绎证明方法。定理证明方法通过使用推导规则对逻辑公式进行证明[6]。通过定理证明工具编程者可以交互式地或自动地验证公式的正确性。定理证明的基本思想是将软件系统和性质都用逻辑方法来规约，通过基于公理和推理规则组成的形式系统，以如同数学中定理证明的方法来证明软件系统是否具备所期望的关键性质[7]。

1.3 抽象解释

抽象解释理论[8]是一套抽象和构建逼近的理论，它提供了一个通用框架来设计和构建静态分析以自动化地推导程序的静态性质[9]。抽象解释理论的作用对象是对复杂或无穷系统以及进行形式化表述的数学结构以及推导或验证这些系统的组合或不可判定的性质[10]。抽象解释理论的提出就是为了在对程序进行静态分析时构造和逼近程序的不动点语义。抽象解释严格定义了具体程序语义与抽象形式语义之间的关系、正确性与精确性等不依赖于特定应用的抽象数学概念。它的本质是在计算效率和计算精度之间取得均衡，以损失计算精度求得计算可行性，再通过迭代计算计算增强计算精度的一种抽象逼近方法[11]。

与模型检测技术相比，采用抽象解释的基本理论为分析框架，在模型检测方法中去掉一些无关信息，通过状态集合之间的映射关系构造抽象模型，可以有效解决模型检测方法中状态空间爆炸的问题。与定理证明相比，一阶逻辑是半可判定的，定理证明不能保证停机问题，而抽象解释是解决不可判定问题的一种有效的方法。由此可见将不同的形式化验证方法进行有效的结合的新的形式化验证工具是十分必要的。

2 Frama-C工具简介

Frama-C就是一个基于不同理论对程序进行分析验证的平台。它的分析对象是C程序源代码。如图1给出了Frama-C的基本框架。这个平台基于同一个核（ kemel），并且使用同一种形式化的规约语言ACSL即标准C规约语言（ANSI C Specifi-cation Language）用于对C程序做标注（annota-tion），因此基于Frama-C平台开发的一系列插件可以合作用于对软件进行静态分析，推导证明以及测试[12]。同时，Frama-C也提供了一些可扩展的API方便用户开发插件。其中，Frama-C平台上基于抽象解释，演绎验证和具体的符号执行测试开发三个基本的插件，并在此基础上衍生了一些列其他的插件。一些常见的Frama-C插件如表1所示。

Frama-C的插件之间可以组合使用得益于构建在该平台上的各插件之间共享使用Frama-C提供的一种形式化的行为规约语言ACSL，用户对程序的功能特性进行描述。针对Frama-C上的几个常用插件的简单介绍如下：

（1）基于抽象解释的值分析插件

Frama-C的值分析插件基于抽象解释原理，能够自动地计算程序变量在不同的程序点中可能的取值，并且对潜在的运行时错误发出警报。类似的商业化的软件例如Polyspace和Astree也有这些的功能。但是Frama-C的值分析插件除了具有开源的优势外，更显著的不同的是，Frama-C的值分析插件可以应用于满足ISO C99标准的所有源代码，而并不针对某一特定的应用领域。除此之外Value插件的独特之处在于它根植于Frama-C的系统框架中，其结果能够别Frama-C的其它插件重用。

（2）基于推导验证的Jessie和WP插件

这两个插件基于最弱前置条件技术，用于证明C代码满足使用ACSL描述的程序规约。推导验证的方法是基于模型的。对一个C程序，使用抽象表达的算法模型来对整数或浮点数进行描述，使用内存模型对程序的存储进行抽象。而使用WP插件能够减缓验证条件，独立于特定的模型.对于算法模型，用户可以使用选择整数、浮点数机器整数、实数或浮点数。而WP插件的内存模型直接收到最弱前置条件算子的启发，假定程序中是不包含指针的。

（3）基于程序流分析的切片插件

Frama-C的切片插件（slicing）将原有的代码的一个子集作为输出。产生切片程序的依据是用户提供的切片准则。并且作为输出的切片程序仍然是与原程序具有相同行为的可编译的C代码。

3 应用示例

与一些基于模型检测或定理证明或抽象解释理论等单一理论的形式化验证工具相比，Frama-C基于不同理论的插件之间能够互相协作有利于兼顾不同理论的优点。产生了基于Frama-C平台的组合验证策略。通过使用一个插件的输出作为另一个插件的输入，可以将不同的分析验证理论相结合。例如，首先可以在如下代码段中使用Frama-C的Slicing插件对程序中与循环相关的变量进行切片，得到与循环相关的切片程序如图2所示：

由切片程序可以得到与循环相关的程序变量i，j，n，显然，n的大小在整个循环过程中不变。由此我们在程序中对相关的循环变量添加形如/*@looppragma WIDEN_HINTS vl，，vn，el，…，em;术/的标注来指定循环迭代的次数，如图3所示：

最后，使用Value Analysis插件对循环进行分析得到变量i，j的在程序运行后可能运行结果：

[value]======VALUES COMPUTED======

[value] Values at end of function main：

i∈{13;14;15）

j∈[0_55]

n∈{13）

此外，針对循环，值分析插件分别提供了不同的循环选项，分别是在缺省状态下计算循环中变量的取值范围（ default），强制指定循环边界（stipulat-ing），以及对循环的句法展开（syntactic unrolling）和语义展开（ semantic unrolling），如表2给出了针对不同的循环处理，得到最终变量的取值范围。

4 应用领域

在一些安全关键领域的程序分析验证过程中，形式化的分析验证方法对软件的安全性质验证具有重要的作用。例如在一些实时的安全关键系统中，比如航空发动机系统，飞机的襟缝翼控制系统，对程序能够在规定的时间范围内完成指定的任务有较高的要求。在对程序的执行时间进行分析时，需要对程序的软件执行过程和程序所运行的硬件环境进行分析。其中软件的执行过程的分析过程中着重考虑的是程序的执行路径。例如程序在执行过程中循环结构的迭代次数等问题。为此需要采用Frama-C的切片插件将程序执行过程中与循环相关的程序语句作为切片的结果。例如在某程序的切片处理后得到如图所示的切片结果。切片程序中仅仅保留了与循环迭代相关的程序语句。现在对该程序的循环迭代次数进行估计。

input（i）;//循环变量i=[1..4]

while（i<10）f

input（j）;//循环变量j=[1..4]

while（j<10）f

j=j+2;

}

i++：

）

通过使用Frama-C的值分析插件对程序中的循环变量进行分析之后得到i和j取值分别为：l=[1;。10]，j=[1。。10]。在较为粗糙的循环边界计算过程中，可以简单的认定程序的循环边界为10*10=100次，实际的程序循环迭代次数显然是小于这个值的。将变量i和j的初始值i=[1。。4]，j=[1。。4]带人切片程序中，循环的迭代过程中计算结果如表3所示：

不难估算程序的循环边界为10：1：5=45次。为了对验证估值45是否可以作为更加精确的程序循环边界，首先使用Frama-C值分析插件中对循环进行展开的模块在设置循环展开100次是得到如图4所示结果：

显见，在循环展开100次之前循环变量i和j的取值已经满足了循环的退出条件，循环的实际迭代次数小于100。为了对45进行验证，设定循环的展开次数为45次，仍然得到如上图所示的结果。从而证明45次可以做为相对100次更加精确的循环迭代次数。在对程序的循环边界进行分析过程中，获取较为精确的循环边界对程序的执行时间分析具有中要的意义，尤其是程序的循环上界对航空发动机系统的最坏执行时间（ Worst Case ExecutionTime，WCET）的分析过程中意义重大。

5 结论

第3节的示例是简单展示了Frama-C平台上Slicing插件和Value Analysis插件的使用，使得不同原理的静态分析技术可以组合使用完成程序的静态分析过程。在第4小节中针对一些航空控制软件普遍面临的执行时间分析的问题中如何使用Frama-C进行程序的循环边界的分析验证过程进行了简单的演示。而在[13]的案例程序分析过程中，使用通过迭代使用Value Analysis插件和WP插件不断对程序添加标注以及分析来对程序进行验证。类似的分析验证策略还出现在软件最坏执行时间分析软件SWEET[14]中，首先对程序进行切片，计算循环边界最后依据程序标注中的不变式对产生的循环边界进行精化，能够得到较为精确的循环边界。这些案例表明支持使用不同静态分析技术的形式化分析验证平台对软件的形式化分析验证意义重大。

參考文献

[1]

WICHMANN B A，CANNING A A.Industrial perspective on staticanalysis[J].Software Engineering Journal. 1995，10（2）：69-75.

[2] BAIER C.KATOEN J P.Principles of model checking [M]. TheMIT Press Camhridge， Massachusetts， 2008.

[3] LIN H M.ZHANG W|L Model checking：theories，techniquesand applications[J]. ACTS ELECTRONICA SINICA.2002.30（12）：1907-1910.

[4]

VISSER W，HAVELUND K.BRAT G， et al.Model checking pro-grams[J]. Automated Software Engineering;， 2003， 10（2）：203- 232.

[5]

BEYER D.KEREMOGLU M E.A tool for configurahle softwareverification[J].Computer Aided Verification（ CAV' 11）， 2011，184-190.

[6]

SCHUMANN J M.Automated theorem proving in software engi-neering[M].Springer， Berlin， 2001.

[7]

CHEN H W.WANG J. DONG W. High confidence software engi-neering technologies [J]. ACTA ELECTRONICA SINICA . 2003 .31（12） ：1933-1938.

[8] COUSOT P. COUSOT R. Abstract interpretation ： a unified latticemodel for static analysis of programs by construction or approxi- mation of fixpoints [C]. Proc. of the 4th POPL. Los Angeles ： ACMPress . 1977 ： 23 8-252.

[9] CHEN L Q， WANG J.HOU S N. An abstract domain of one-vari-ahle interval linear inequalities

[J]. Chinese Jouranl of Comput-ers . 2010 . 33 （3） ： 238-252.

[10]

COUSOT P . COUSOT R. Ahstract interpretation ： past ， present andfuture [C]. CSL-LICS '14 Proceedings of the Joint Meeting of theTwenty-Third EACSL Annual Conference on Computer ScienceLogic

（CSL） and the Twenty-Ninth Annual ACM/IEEE Sympo-sium on Logic in Computer Science （ LICS ） .2014.

[11] LI M J， Li Z J .CHEN H W. Program verification techniques basedon the abstract interpretation theory [J]. Journal of Software.2008 .19（ 1） ： 17-26.

[12] KIRCHNER F.KOSMATOV N.PREVOSTO et al. Frama -C ： asoftware analysis perspective

[J] . Formal Aspects of Computing ，2015 .27（ 3 ） ： 573-609.

[13] BOULANCER J L. Static analysis of software [M].ISTE Ltd andJohn Wiley & Sons， 2012.

[14] ERMEDAHL A.SANDBERG C.GUSTAFSSON J，et al. Loophound analysis hased on a comhination of program slicing，ah-stract interpretation ， and invariant analysis

[C] . 7th InternationalWorkshop on Worst-Case Execution Time Analysis （ WCET'07 ） . 2007.