近年来,随着软件在航空航天、高铁和医疗等领域所占的比重越来越大,提高软件的安全性和可靠性成为工业界和学术界关注的热点.传统的测试仿真技术在保证软件可靠性方面发挥着巨大的作用,但是对于安全关键软件,传统技术没有穷尽程序输入,无法遍历所有的执行路径,因此难以发现隐藏极深的软件错误.而且对于并发、实时等不确定执行系统,这类技术无法起到很好的作用.因此,需要引入形式化验证方法来保证系统的安全性.模型检测^[1]作为一种形式化验证技术,已经在硬件设计^[2]和网络协议^[3]方面取得了重大的突破.将模型检测技术应用到软件验证领域,尤其是对软件代码的验证,是学术界近10年的研究难点和重点.

软件模型检测技术目前主要有以下几类:(1) 基于完全状态搜索(explicit model checking)的模型检测^[1]技术,如贝尔实验室Godefroid等人开发的Verisoft^[4],该工具主要验证并发和实时软件系统;(2) 符号模型检测(symbolic model checking)技术^[5],包括使用BDD的符号模型检测^[5]和使用SAT(Boolean satisfiability problem)/ SMT的符号模型检测^[6],如McMillan提出的基于SAT的符号模型检测^[6];(3) 基于抽象解释^[7]的模型检测技术,包括谓词抽象^[8](predicate abstraction)和惰性抽象^[9](lazy abstraction),如微软的Ball等人基于谓词抽象开发的SLAM^[10]和加州大学伯克利分校采用惰性抽象技术开发的BLAST^[11];(4) 通过限制程序执行路径长度的有界模型检测(bounded model checking)技术,如卡内基梅隆Clarke等人开发的CBMC^[12]以及在其上开发的ESBMC^[13]和LLBMC^[14].

软件模型检测主要存在以下两个问题:

(1) 对于无限状态的程序模型,由于状态的无限性,模型检测问题本身就是不可判定问题;

(2) 对于有限状态的软件系统,状态空间爆炸是一个非常重要且难以解决的问题.

针对以上问题,文献^[12,15]提出了有界模型检测,对程序的递归调用层数和循环的次数都设定一个上界,这样程序必然终止,可以将不可判定问题转化为可判定问题.软件抽象解释技术^[7]对于将软件无限状态转化为有限状态以及约简软件的状态空间具有非常重要的作用,例如,谓词抽象^[8,16]是实现软件抽象自动化的非常成功的技术.SATABS^[17]是采用谓词抽象技术开发的C语言模型检测工具.布尔可满足问题求解技术SAT^[18]的发展,促使Clarke等人提出基于命题逻辑的C程序符号模型检测^[12].将C语言程序与所验证的属性转化为命题逻辑公式,然后利用SAT求解器(SAT solver)对公式进行求解,如果发现公式可满足,则找到程序的一条错误执行路径.可满足性模理论SMT(satisfiability modulo theory)^[19]是在一阶逻辑的基础上对数组、记录和算术运算等语义进行解释的判定过程.SAT/SMT求解器提高了模型检测的执行效率,文献^{[20, 21, 22]}表明,基于SAT和SMT的软件形式化验证技术现在已经成为国内外学者的关注重点.

除了以上的验证技术以外,对于程序属性的规约也是模型检测的重要方面,例如,采用线性时序逻辑LTL (linear temporal logic)^[23]和计算树逻辑CTL(computation tree logic)^[23]作为模型属性的规约语言.现在对C语言代码验证的属性规约可以分为两种类型:第1种是程序本身所固有的运行时属性,例如数组越界、算术除零和指针非法使用等错误;第2种错误是用户自定义错误,与应用语义相关,例如文件操作必须先打开后关闭、队列操作必须先进先出等.针对第2类属性的规约方法,现在的验证工具主要采用断言的形式.在所需验证的程序位置加入assert(expression),判断该断言在所有执行路径下是否成立.

基于断言的属性规约描述了从程序的初始状态到某个状态集合的可达性.一个程序的状态可以表达为(pc,var₁,var₂,…,var_n),其中,pc为程序当前执行位置,var₁,var₂,…,var_n为程序的所有变量.程序的初始状态就是pc指向程序起始位置,并且所有的变量值都为初始值.可达集合是pc指向程序的指定位置,并且变量满足一定的约束.这里的约束是一个谓词表达式,例如x>4Ùy<4,也就是所有的变量值满足x>4Ùy<4.在程序的位置l插入断言assert(x>4Ùy<4),就表达了一个程序的状态集合.CBMC^[12],BLAST^[11]和SATABS^[17]等模型检测工具都采用断言作为用户自定义属性的规约形式.

但是,基于断言的属性规约具有一定的局限性:

(1) 无法表达无限状态的安全属性,例如队列的先进先出属性;

(2) 对于程序的一条执行路径,我们希望表达整条路径应该满足的属性,比如路径执行必须先满足命题p再满足命题q,而可达性只表达最终到达状态的属性;

(3) 缺乏对程序中事件的表达.

针对以上的问题,结合近年来发展的运行时验证技术^[24,25,26],本文在断言的基础上提出了带变量的事件自动机^[27],对C语言属性进行规约.事件自动机带有变量,自动机发生转移的前提是事件的发生.事件自动机具有更强的表达力,可以描述事件发生的时序,可以描述无穷状态的安全属性.事件自动机是独立于程序本身的,因此与程序分离不会影响程序自身的结构.在嵌入式和操作系统等多事件系统中,该方法将有利于对系统属性规约.

在事件自动机的基础之上,我们采用基于SMT的有界模型检测作为程序验证技术基础,首先使用文献^[20]提出的方法将C程序转化为SMT模型,然后给出了自动机可达树的概念.通过自动机可达树,将事件自动机与C语言程序之间的约束关系转化为SMT模型.通过SMT求解器判断程序是否违反事件自动机所规约的属性,最后,根据求解器返回结果给出生成程序反例路径的算法.最后的实例分析表明:本文方法可以检测像变量溢出等底层错误,并且可以验证像队列先进先出等断言无法表达的属性.

本文第1节给出事件自动机的语法和语义规则及用事件自动机对程序属性规约的实例.第2节给出基于事件自动机规约的有界模型检测技术.第3节给出两个使用本文方法进行形式化验证的实例,并通过实验分析本文方法的执行效率.第4节给出结论.

1 使用事件自动机规约C程序安全属性

本节给出事件自动机的形式化定义、描述语言及其生成算法.

1.1 事件自动机的形式化定义

事件(event)在程序设计语言中可以定义为一条语句的执行或一个函数的调用.每一个事件都有一个标识作为事件的名称,本文使用S表示事件名的集合.

在程序中经常使用变量和常量,我们用Var和Val分别表示变量的集合和常量的集合.变量和常量统一称为符号量,用Sym来表示,Sym=VarÈVal.我们首先给出本文对事件的定义:

定义1(事件). 一个事件定义为或写为,eÎS为事件名,为事件参数序列.

根据事件的参数将事件分为两类:

1. 若则该事件为实参事件,即,所有的参数都是常量;

2. 若则该事件为形参事件.

为的第i个参数,对于参数个数相同的形参事件和实参事件如果满足以下任意一个条件,则和匹配:

(1) 若

(2) 若类型一致.

对于程序的一次运行来说,所有变量的值都是确定的,所以产生的事件也都是实参事件.但因为程序的输入是不确定的,因此,使用变量可以让规约的表达能力更强.例如,对于文件操作open和close,必须满足每一个open操作之后都要有一个close操作.使用正则表达式表达为(open(f) close (f)),这里的f为一个变量,它代表任意一个文件名,该正则表达式规约了任意文件的行为.

事件自动机是基于事件驱动转移的、监视源程序行为的一类自动机,事件自动机的变量机制可以增强自动机的表达能力.我们首先给出事件自动机的形式化定义:

定义2(事件自动机). 事件自动机是一个六元组:EA=(Q,Var,A,T,s₀,F),其中,

(1) Q是自动机状态的有限集合.

(2) Var为自动机变量的集合,自动机变量记录自动机转移中事件的信息,在自动机执行前部分变量要赋初始值.

(3) A为事件的有限集合,自动机只有在接收到A中的事件才会发生转移,带有形参的事件中形参必须是自动机变量.

(4) TÍQxAxGuardxAssignxQ,其中:Guard是一个谓词表达式,表示转移能够发生的条件,它是由自动机变量和所监视程序中的变量组合的一阶谓词逻辑公式;Assign为一组赋值语句,赋值语句中所有的写操作都是针对自动机变量,所监视的程序中变量是只读的.我们用d(s_i)表示一个自动机状态的所有下一个状态的集合,即,对任意状态s_jÎd(s_i),都存在转移(s_i,e,guard,assign,s_j).

(5) s₀为初始状态,对于有多个初始状态的自动机,可以很容易地转化为只有1个初始状态的自动机.

(6) F为接受状态集合,所有进入接受状态的程序执行路径都是反例路径.

在事件自动机中,我们定义了自动机变量集合.在自动机的状态转移过程中,对自动机变量进行写操作的方式有两种:第1种是通过转移函数中的Assign序列可以对自动机变量执行写操作;第2种方式是通过实参事件参数对变量进行绑定赋值.例如,事件自动机有一个转移(s₁,start(x),true,empty,s₂),当接收到一个事件start(2)时,则将x赋值为2,记为[xa2],这样就对自动机变量进行了赋值.

转移函数是事件自动机的核心概念.事件自动机转移发生的条件是:所监视的程序中出现了驱动事件,并且满足转移的Guard.然后,执行赋值操作序列Assign.如果在程序执行过程当中没有发生自动机所规约的事件,则自动机不发生任何行为.这与线性时序逻辑(LTL)对模型属性进行规约不同,模型每发生一次转移,由LTL转化为的Büchi自动机也要发生一次转移.

定义3(绑定). 一个绑定Bind是对一组变量的赋值,定义为一个映射,即Bind:Var®Expr.Expr为表达式集合,它由Sym中的符号组成.大多数情况下,绑定到一个变量的值为一个常量.这里,为了后面算法的表达方便,将其泛化为表达式.Binds(Var)表示一个绑定的集合,该集合中任意一个绑定都是对Var中的变量进行赋值.

定义4(配置). 我们引入配置的概念来实例化事件自动机的一次运行,事件自动机的一个配置Config定义为一个状态和自动机变量一个绑定的组合,即ConfigÎQxBinds(Var).事件自动机的转移都是建立在配置上的,对于一个转移(s,,Guard,Assign,s¢),并且在状态s的情况下绑定为j,转移可发生的条件:

· 当程序中产生一个与匹配的实参事件其中,我们将对应的实参中的参数值按顺序分别绑定到形参中的变量,得到新绑定j¢;

· j¢必须满足转移中的Guard,否则,转移无法发生,若转移不发生,则绑定j¢将被取消;

· 在转移可以发生的前提下执行Assign赋值序列,产生新的绑定j².

例如自动机接收事件start(x),若程序产生事件start(2),则生成绑定xa2.如果新绑定满足Guard,Assign也将

对自动机变量进行操作并产生新的绑定;如果start(2)不满足Guard,则不被自动机接收.

定义5(事件自动机的事件序列). 对于事件自动机EA和一个事件序列e₀e₁…e_n-1,假设自动机变量初始绑定j₀.如果存在EA的配置序列(s₀,j₀)(s₁,j₁)…(s_n,j_n),对于任意0≤i<n,存在转移(s_i,e_i,Guard_i,Assign_i,s_i+1)可发生,并且s_nÎF,则事件自动机EA接收该事件序列.

定义6(程序中事件的生成). 我们定义程序中一条语句的执行完成为一个事件的发生,所产生事件的名称可以为程序中某个函数的名称,也可以是我们自定义的名称.事件的参数可以是程序中的表达式,也可以是一个常量.将某个事件与一条执行语句绑定,表示当程序执行完该语句之后,程序将生成一个事件传递给事件自动机,事件自动机将会根据事件流对程序行为进行监控.

图 1给出了对函数sum绑定事件sum(a,b)的示例,在执行完最后一条语句return s之后将产生该事件,每当该函数被调用执行一次之后都会产生该事件.这里采用在注释中加入绑定事件的方法,不会影响程序的固有 结构.

本文事件自动机中的自动机变量和事件的参数类型限制在整型(int)、实型(real)和布尔型(bool).C程序中也会存在字符串类型的变量,在绑定事件的时候可以做一个映射,即,将字符串型变量映射到整型.另外,事件自动机变量不可以为指针类型,因为指针类型如果指向程序中的变量地址,会导致自动机转移修改程序的变量,这在监视过程中是不允许的.

为了方便表达,本文引入两个专有事件:

· 第1个是结束事件:terminal,因为对程序中所有的循环和递归加了上界,所以程序必然是终止的,在编码过程中,编码的最后产生一个结束事件.

· 第2个是完全事件:all,完全事件可以接收任何从程序产生的事件,也即当程序产生任意事件时,事件自动机的完全事件可以无条件匹配该事件.

对于事件的参数,我们引入“*”表达可以匹配任何参数.例如,start(*,y)表示接受任何事件名为start,第1个参数为任意值,第2个参数赋值给y的事件.下面给出两个事件自动机规约的实例.

图 2给出了一个描述文件操作的事件自动机实例,它有3个状态:s₀是初始状态,s₁是在打开一个文件之后的状态,s₂ÎF是接受状态.当自动机接收到一个open事件之后,就将open中的实参赋值给自动机变量f.显然,自动机描述了所有打开一个文件之后,但是程序终止时却没有关闭文件的执行路径.在状态s₀使用了完全事件,它的好处在于:当程序同时打开多个文件时,可以只用这1个事件自动机进行表达.对于自动机中没有guard和赋值序列的转移,我们在图中忽略,没有标出.

图 3给出了对一个队列先进先出(FIFO)属性进行规约的事件自动机,队列有两个操作:insert(x)将x插入到队列的末尾,delete(y)将队列头部数据删除并保存到变量y中.在初始状态,我们可以接收任意多个插入事件,但是一旦选择转移到状态s₁之后,则只接收删除事件,而忽略插入事件.通过计数变量cnt,我们可以判断当cnt=0时,再发生删除操作并且删除的数据不等于x,则必然不满足FIFO属性.因为规约的是错误属性,也就是说,当删除的不是x时,我们找到了一条错误路径.

1.2 事件自动机的描述语言及其生成算法

本文事件自动机描述语言的BNF范式定义如下:

EventAutomata::=Defines;

    Defines::=Define;Defines|Define

        Define::=Dstate|Dvariable|Dtransition

        Dstate::=define state Id Stype

            Stype::=0|1|2|3

  Dvariable::=define Type Id=Expr

            Type::=int|real|bool

  Dtransition::=define transition Id (Id;Event;Expr;Assignments;Id)

        Event::=Id(Syms)|Id(×)

            Syms::=Sym,Syms|Sym

            Sym::=Id|Constant

在BNF范式中,所有大写字母开头的都是非终结符,所有小写字母或数字开头的都是终结符.上述BNF范式所代表的含义如下:一个事件自动机(EA)是由一系列的定义(Define)组成,每一个定义(Define)可以是对状态的定义(Dstate)、对变量的定义(Dvariable)和对转移的定义(Dtransition):

· 一个状态的定义包括了表示该状态的标识符(Id)和该状态的类型(Stype),状态类型取4个值:0表示该状态既不是初始状态也不是接受状态,1表示该状态为初始状态,2表示该状态为接受状态,3表示该状态既是初始状态又是接受状态.

· 变量的定义包括变量的类型(Type)、变量的标识符(Id)和变量的初始值(Expr),其中,变量类型的定义包括3种数据类型:整型(int)、实型(real)和布尔型(bool).

· 转移的定义包括转移的标识符(Id)、转移的开始状态标识(Id)、转移的触发事件(Event)、转移应该满足的条件(Expr)、转移的赋值语句(Assignments)和转移的下一状态标识(Id).

事件的定义包括事件的标识符(Id)和事件的参数(Syms),事件可以没有参数或者事件的参数序列中每一个参数可以是一个变量(Id)或者一个常数Constant.

上述BNF范式中的非终结符Expr,Assignments,Id,Constant没有给出定义,这部分可以参考C语言BNF范式进行定义,这里不详细展开.下面我们给出图 2中事件自动机的描述:

define state s0 1; define state s1 0; define state s2 2;

define int f=nondet; define int f¢=nondet;

define transition t0 (s0;all;true;empty;s0);

define transition t1 (s0;open(f);true;empty;s1);

define transition t2 (s1;close(f¢);f¢=f;empty;s0);

define transition t3 (s1;terminal;true;empty;s2);

其中,关键字all表示完全事件.关键字empty表示空,例如上述的自动机描述中,empty表示该处不存在赋值语句.关键字nondet表示赋值为一个随机值.关键字true表示永真.

下面我们给出从事件自动机描述语言生成事件自动机的算法.

算法1. 事件自动机生成算法.

输入:L={l₁,…,l_n}为一组自动机描述语言的语句集合,它描述了一个事件自动机.

输出:事件自动机EA=(Q,Var,A,T,s₀,F).

算法描述:

CreateEA(L)

begin

           EA=EmptyEA;

           for each l_iÎL do

                    if l_i is in form [define state s c] then

                             add s to Q;

                             if c=1 then s₀=s; endif

                             if c=2 then add s to F; endif

                             if c=3 then s₀=s; add s to F; endif

                    endif

                    if l_i is in form [define Type v=expr] then add v=expr to Var; endif

endfor

           for each l_iÎL do

                    if l_i is in form [define transition t (s₀;e;expr;assignments;s₁)] then

                             add e to A;

                             add (s₀;e;expr;assignments;s₁) to T;

                    endif

           endfor

end

上述算法分为两个循环:第1个循环生成自动机的状态集合和变量集合;因为转移集合需要用到状态集合和变量集合,在这两个集合已生成的基础上才能生成转移集合和事件集合.其中,EmptyEA表示一个空事件自动机,空事件自动机的状态集合、变量集合、事件集合、转移的集合和接受状态集合都为空,并且初始状态未 设置.

2 基于事件自动机规约的有界模型检测算法

基于SAT和SMT的有界模型检测在C语言程序验证方面占据重要地位,包括CBMC^[12],ESBMC^[13],SATABS^[17]和F-Soft^[28]等,都是基于SAT/SMT的模型检测工具.本文将采用基于SMT的有界模型检测,将事件自动机和C语言程序转化为SMT模型.

布尔可满足问题(SAT)^[18]是针对命题逻辑的判定过程,其目的是确定一个由布尔变量和逻辑连接符析取、合取和取反组成的公式是否存在对其布尔变量的赋值使得公式的值为真.例如,(pÚr)Ù(pÚq)在p=true,q=false,r=false的情况下为真.一些问题需要更丰富的逻辑描述,例如一阶谓词逻辑.一阶逻辑是由逻辑连接符、变量、全称量词、存在量词、函数和谓词符号组成,一阶谓词逻辑公式的可满足性是建立在一个模型的基础上.模型解释了公式中的变量、函数和谓词.SMT对符号的解释是限制在一个理论背景中,例如算术运算(linear arithmetic)、位向量(bit vector)和自由函数(free function)等.

算术运算. 例如公式3x₁+2x₂≤5x₃Ù2x₁-2x₂=0,SMT求解器对其中的+,≤,-,=分别解释为算术加法、算术小于等于、算术减法和算术相等,并给出对x₁,x₂,x₃的赋值使其满足上述公式.

位向量. 定义了位向量的多种操作,包括与、或、非、异或、左移和右移等.例如公式a_[8]Ùb_[8]=á00000000ñ₂,SMT求解器判断是否存在对两个8位的位向量赋值,使得它们的与为0.

自由函数. 自由函数是不对函数做任何解释的函数,例如,f:int®int表示一个从整数映射到整数的函数,但是没有给出具体的映射.现在给出公式f(2)=3Ùf(3)=4,可知该公式可满足.如果f(2)已经绑定为5,则该公式不可满足.

关于SMT的详细理论可以参考文献^[19].本节主要分为3个部分:第1部分介绍将C程序转化为SMT模型的方法和原理,第2部分介绍事件自动机SMT模型转化方法,最后一部分给出反例路径的算法.

2.1C程序到SMT模型的转化

为了解决无限堆栈程序模型状态的无限性和程序中对递归和循环次数难以确定的困难,本文对有界模型检测的中“有界”的定义为设定循环和递归执行次数的上界.如果程序的执行不可能超过上界则正确进行检测,否则提示增大循环和递归的上界.

本节介绍的转化过程主要分为3个步骤:步骤1将C程序中的循环和函数调用进行展开;步骤2将步骤1中的程序转化为只包含if语句、赋值语句和断言的程序;步骤3将步骤2的程序转化为单一赋值形式(static single assignment).本节的转化过程参考了Clarke等人^[2,12]和Armando等人^[20]的工作,但是在数组和结构体的转化方面存在一定的差异.

步骤1. 循环与函数的展开.

C语言中的循环结构包括for,do...while,while等,这里我们只以while循环为例来演示如何将其展开,其他循环的展开方式类似.while循环的一次展开过程如下:

while(e) I;Þif(e){I; while(e) I;}.

在已经设定上界为n的情况下,我们将上述循环展开n次.对于展开n次之后的循环,并不能代表循环在n次之后一定结束,因此,我们需要判断在展开之后循环是否终止.我们将在最后一次循环展开加入一个断言来表示,即

assert(!e).

这样,当程序循环展开没有达到循环终止的条件时,断言就会提醒用户重新设定循环上界,验证算法是不会验证之后的程序,而只是局限在已经展开的部分.从图 4(a)到图 4(b)的转化为循环的展开过程.

递归函数可以采用与循环相同的策略进行展开.对于带有返回值的函数,增加一个辅助变量存放该函数的返回值,这样,我们把计算结果直接赋值给辅助变量,即可代替程序中的return语句.

步骤2. 转化为只包含if语句、断言和赋值语句程序.

经过步骤1的转化,程序中已经不存在循环语句和函数,因此,程序中只存在if语句、赋值语句、goto语句、break语句和continue语句等.continue语句和break语句都可以很容易地转化为goto语句表达,goto语句可以被转化为if语句表达的形式,switch语句也可以转化为if语句表达.这几步的转化并不是很复杂,这里不再详细叙述,Armando等人在文献^[20]中有完整的描述.

步骤3. 转化为单一赋值形式.

经过展开之后,程序将只包含if语句、赋值语句和断言(assertions).下面将其转化为单一赋值形式的SMT模型.

对每一个变量x,它的n个复制设为{x₀,x₁,…,x_n-1},其中,n是程序中对变量x赋值的次数.除了程序中的变量之外,单一赋值形式有一个guard变量,它表达的是程序执行到该位置所应满足的条件.对于每一个赋值语句,我们将赋值语句左边的变量下标加1,赋值语句右边所有的变量保持该语句之前的标号.

条件赋值表达为x=guard?x₁:x₂,即,guard为true,则x=x₁;否则,x=x₂.

一维数组可以看作是一个函数f:¥®data,其中,¥表示数组的下标,是包含0的自然数;而data表示的是符合数组元素类型的数据的集合.这样,f(i)就表示取数组中第i个元素.因为SMT求解器对于函数的表达非常方便,所以本文将数组表达为函数.例如,赋值语句a[k]=e,其中,a为一个数组,e为一个类型符合该数组的表达式,且在该语句之前数组的单一赋值下标为i,则该语句的单一赋值形式为a_i+1:=a_i with a_i(k)=e,即

对于多维数组可以转化为多个参数的函数,例如二维数组a[i₁][i₂],可以用a(i₁,i₂)来表示.

对于C语言中的结构体,SMT求解器中有针对Record的判定理论.而Record和结构体的特性非常相似,有利于我们直接对其进行转化.对于结构体赋值语句s.f=e,其中,s为结构体变量,f为结构体变量的一个数据分量,它转化成单一赋值语句为s_i+1:=s_i with s_i.f=e,即

.

图 4(b)到图 4(c)给出了步骤3的转化过程.

在转化的处理过程中,指针是一个非常重要的特性,本文对指针的转化主要采用Clarke E在文献^[2,12]中所给出的方法.对于一个变量a,我们用&a表示它的地址,地址是一个常数.当表达式中没有出现对指针表达式的间接引用时,对于一个指针变量p,转化为单一赋值形式与非指针变量相同,例如,p=p+1转化为p_i=p_i-1+1.当程序表达式中出现对指针表达式的间接引用时,情况比较复杂,下面将详细介绍.

通过使用一个递归函数f(e,g,o)消除程序中的指针表达式的间接引用,其中,e表示一个将要被间接引用子表达式,g表示该表达式被执行的guard,o表示偏移量.标准C语言提供两种间接引用操作符:“*”操作符和下标操作符:*e®f(e,g,0),e[o]®f(e,g,o).

对于任意一个指针都有它的类型*T,在语法分析的时候就可以确定.在介绍函数f之前,首先定义r(expr),其中,expr为一个符合C语言语法的表达式,r(expr)表示该表达式在程序中的单一赋值形式.

f函数的详细定义如下:

1. e是一个指针变量,且在已经生成的单一赋值形式中存在r(e)=e¢,那么f(e,g,o)=f(e¢,g,o).

2. e为一个数组,假设a为一个数组,e=a,即e=&a[0],那么f(e,g,o)=f(&a[0],g,o).

3. e为一个非数组变量的地址,假设e=&s其中,s是一个变量,那么f(e,g,o)等于s,并且o=0,即,f(e,g,o)=s.并且s的类型必须为T.

4. e为某个数组元素的地址,假设e=&a[i],其中,a为一个数组,那么f(e,g,o)=a(i+o),数组的值在前面介绍中使用函数表达.

5. e为一个条件赋值语句的条件表达式,假设e=c?e¢:e²,其中,c不包含间接引用操作符,那么:

f(c?e¢:e²,g,o)=c?f(e¢,gÙc,o):f(e²,gÙØc,o).

6. e为一个指针算术表达式,指针算术表达式是一个指针和一个整数的和,假设e¢为指针部分,i为整数部分,则e=e¢+i.那么f(e¢+i,g,o)=f(e¢,g,o+i).

7. e为一个指针类型强制转换,即e=(Q*)e¢,Q为任意类型,那么f((Q*)e¢,g,o)=(Q)f(e¢,g,o).需要说明的是:在强制转化过程,需要用到SMT模型中的位向量进行建模.例如,对于一个整型变量x,转化为char类型的操作为xÙ(11111111)₂.

8. 在其他情况下是没有意义的,例如,e可能指向一个空(NULL)或者指针没有被初始化.为了保证这种情况不会发生,通过加入断言assert(!r(g))来实现.

我们给出一个例子来说明上述的计算过程,请看下面的一段程序:

int a,b,*p;

if (x) p=&a; else p=&b;

*p=1;

第1条语句被转化为p₁=(x₀?&a:p₀);p₂=(x₀?p₁:&b).间接引用*p可以通过如下的计算被消除:

*p=f(p,true,0)

=f((x₀?p₁:&b),true,0)(因为p₂=(x₀?p₁:&b))

=x₀?f(p₁,x₀,0):f(&b,Øx₀,0)

=x₀?f(p₁,x₀,0):b

=x₀?f(x₀?&a:p₀,x₀,0):b(因为p₁=(x₀?&a:p₀))

=x₀?(x₀?a:f(p₀,false,0)):b

=x₀?a:b.

由此可知:在x₀的情况下,对a赋值为1;在Øx₀的情况下,对b赋值为1.即,a₁=x₀?1:a₀,b₁=Øx₀?1:b₀.

2.2 事件自动机SMT模型转化方法

本节通过引入自动机可达树的概念,给出事件自动机到SMT模型的转化.我们首先介绍一些符号表示,这有利于下面对转化算法的描述:

事件符号表示. 对于一个事件e,它有多个参数,我们用e[i]表示事件的第i个参数,e.name表示事件的名称,e.size表示参数的个数.

单一赋值操作符号表示. 对于一个表达式expr,针对单一赋值形式,我们定义两种操作:

· r(expr)表示结合已有SMT模型将该表达式转化成单一赋值形式;

· 对于一个变量v,我们使用a(v)表示变量v被赋值的次数,每当变量v被赋值一次,a(v)的值加1.

事件自动机符号表示. 对于一个事件自动机EA,假设事件自动机的状态为s₀,s₁,…,s_m,其自动机变量为x₀,x₁,…,x_n.我们给出以下重要的符号表示:

· EA.Var表示事件自动机中变量的集合,即,EA.Var={x₀,x₁,…,x_n}.

· 对于自动机中的每一个状态s_i,与单一赋值形式类似对s_i进行标号,也就是说,当转移到该状态时,该状态的标号加1.s_i,j为s_i的第j个复制,我们称s_i,j为状态变量.

· trans(s_i)表示所有从s_i出发的转移的集合,对于任意tÎtrans(s_i),t.e表示触发该转移的事件,t.guard表示转移发生的条件,t.assigns表示转移的赋值语句的序列,t.start表示转移的起始状态,t.end表示转移的下一个状态.

· EA.s₀为事件自动机的初始状态,EA.F为事件自动机的接受状态集合.

绑定操作符号表示. 一个绑定Bind可以表示为[x₁aexpr₁;x₂aexpr₂;…;x_naexpr_n].我们给出如下操作:

· 变量在绑定中的取值:

· Bindáxavñ:产生一个新的绑定,如果x在Bind中已经赋值,则将v重新绑定到x;否则,将xav加入到绑定中.即

· 对于一个表达式expr,变量xÎexpr表示表达式中存在变量x.将一个绑定作用到该表达式上定义为expr(Bind):"xÎexpr,在表达式expr中,使用Bind(x)代替x.

· 对于一个变量x,xÎBind表示x在Bind中被绑定,xÏBind表示x在Bind中未被绑定.

针对自动机和C语言结合的转化,本文提出一种自动机可达树来描述自动机的所有可能的执行路径,自动机可达树是本文算法的核心概念.

定义7(自动机可达树). 一棵自动机可达树定义在一个事件自动机上,它定义为一个五元组ART=(Nodes,r₀,Edges,leaf,acceptleaf),假设它的事件自动机为EA,其中,

(1) Nodes为可达树中节点的集合,每个节点都由两个部分组成:一部分是状态变量,另一部分是一个绑定.即,n=(s_i,j,Bind),其中,s_i,j为状态变量,Bind为自动机变量的绑定.n.state表示节点的状态变量,n.bind表示节点绑定.对于一个状态变量s_i,j,如果s_iÎEA.F,则表示为s_i,jÎEA.F.

(2) r₀为根节点,它包含初始状态的第0个复制和所有自动机变量初始值的绑定,即

r₀=(s_0,0,[x₀ainitialval₀;…;x_nainitialval_n]).

(3) Edges为可达树的边,对于边(n₁,n₂)ÎEdges,其中,n₁,n₂ÎNodes,n₁=(s_i,j,Bind₁),n₂=(s_k,l,Bind₂),则n₁,n₂满足以下两种情况之一:

1) s_kÎd(s_i),即,存在转移从s_i到s_k;

2) i=k,l>j,Bind₁=Bind₂.

第2种情况是在事件不发生的条件下产生的节点,事件不发生会产生不发生约束,所以这里必须多生成一个子节点,如果事件必然发生,则不生成该节点.

(4) leafÍNodes为自动机可达树的叶子节点集合,叶子节点定义为没有子节点的节点.

(5) acceptleafÍleaf为自动机可达树的接受叶子节点集合,对于一个节点nÎacceptleaf,n.stateÎEA.F.

自动机可达树的构造是在对事件自动机和程序进行转化的过程中进行的,自动机可达树从根节点到接受叶子节点的路径,就是一条事件自动机的接受路径.自动机可达树中所有的节点的状态变量都不重复.

定义8(自动机可达树路径). 自动机可达树的一条路径定义为n₀,…,n_k,其中,n₀=r₀且"0≤i≤k-1,(n_i,n_i+1)Î Edges.如果自动机可达树的一条路径为接受路径,则n_k.stateÎEA.F.自动机可达树的一条接受路径表达了程序中存在的一条错误路径.

图 5给出了图 2中对文件打开和关闭属性描述的一棵自动机可达树实例,左边的路径s_0,0s_1,0s_0,2不是一条可接受路径,而s_0,0s_1,0s_2,0是一条可接受路径,因为最后一个节点为接受叶子节点.节点(s_0,1,[×])为open事件不发生情况下的节点,在编码中会产生不发生事件约束.

下面给出一些关于自动机可达树的符号表示.

自动机可达树符号表示. 对于一棵自动机可达树ART,它的一个节点n的父节点表示为parent(n),该节点的直接子节点集合表示为child(n),该节点的状态变量分量表示为n.state,绑定分量表示为n.bind. ART.root表示可达树的根节点,ART.leaf表示当前所有叶子节点的集合,ART.acceptleaf表示接受叶子节点集合.

在开始算法介绍之前,我们首先介绍一些全局存储变量:

· ART:自动机可达树.

· Model:存储事件自动机和C程序当前已经完成的SMT模型.Model.add(statement)表示增加一条SMT编码.

· EA:对属性进行规约的事件自动机,它的状态集合为{s₀,…,s_m}.

下面给出本文结合C程序SMT模型生成事件自动机SMT模型的算法.

算法执行框架. 输入经过第2.1节步骤2处理过的程序Program={p₁,…,p_n},即,只包含赋值语句、if语句和断言语句,p_i为一条语句.输入一个对该程序属性规约的事件自动机EA.

BuildSMT(Program,EA)

begin

Initial(ART);

for i from 1 to n do

Model.add(translate(p_i));

guard=the execution condition of p_i;

if p_i generates event e then ReceiveEvent(e,guard); endif

endfor

MakeAssertion(×);

end

框架中的Initial(ART),ReceiveEvent(e,guard),MakeAssertion(×)将在下面的算法3、算法6和算法7中描述.上述执行框架首先使用Initial(ART)初始化自动机可达树;然后将程序中的每一条执行语句转化为单一赋值形式,本文使用translate对该语句进行转化,translate为第2.1节中介绍的算法实现,文献^[12,20]中已经给出,本节直接引用.如果该语句的执行会产生事件e,则调用ReceiveEvent(e,guard)生成事件自动机和程序之间约束关系的SMT模型;最后,调用MakeAssertion(×)生成违反事件自动机属性的断言.该算法框架生成的SMT的模型将会使用SMT求解器求解,求解结果使用算法8生成反例路径.

算法2. 事件匹配函数.

对于两个事件e₁和e₂,判断两个事件是否匹配,当接收到匹配的事件,才会触发自动机的迁移.

输入:两个事件e₁和e₂.

输出:如果两个事件匹配,则返回true;否则,返回false.

算法描述:

bool match(e₁,e₂)

begin

if e₁=SÚe₂=S then return true; endif

if e₁.name¹e₂.name then return false; endif

if e₁.size¹e₂.size then return false; endif

for i from 0 to e₁.size-1 do

if the types of e₁[i] and e₂[i] are not same then return false; endif

endfor

return true;

end

上述算法中,类型不一致相当于编译中的类型检测(type checking),因为实参事件的参数类型必须与自动机事件的参数类型一致.算法首先判断事件的名称是否一致,然后判断事件参数个数是否相等,最后判断每一个参数对应的类型是否一致.

算法3. 自动机可达树初始化函数.

输入:自动机可达树ART.

输出:初始化后的自动机可达树ART.

算法描述:

void Initial(ART)

begin

Bind=[×];

for each vÎEA.Var do

v₀=initialvalue; Bindávainitialvalueñ;

endfor

ART.root=(s_0,0,Bind);

end

算法首先对所有自动机变量的第0个复制赋初始值,然后加入到绑定当中,最后将可达树根节点的自动机变量设置为初始状态,根节点的绑定设置为所有自动机变量的初始值.

算法4. 判断一个表达式的值是否为常数.

输入:一个表达式expr,一个变量的引用t,如果在上下文中expr是常数,则将表达式的值赋值给变量t.

输出:布尔值,若为真则表示该表达式为常数;否则,说明该表达式含有不确定值的变量.

算法描述:

bool Constant(expr,&t)

begin

Bind=[×];

for each varÎexpr do

if the value of var is constant val then Bindávaravarñ else return false endif

endfor

t=expr(Bind);

return true;

end

对于一个表达式中的所有变量,如果已有的值为常数,则将这个常数加入到绑定当中;如果不是一个常数,则返回false.最后,将所有变量用它们的常数值代替,可以得到表达式的值,将该值赋值为变量t.例如a=3,表达式a+4的值计算为7.

算法5. 当产生事件e,并且匹配自动机转移的事件t.e的编码.

输入:程序产生的事件e,节点n为可达树的一个非接受叶子节点,该节点为准备扩展的节点,t为可以发生的转移,n的状态变量为t.start.j为该事件发生的上下文条件与n.state=true的合取.这里,前置条件为e,与t.e是匹配的.

输出:新的SMT模型Model.

算法描述:

void codeTran(e,t,n,j)

begin

Bind=n.bind;

for i from 0 to e.size-1 do

if t.e[i]ÎVar then

if Constant(e[i],c) then Bindát.e[i]acñ; continue; endif

Model.add(t.e[i]_a(t.e[i])+1=r(e[i]));

a(t.e[i])=a(t.e[i])+1;

Bindát.e[i]at.e[i]_a(t.e[i])ñ;

endif

endfor

guard=jÙt.guard(Bind);

Model.add(t.end_a(t.end)+1=guard?true:false);

a(t.end)=a(t.end)+1;

for each (v=expr)Ît.assigns do

if Constant(expr,c) then Bindávacñ; continue; endif

Model.add(v_a(v)+1=r(expr));

a(v)=a(v)+1;

Bindávav_a(v)ñ;

endfor

n.addChild(t.end_a(t.end),Bind);

if guard is not always true then

Model.add(t.start_a(t.start)+1=((n.state=true)Ùt.end_a(t.end)=false)?true:false);

a(t.start)=a(t.start)+1;

n.addChild(t.start_a(t.start),n.bind);

endif

end

该算法描述了对一个转移的编码,当产生一个实参事件时,首先判断实参事件中参数是否为一个常数:如果为一个常数,则直接绑定,不生成SMT模型;否则,将转移t上的事件参数生成一条赋值约束,并加入到绑定Bind当中.然后处理转移条件t.guard,算法中的变量guard是jÙt.guard(Bind),也就是说,只有当转移的条件也被满足之后才可以转移到下一个状态,然后对转移的下一个状态产生一个新的状态变量,新的状态的变量标号为a(t.end)+1,也即该状态的第a(t.end)+1个复制.然后处理转移中的赋值语句,将所有的赋值语句转化为单一赋值形式.最后,我们更新自动机可达树,在自动机可达树的节点n上增加一个子节点.

另外,最后要判断算法中的变量guard在上下文中是否永真:如果永真,则说明该转移必然会发生;否则,就需要考虑不发生的情况.在不发生的情况下,需要增加一个状态赋值约束,就是节点n的状态被复制到其子节点,并且这是在事件不发生的情况下才有的操作,所以它的条件是t.end为false且n.state为true.子节点的绑定为节点n的绑定,最后把状态和绑定加入到n的子节点中.

算法6. 接收事件.

输入:事件e,j为该事件可以发生的条件,也就是一个谓词表达式.

输出:新SMT模型Model.

算法描述:

void ReceiveEvent(e,j)

begin

for each nÎART.leaf-ART.acceptleaf do

for each tÎtrans(n.state) do

if match(t.e,e) then

guard=jÙ(n.state=true);

codeTran(e,t,n,guard);

endif

endfor

endfor

end

算法6给出了当产生一个事件之后的编码,当该事件和转移的事件能够相互匹配时,转移可以发生.首先生成事件发生和当前节点状态变量为真的条件,用变量guard表示,最后调用codeTran对该转移和事件进行编码.

算法7. 生成SMT模型的断言.

输入:自动机可达树.

输出:增加断言的SMT模型Model.

算法描述:

void MakeAssertion(×)

begin

formula f=false;

for each nÎART.acceptleaf do

f=fÚn.state

endfor

Model.add(assert(f));

end

算法7是在C程序和自动机两者的SMT模型都生成完毕之后,最后加入断言.如果模型满足断言,则说明我们找到了一条错误路径.

2.3 反例路径生成算法

我们使用Yices^[29,30]对SMT模型进行判定.Yices将会对模型中的所有未初始化的变量或被赋值为非确定值的变量给定一个确定值,根据所有变量的初始值确定程序执行的路径和事件自动机的接受路径.反例路径算法将生成两个路径队列:(1) 一个队列给出事件自动机的一条接受路径;(2) 另外一个队列给出C程序中反例的执行路径.下面给出反例路径算法所使用的符号表示:

· K表示所有变量的当前值的绑定,包括C程序的变量、自动机状态变量和自动机变量.

· 事件自动机和C程序的SMT模型定义为Z={z₁,z₂,…,z_n},其中,z_i为一条SMT模型语句.

· C程序定义为一系列语句的集合C={c₁,c₂,…,c_m},c_i是C程序中的赋值语句和条件语句等.给出一个映射f:Z®CÈ{e},其中,e表示对于一条SMT模型语句在C程序中不存在一条语句与之对应.在第2.1节介绍的C程序到SMT模型转化的过程中,每转化一条C语句,建立一个f的映射绑定.

· Q={s₀,s₁,…,s_k}为事件自动机状态的集合,给出一个映射g:Z®QÈ{e},其中,e表示对于一条SMT模型语句在一个事件自动机中不存在一个状态与之对应.在第2.2节事件自动机转化为SMT模型的过程中,每生成一个可达树节点,建立一个g的映射绑定.

· 给定两个队列que_C和que_Q,que_C存储C程序中错误路径,que_Q存储事件自动机的一条接受路径.对于一个队列有两种操作:queue.inqueue(e)在队列末尾中插入一个元素,queue.dequeue(e)在队列的头部删除一个元素并将值赋值给e.

算法8. 反例路径生成算法.

输入:K为所有变量的当前赋值绑定,i为当前的语句标号,语句标号从1开始一直到SMT模型结束.

输出:打印反例路径.

算法描述:

void FindCounterExample(K,i)

begin

(a):

if z_i is in form [v_i=c?e₁:e₂] then

if c(K)=false then FindCounterExample(K,i+1) return;

else Kávae₁(K)ñ

endif

endif

(b):

if z_i is in form [v_i=e₁] then Kávae₁(K)ñ endif

(c):

if f(z_i)¹e then que_C.inqueue(f(z_i)); PTINT(f(z_i)); endif

(d):

if g(z_i)¹e then que_Q.inqueue(g(z_i)); PTINT(g(z_i)); endif

FindCounterExample(K,i+1);

end

算法中,c(K)=false表示用绑定中变量的值代替表达式c中的变量,然后判断c为真或假.标号(a)表示对于一条SMT模型语句,如果它是一个条件赋值,且当前所有变量绑定的值不能够满足条件c,则该条语句在C程序或事件自动机中没有被执行,直接进入下一条语句;如果满足,则更新绑定K中变量的值.标号(b)表示一条简单赋值语句,更新绑定K中变量的值.标号(c)表示当SMT模型语句对应的是一条C程序语句,则将对应的C程序语句加入到队列que_C中.标号(d)表示当SMT模型语句对应的是一个自动机状态时,则将该自动机状态加入到队列que_Q中.程序最后将新的变量绑定值传递到下一条语句来处理.

我们通过调用FindCounterExample(K,1)就可以打印程序中存在的错误路径,z₁为SMT模型的第1条语句.上述算法将会打印一条C程序的执行路径,并且当某条语句产生一个事件的时候,会打印出事件自动机发生转移的状态.两个队列que_C和que_Q则分别保存了C程序的反例路径和事件自动机的一条接受路径.

3 实例分析 3.1 实例1:lock和unlock属性验证

首先,我们学习CBMC主页的一个示例程序,参见文献^[31].如图 6所示的一段C语言程序,它定义了两个函数:lock(×)和unlock(×).程序中的定义_Bool nondet_bool(×)表示该函数不确定返回布尔类型的值,这是CBMC的函数库所定义的,而且不需要函数体.当nondet_bool(×)返回true时加锁,设置LOCK=1,否则不进行加锁操作. unlock(×)是开锁操作,直接设置LOCK=0.main是对两个函数的使用.我们现在要规约对程序的所有执行路径开锁操作的前提是已经上锁.

图 7给出事件自动机在所有未加锁的情况下执行了解锁操作路径的规约,该自动机有3个状态:s₀为自动机初始状态,s₁为已加锁状态,s₂为接受状态.也就是说,当程序进入该状态时,说明已经找到一条违反该属性的执行路径.

对已有的C语言程序和事件自动机,执行本文的转化算法可以得到一个SMT模型,保存在文件case1.ys.转化的SMT模型可以在网上下载(本文实例1和实例2的SMT模型可以通过http://www.kuaipan.cn/file/id_218529353359693077.htm?source=1下载),我们首先把main中的while循环展开1次,然后转化为SMT模型.使用SMT求解器Yices进行判定,执行命令yices -e case1.ys返回unsat,即,没有发现错误.然后,我们将循环展开2次,重新生成SMT模型,使用Yices对SMT模型重新进行判定,得到分析的结果为sat,如图 8所示.判断结果是SMT模型可满足,即存在一条执行路径使事件自动机到达接受状态,程序中存在错误.根据Yices所提供的反例可知,在t₁=false,t₀=false,times₀=2的情况下程序出现错误.程序在循环展开2次的情况下,t₀代表第1次执行lock操作时不确定选择为false,即程序没有选择加锁.t₁代表第2次执行lock操作时不确定选择也为false. times₀确定循环展开了两次.所以,反例就是在循环的两次执行中lock操作选择不加锁的情况下产生.

出错的原因:程序第1次没有加锁的时候,unlock也不会执行,但是get_lock会减1;又因为get_lock的初始值为0,减1会出现溢出问题,get_lock不再为0;在第2次循环执行的情况下,依然没有执行加锁操作,但是因为get_lock¹0,所以进行解锁操作.也就是程序从状态s₀进入状态s₂,从而找到一条反例路径.由此可以看出:SMT对变量的取值范围的解释和C程序中的一致,也就是说,本文方法可以检测变量的溢出等比较底层的逻辑错误.

3.2 实例2:队列FIFO属性验证

图 9给出了一段队列操作的代码,参考文献^[20]中的一段程序.它定义了插入操作、删除操作,队列我们用结构体来定义.队列的定义中,nelem表示当前队列保存的数据个数,head和tail分别代表队列的头部和尾部,buffer存放队列中的数据.队列的插入操作是在队列的队尾插入,删除操作是队列的头部删除,队列的实现是循环队列.在代码中加入生成事件的注释,看出我们只有在真正将数据插入到队列中才会产生事件,如果队列是满的,则不会产生插入事件.同理,删除操作中,只有当队列非空才会产生删除事件,删除的数据被保存在变量res中.队列插入的数据使用随机函数生成.本文使用图 3中对队列先进先出属性的规约验证这段程序的所有执行路径是否符合先进先出的规则.

使用本文转化到SMT模型的算法,可以得到转化后的模型case2.ys.这里,在程序中有两个循环,他们循环的次数都是2,所以该程序不需要设定循环上界.使用工具Yices对该模型进行判定yices -e case2.ys,得到判定结果如图 10所示.结果为unsat,也就是SMT模型无法满足,程序的所有路径都不会进入图 3所规约的事件自动机的接受状态,该段代码在图 3的事件自动机下是正确的.图 11是该段程序验证过程中生成的自动机可达树,表 1存放的是自动机可达树每个节点的详细信息.自动机可达树中所有的接受叶子节点中状态变量都为false,也就是在实际的执行路径中无法到达该节点.

3.3 性能分析

本节对事件自动机模型检测算法的性能进行评估.有界模型检测的效率与循环和递归的展开有密切的关系,因为:(1) 循环和递归展开会使代码量激增;(2) 代码的增加会导致变量复制的增加.本节的实验基于第3.2节中队列先进先出的实例,将图 9中第38行和第40行的循环改为for (i=0;i<M;i++).M从50开始每次增加50次,记录每次运行的时间和内存.

为了形成对比效果,本文使用文献^[20]中的方法,通过加入断言的形式来验证第3.2节中图 9的代码.这里必须要说明的是:图 9中的代码是无法通过加入断言来验证FIFO属性的,因为无法知道第i次插入队列中的数据是多少,这也是事件自动机表达能力上的体现.为了能够使用断言表达,修改图 9中第39行的代码为insert(i);并在第41行代码之后加入断言assert(res=i).这样确定了第i次插入队列中的数据是i,所以第i次删除的数据也是i.实验硬件条件为Intel® Pentium® CPU P6200处理器和2G内存.

实验结果如图 12和图 13所示,其中,SMT-ASSERT表示使用断言规约的FIFO属性验证,SMT-EA表示使用事件自动机规约的FIFO属性验证.从图中可以得出如下结论:

(1) SMT-ASSERT验证的最大循环次数为750,当循环次数超过750时,Yices求解器无法给出结果(Yices求解器返回3类结果:sat,unsat,unknown),SMT-EA验证的最大循环次数为900.所以,图中实线的最大循环次数达到750,虚线的最大循环次数达到900.

(2) SMT-EA的运行时间要优于SMT-ASSERT,SMT-ASSERT在每次进行删除的时候都加入断言,断言不提供上下文信息,SMT-EA的自动机可达树会记录路径的信息.

(3) SMT-ASSERT使用的内存要远小于SMT-EA,这是因为SMT-ASSERT在每次执行队列删除的操作时只需加入一个断言即可,而SMT-EA则需要记录事件自动机的所有可能的执行情况,也就是说,自动机可达树会不断增大.这是事件自动机在表达能力上增强的后果.

综上所述,实验中,SMT-EA在最大验证循环次数和验证的时间上要优于SMT-ASSERT,SMT-ASSERT所用的内存要少于SMT-EA.这里需要说明的是:有界模型检测对验证规模的评估不能使用代码行数,而应该是程序执行的路径长度.例如图 9中的程序,SMT-EA验证900次的insert和delete操作,insert和delete操作展开的步数为6,那么验证的程序执行最长路径长度为5 400步.

4 总结与下一步工作

本文针对已有的C语言形式化验证工具中对属性描述表达力不够丰富、属性与程序不分离和缺乏对事件的表达等缺点,提出使用事件自动机对程序属性进行规约,给出从C程序生成事件的方法.在有界模型检测方法的基础上,结合本文提出的自动机可达树,给出了从事件自动机到SMT模型的转化方法和建立反例路径的算法.实例分析表明:事件自动机可以有效地表达现有的C语言形式化验证工具中无法表达的属性,且可以描述软件中与事件相关的安全属性.基于SMT求解器的模型检测算法提高了算法的执行效率,且与C程序中数据类型的语义相符.因此,本文所提出的方法适合基于事件自动机属性描述的C程序形式化验证.由实验分析可知,本文方法所消耗的内存较多.因此,研究自动机可达树的约简技术,将作为本文的下一步工作.另外,本文没有给出并发程序验证的算法,这部分工作将在未来展开.

致谢 感谢审稿专家提出的宝贵意见和建议,并向对本文工作给予支持和建议的同行表示感谢.