基于抽象不变式的程序安全性验证
张 1,2 , 钱俊彦 3 , 李舟军 1 , 马殿富 1     
1. 北京航空航天大学 计算机学院, 北京 100085 ;
2. 湖北大学 计算机与信息工程学院, 武汉 430062 ;
3. 桂林电子科技大学 计算机科学学院, 桂林 541004
摘要:程序安全性验证是软件系统安全领域的研究难点,构造程序不变式是程序安全性验证的主要方法之一。验证程序是否满足时态性质的问题可转化为不动点求解问题,然而直接构造不动点的求解算法是非常困难的。该文探讨了一类基于抽象解释框架的不变式求解构造方法。首先通过Tableau方法构造时态公式的谓词图,基于传统不变式构造规则,使用前向或逆向状态转换,改进不变式验证规则;然后采用抽象解释框架构造抽象状态转换系统,给出了抽象不变式验证规则;最后基于不动点抽象定理,通过前向或逆向转换求解近似的不动点,使用加宽近似和收窄近似操作进一步加速收敛,从而给出基于抽象不动点的不变式验证算法,最终完成了基于抽象不变式的程序安全性自动验证。
关键词抽象解释     不变式验证     不动点     程序安全性验证    
Program security verification based on abstract invariants
ZHANG Yan1,2 , QIAN Junyan3 , LI Zhoujun1 , MA Dianfu1     
1. School of Computer Science and Engineering, BeiHang University, Beijing 100085, China ;
2. School of Computer Science and Information Engineering, Hubei University, Wuhan 430062, China ;
3. Department of Computer science and Engineering, Guilin University of Electronic Technology, Guilin 541004, China
Abstract:Program security verification is a difficult issue with program invariants used for program security verification. Verification of whether a program has the correct temporal nature is converted into a problem solved at a fixed point. However, directly constructing an algorithm to solve the fixed point problem is very difficult. This paper presents a class of invariant construction methods based on an abstract interpretation framework to solve the structure method. Firstly, the Tableau method is used to construct the figure of the temporal formula based on the traditional invariant structure rules, with forward or backward state transitions to improve the invariant validation rules. Secondly, this paper presents an abstract state transition system based on an abstract interpretation framework and gives the abstract invariants validation rules. Finally, the fixed point theorem of abstract invariants is used with the forward or reverse transformations to solve the approximate fixed point in an automatic validation method based on abstract invariants of the program. Approximate widening and narrowing operations based on the abstract fixed point invariant verification algorithm accelerate the convergence.
Key words: abstraction interpretation     invariant verification     fixed point     program security verification    

随着抽象解释与模型检验等技术的发展,一些研究人员把此类技术与程序不变式验证相结合,研究不变式的自动验证[1-5]问题。 假定程序为Pr,其模型为M,所验证性质用谓词p描述,p可表示状态集合、迹集合或树集合等,验证M $\vDash $p,则pM的不变式。 不变式验证可归纳为不动点检验问题: 假定状态转换关系R、 前向转换函数post、 初始状态集I和状态集PP是谓词p的状态集表示,可达状态集∪i≥0post[Ri](I)是P的子集,当且仅当P是程序Pr的不变式。 然而直接计算不动点是非常困难的,故不变式验证[6]通常依赖找到适合的辅助不变式Q,使之满足∪i≥0post[Ri](I)⊆QP。 当系统状态空间无限或规模太大时,计算不动点变得不可行,为了有效计算不动点,常把系统抽象为有限状态转换系统或满足不动点计算的近似模型。

为了验证不变式,首先需要构造一阶前提,然后采用辅助不变式来验证,从而避免直接计算不动点[7-8]。 获取不变式有两种完备的方法: 一种是自底向上,从初始状态通过前向转换生成辅助不变式; 另一种是自顶而下,从待验证不变式通过逆向转换获取优于系统给定的性质。

通常抽象主要有抽象解释[9]和模拟[10]两种方法。 假定在抽象和具体状态系统中有模拟关系ρ,可通过Galois连接(post[ρ],pre[ρ])构造抽象解释框架。 2007年Cousot等[11]给出了基于不动点导向的抽象精化算法CGR。 Ranzato[12] 于2008年改进了CGR算法,给出了一个双向传播的抽象精化算法。 2010年Gantya等[13]针对交换自动机,提出了基于不动点导向的抽象精化算法。 文[14-15]给出了线程模块的抽象精化算法。 Bensalem等[16]在2003年给出了不变式的谓词抽象规则,Gulwani等[17]在2009年提出基于谓词抽象对不变式规则进行约束。

本文首先提出基于不变式的验证规则,通过Tableau方法构造所验证时态公式的谓词图,采用状态前向或逆向转换,基于抽象解释框架,通过模拟构造抽象状态转换系统,给出了不变式验证的抽象规则。 然后把不动点搜索约束到抽象域中,通过不动点抽象定理,利用前向或逆向转换求解近似的不动点,并使用加宽近似和收窄近似操作加速收敛,最后给出了基于抽象不动点的不变式验证算法。

1 基础知识 1.1 转换系统

为了形式化描述软硬件系统的状态迁移,通常采用状态转换系统来描述。

定义1 (状态转换系统)状态转换系统是一个 五元组M =(Σ,I,R,err,F),其中Σ 为状态集,I ⊆ Σ 为初始状态集,RΣ ´Σ 表示状态转换关系,err ⊆Σ 为错误状态集,FΣ 为终止状态集.

假定程序语言L,Pr∈L为任意程序,函数 R[Pr]映射Pr到状态转换关系,同理可得Σ[Pr]、 I[Pr]、 err[Pr]、 F[Pr]。

为了方便描述,本文采用小写字母表示谓词,对应的大写字母或符号 表示状态集,例如p为谓词,Pp表示状态集。 当描述具体程序时,假定V是程序变量有限集,包括数据变量、控制变量和辅助变量,Σ表示V上的状态集,初始条件I可用V上一阶谓词描述,转换关系tR映射每个状态 sΣs后继状态集t(s)⊆Σ,且转换关系t可用谓词ρt($\bar{x},\bar{x}'$)表示,其中x表示状态s上的变量值,x′表示后继状态s′∈t(s)的值。 如果t(s)={s},那么t是空转换。

给定Σ,其幂集为(Σ),转换关系的逆向或前向转换函数及其对偶函数定义如下:

$\begin{align} & pre\left[ R \right]\left( X \right)\triangleq \left\{ s\left| \exists v.\left( s,v \right)\in R\wedge v\in X \right. \right\}, \\ & \widetilde{pre}\left[ R \right]\left( X \right)\triangleq C\circ pre\left[ t \right]\circ C= \\ & \left\{ s\left| \forall \right.v.\left( s,v \right)\in R\Rightarrow v\in X \right\}, \\ & post\left[ R \right]\left( X \right)\triangleq \left\{ v\left| \exists s.s\in X\wedge \left( s,v \right)\in R \right. \right\}, \\ & \widetilde{post}\left[ R \right]\left( X \right)=C\circ post\left[ t \right]\circ C= \\ & \left\{ v\left| \forall \right.s.\left( s,v \right)\in R\Rightarrow s\in X \right\}. \\ \end{align}$

直观地,前向转换post[R](X)表示状态集X的后继集合∪sXR(s),逆向转换pre[R](X)表示状态X的前趋集合。 pre[R](X)的状态集合是指如果集合中的状态存在前向转换,则其后继状态一定在X中。 post[R](X)的状态集合是指如果通过转换能从其他状态一步到达,则其前趋状态一定在X中。 给定有限转换集TR,则对于状态集X,通过转换关系T的逆向和前向转换表示为

$\begin{align} & pre\left[ T \right]\left( X \right)\triangleq {{\cap }_{t\in T}}pre\left[ t \right]\left( X \right), \\ & post\left[ T \right]\left( Y \right)\triangleq {{\cap }_{t\in T}}post\left[ t \right]\left( t \right), \\ \end{align}$

且有

$X\subseteq pre\left[ T \right]\Leftrightarrow post\left[ T \right]\left( X \right)\subseteq X.$
1.2 不变式验证

给定谓词p,若pM的不变式,则M $\vDash $p,可用规则INV验证。 规则INV如图 1所示:

图 1 规则INV

此规则前提I1I3是安全的,且是相对完备的。 因为规则INV中没有描述如何寻找辅助谓词q的方法,所以使用规则INV去验证程序的最大困难是如何找到辅助谓词q。 给定转换系统M和谓词p,把M$\vDash $p问题转化为一阶公式的前提条件,以此证明pM中是可满足的。 然而,为了使用规则INV去验证不变式,不得不去寻找一个相对于p更优的辅助谓词q,使一阶命题I1I3在M状态中满足。 故不变式验证中,主要难点是如何找到谓词q,满足Reach(M)⊆ qp。 事实上,Reach(M)是系统M的最小归纳不变式,然而通过不动点计算Reach(M)是非常困难的,且不能保证收敛。

对于前提I3,则可进行重新定义,形如{φ}R{ψ }$\triangleq $tR{φ}t{ψ},并对每个验证条件{φ}t{ψ}能等价表示为

1) 标准的表示方法: φ∪ ∪{s′|(s,s′)∈t∧s ∈φ} ⊆ψ

2) 基于逆向转换的表示方法: $\bar{x}$.φ⊆ pre[t](ψ);

3) 基于前向转换的表示方法: $\bar{x}'$. [post[t](φ)⊆ψ.

1.3 可达性与不动点

假定〈L,⊑,⊥,丅,∪,∩〉是完备格,对于函数f:L→L用上标向上箭头↑和向下箭头↓分别表示升函数和单调降函数。 通过Knaster-Tarski定理,最小不动点描述为

$lf{{p}^{\sqsubseteq }}f=\left\{ \bigcap \left\{ x\in L\left| f\left( x \right)\subseteq x \right. \right\} \right.={{\bigcup }_{n\in \mathbb{N}}}{{f}^{n,\uparrow }}\left( \bot \right).$

其中迭代序列{fn,↑(x)} n$\mathbb{N}$递归定义如下:

1) n=0,f0,↑(x)=x

2) 后继序数n+1,fn+1,↑(x)=f(fn,↑(x));

3) 有限序数n,fn,↑(x)=Ui<nfi,↑(x) .

类似地,最大不动点为

$gf{{p}^{\sqsubseteq }}f=\bigcup \left\{ x\in L\left| x\subseteq f\left( x \right) \right. \right\}={{\supset }_{n\in \mathbb{N}}}{{f}^{n,\downarrow }}\left( \text{T} \right)$

R*=∪i≥0Ri (其中R0$\triangleq ${(s,s)|sΣ},且Rn+1$\triangleq $R$\circ $Rn= Rn$\circ $R)是二元关系R传递的、自反的闭包,则post[R*]I=lfpIλX.X ∪ post[R](X)=lfpλX.I ∪ post[R](X)。 通过不动点定理,lfpI λX.X ∪ post[R](X)求解如下: lfpI λX.X ∪ post[R](X)=∪i≥0Xi,其中X0=I,Xi+1= Xi ∪post[R](X)。

假定转换系统M=(Σ,I,R,err,F),状态集 PΣ,Reach(M)表示系统M的可达状态集,即Reach(M)$\triangleq $post[R*]I。 如果Reach(M)⊆PP包含M的每个可达状态,则称P是M的不变式,表示为M$\vDash $P。 故不变式验证问题可转换状态可达性问题,描述为post[R*]IP,或归纳为不动点检验问题。

2 基于谓词图的不变式验证

本节采用谓词图的方式描述时态公式p。假设p是一个有约束的路径公式,因其他时态算子可用X和U描述,故本文仅考虑时态算子XU。例如Ff表示True Uf,Gf表示ㄱFff1Rf2则表示ㄱ[ㄱf1Uㄱf2]。

2.1 谓词图

程序的运行迹σΣ∞可用非空有限状态序列或无限状态序列σ0,σ1,…σi,…表示,其中σiσ,运行迹开始于初始状态σ0I,状态σi通过转换关系 tR 与后继状态σi+1相关联,即(σi,σi+1)∈t。 序列σ=σ0,σ1,…σi,…σn是有限的(长度|σ|=n+1)当且仅当最后状态是终止状态(σnF)或是错误状态(σnE)。

谓词图G=〈N,N0,E,λ〉是一个标签有向图,其中N表示结点集合,N0N表示初始结点集,EN×N 表示边,λ:N×A表示从结点到谓词的映射。 如果G能精确描述p的模型,则Gp 的谓词图,也就是对每条计算迹σs0,s1,s2,…,〈σ,0〉$\vDash $p当且仅当在G中,对i≥0,存在路径n0,n1,…,满足si$\vDash $λ(ni)。

给定公式φ,其闭包cl(φ)形式化表述如下:

1) ㄱf1∈cl(φ) 当且仅当 f1∈cl(φ);

2) 如果f1f2∈cl(φ),那么f1,f2∈cl(φ);

3) 如果X f1∈cl(φ),那么f1∈cl(φ);

4) 如果ㄱX f1∈cl(φ),那么Xf1∈cl(φ);

5) 如果f1 U f2∈cl(φ),那么f1,f2,X [f1 U f2]∈cl(φ).

根据以上表述,pUq的闭包cl(pUq)={p,q,ㄱp,ㄱq,pUq,X[pUq]}.

下面采用Tableau算法直接构造公式的谓词图。 G=〈N,N0,E,λ〉有如下组成:

1) N⊆2cl(φ)(nN)当且仅当

a) φn

b) 对任何f∈cl(φ),fn当且仅当ㄱfn

c) 对任何f1f2∈cl(φ),f1f2n当且仅当f1nf2n

d) 对任何ㄱX f1∈cl(φ),ㄱX f1n当且仅当Xf1n

e) 对任何f1Uf2∈cl(φ),f1Uf2n,那么f1,X [f1Uf2]∈nf2n

2) N0N (nN0) 当且仅当φn

3) (n1,n2) ∈E当且仅当

a) 对任意X f1∈cl(φ),X f1n1当且仅当f1n2

b) 对任意f1Uf2∈ cl(φ),f1Uf2n1当且仅当f2n1f1Uf2n2

4) λ(n)=∧{ fn|f是一阶公式}。

对于结点nN,如果在S中的每个有限计算迹s0,s1,…,sk和在G中的每条路径n0,n1,…,nk满足si$\vDash $λ(ni),其中s=sk,n0N0,n=nk,那么状态s是(S,n)-可访问的。如果对S中的每个状态都满足,那么谓词φ是(S,n)-有效状态。

验证规则SAFE把规则INV的I1I3转化为一阶前提S1S3,如图 2所示。 假定转换系统为S,谓词安全公式为p,及其谓词图为G,为了获得p-有效状态,那么只要找到辅助谓词集{φn}nN,使之令S1是S-有效状态,而对结点nNS2S3是(S,n)-有效状态。

图 2 规则SAFE

定理1 规则SAFE是安全的。

证明: 假定规则SAFE的S1S3是满足的,需证明p是S-有效状态,考虑S的任意计算序列σs0,s1,…,也就是s0$\vDash $I且∀i≥0,∃tR. (si,si+1)$\vDash $ρt($\bar{x},\bar{x}'$). 通过前提S1,nN0,s0$\vDash $φn,通过归纳,能得i≥0,nN,si, φn。 因此通过前提S2σ导出一条G中的路径n0,n1,…,满足si$\vDash $λ(ni). 并依据S3,有∀i≥0,∃nN,[si,φn×m,(n,m)Esi+1$\vDash $φm]。 证毕。

2.2 基于前向转换

通常规则SAFE无法确定唯一的最小辅助谓词集,因此不能通过前向转换的不动点找到可能最优的辅助谓词。 为了获得辅助谓词集,可采用更优化的规则Strong-SAFE,如图 3所示。

图 3 规则Strong-SAFE

规则Strong-SAFE的S1aS1b是对规则SAFE前提S1的强化,类似地,S3aS3b是对规则SAFE前提S3的强化。 根据此规则,谓词图G能寻找到唯一的辅助谓词集。

定理2 若辅助谓词集满足Strong-SAFE规则的前提,那么同样满足SAFE规则的前提。

证明: 假定G是谓词图,S1aS1b蕴含S1,S3aS3b蕴含S3,有

$\begin{align} & post\left[ R \right]\left( \left[\!\left[ {{\varphi }_{n}} \right]\!\right] \right)\subseteq {{\bigcup }_{\left( n,m \right)\in E}}\left[\!\left[ \lambda \left( m \right) \right]\!\right]\subseteq \\ & {{\bigcup }_{\left( n,m \right)\in E}}\left\{ post\left[ R \right]\left( \left[\!\left[ {{\varphi }_{n}} \right]\!\right] \right)\cap \left[\!\left[ \lambda \left( m \right) \right]\!\right] \right\}\subseteq \\ & {{\bigcup }_{\left( n,m \right)\in E}}\left[\!\left[ {{\varphi }_{m}} \right]\!\right] \\ \end{align}$

推论1  规则Strong-SAFE是安全的。 证明过程与定理1类似。

与规则SAFE不同,规则Strong-SAFE存在唯一的辅助谓词最小集。 其最小集可用单调算子 F[R]IN: Σ|N|Σ|N|的逐点计算不动点获得,对于nN,算子F[R]In定义如下:

$\begin{align} & F\left[ R \right]{{I}_{n}}\left( \left[\!\left[ {{\varphi }_{n}} \right]\!\right] \right)\triangleq \left[ \left( I\cap {{\left[\!\left[ n \right]\!\right]}_{n\in {{N}_{0}}}} \right) \right.\cup \\ & \left. {{\bigcup }_{\left( n,m \right)\in E}}\left\{ post\left[ R \right]\left( \left[\!\left[ {{\varphi }_{m}} \right]\!\right] \right) \right\} \right]\cap \left[\!\left[ \lambda \left( n \right) \right]\!\right]. \\ \end{align}$

注意[φn]满足F[R]In(φn)⊆φn,当且仅当φn满足S1aS3a. 如果序列(F)n∈N,F[R]IN((F)n∈N),F[R]I2N((F)n∈N),…有限步收敛于[φF,N],那么[φF,N]是F[R]IN的最小不动点。

定理3 [φF,N]满足S1bS3b,当且仅当存在一个满足规则Strong-SAFE前提的谓词集φF,N表示(S,n)-可访问状态。

证明:因为[φF,N]=F[R]In([φF,N])且F[R]In([φN]) ⊆λ(n),[φF],N满足S2。通过观察,φF,N满足S1aS3a,如果S1bS3b进一步满足,那么φF,N满足S1a-S3b

假定[φN]满足S1a-S3b,则∀nN,F[R]·In([φN]) ⊆[φN]。由于[φF,N]是F[R]IN的最小不动点,对n∈N有[φF,N]⊆[φn]。则nN,post[R]·I([φF,N]) ⊆post[R]I([φn]) ⊆∪(n,m)∈Eλ(m),故[φF,N]满足S3b。证毕。

2.3 基于逆向转换

对于逆向转换,因S2S3存在最大解,故相对简单一些。B[R]PN: Σ|N|Σ|N|通过逐点定义如下:

$\begin{align} & B\left[ R \right]{{P}_{n}}\left( {{\varphi }_{N}} \right)\triangleq \left[\!\left[ \lambda \left( n \right) \right]\!\right]\cap \\ & {{\bigcup }_{\left( n,m \right)\in E}}\left\{ pre\left[ R \right]\left( \left[\!\left[ {{\varphi }_{m}} \right]\!\right] \right) \right\},n\in N. \\ \end{align}$

对于nN,满足[φn]⊆ B[R]Pn([φN]),当且仅当状态集[φN]满足S2S3。如果序列(T)n∈N,B[R]PN((T)n∈N),B[R]P2N((T)n∈N),…有限步收敛于最大不动点[φB,N],φB,N表示满足S2S3的状态s,任何从s开始的状态序列Σs0=s,s1,…,∀i≥0,si+1∈t(si),G中存在从n开始的路径n0 = n,n1,…,i≥0,si$\vDash $λ(ni)。

I⊆∪nN0[φB,n],当且仅当p是状态有效的。从上向下验证p是状态有效的步骤如下:生成最大不动点,检查I⊆∪n∈N0[φB,n]是否满足。

3 状态系统抽象转换 3.1 抽象解释

抽象解释是一个通用的语义近似理论框架。 用于证明程序分析器相对于某种形式语义的正确性[18]。 其基本思想是: 程序分析的过程可视为把程序的精确或具体语义性质映射为近似或抽象语义性质的过程,其中抽象语义把隐含在具体语义中的特定结构信息显示出来。 抽象解释的重要性在于,它不仅提供了程序分析器正确性的证明,而且提供了从具体语义系统地获取抽象语义的方法,并使获取抽象语义的过程有可能由计算机辅助实现。

在抽象解释理论中,抽象通过Galois连接〈L,⊑〉$\underset{\gamma }{\overset{\alpha }{\longleftrightarrow}}$L#,⊑#〉或(L,α,γ,L#)来描述,其中L表示具体域,L#表示抽象域,α: LL#是抽象映射,而γ: L#L是具体化映射,满足∀xL,∀yL#,α(x)# yy⊑γ(x).f:L L 表示在具体 语义规约中任何语义函数,f# :L#L# 表示抽象 语义函数.如果α$\circ $f⊑f#$\circ $α,则<L# ,f# >为安全 的抽象,或者说f#f 相对于L# 的正确近似.当 α$\circ $ff#$\circ $αα$\circ $f $\circ $γf# ,则f 存在相对于抽象 域L# 最正确的近似fbα$\circ $f $\circ $γ.

定理4 假定〈L,⊑,⊥,丅,∪,∩〉和〈L#,⊑#,⊥#,丅#,∪#,∩#〉是完备格,f: LL是单调函数,〈L,⊑〉$\underset{\gamma }{\overset{\alpha }{\longleftrightarrow}}$L#,⊑#〉是一个Galois连接,则α(lfp⊑f)⊑#lfp#α $\circ $f $\circ $γ

定理5  假定〈L#,⊑#,⊥#,丅#,∪#,∩#〉是完备格,f#,${\bar{f}}$#:L#L#是单调函数,且f#$\sqsubseteq $# ${\bar{f}}$#,那么lfp# f#$\sqsubseteq $#lfp#${\bar{f}}$#

3.2 构造抽象转换系统

给定具体转换系统M=(Σ,I,R)和抽象转换系统M=(Σ#,I#,R#),((Σ),α,γ,(Σ#))为 Galois 连接,其中(Σ)为具体域,(Σ#)为抽象域,α: (Σ) → (Σ#)为抽象映射,γ: (Σ#) →(Σ)为具体化映射,满足满足∀x∈(Σ),∀y∈(Σ#),α(x)#y ⇔y⊑γ(x),则存在唯一的模拟关系ρΣ×Σ# ,且ργ$\circ $α

定义2 给定具体转换系统M=(Σ,I,R)和抽象转换系统M=(Σ#,I#,R#),M#M关于映射ρ的抽象,表示为M⊑ρM#,需满足如下条件:

1) ρM上的全映射;

2) 对任何状态s0,s1Σ且s0#Σ#,(s0,s0#)∈ρ,如果存在(s0,s1)∈R,那么存在状态s1#Σ#满足(s0#,s1#)∈R#且(s1,s1#)∈ρ;

3) 对在I中状态s,在I#中存在s#满足(s,s#)∈ρ.

容易看出,给定M⊑ρM#,在M中任意计算s0,s1,…,sn对应于M#中任意计算s0#,s1#,…,sn#,且满足(si,si#)∈ρ,其中in

定理6 给定转换系统MM#,满足M⊑ρM#,让P ⊆Σ,P#Σ#,如果γ(P#) ⊆P,且M#ð □P#,那么M$\vDash $P.

如果要证明转换系统M满足不变式P,那么只需构造关于映射ρ的抽象M#M#ð□P#,从而可使用辅助不变式γ(Reach(M#))证明。

为了定义更弱的抽象,可添加仅考虑P上状态的约束。

定义3 给定PΣM#M关于映射ρ的P-抽象,表示为MρPM#,需满足如下条件:

1) ρM上的全映射;

2) 对任何状态s0,s1Σ且s0#Σ#,(s0,s0#)∈ρ,如果存在(s0,s1)∈R,那么存在状态s1#Σ#满足(s0#,s1#)∈R#且(s1,s1#)∈ρ;

3) IP

4) 对在I中状态s,在I#中存在s#满足(s,s#)∈ρ.

通过归纳证明,在M中存在任意状态序列s0,s1,…sn (siP,0≤in),那么对应于M#中存在任意状态序列s0#,s1#,…,sn#,且满足(si,si#)∈ρ,其中i≤n。

定理7  给定转换系统M和M#,满足MρPM#,让QΣ,Q#Σ#,如果γ(Q#) ⊆QP,且M#ð□Q#,那么Mð□(QP).

4 基于抽象的不变式验证规则

通过节3的抽象,不变式验证规则SAFE可修改为抽象不变式验证规则SAFE,形式如图 4所示。

图 4 抽象规则SAFE

把Strong-SAFE验证规则修改为抽象验证规则Strong-SAFE,形式如图 5所示。

图 5 抽象规则Strong-SAFE

假定具体域上的前向算子F[R]I: (Σ)→(Σ),通过近似,可得抽象域(Σ#)上的抽象算子F#[R#]I#: (Σ#) → (Σ#),且满足F$\circ $γγ$\circ $F -(为了描述方便,F[R]IF#[R#]I#简写为FF#)。此性质保证如果Q∈(Σ#),QF#(Q),那么 γ(Q) ⊆ γ(F#(Q)) ⊆ F(γ(Q)),因此前提I1I3是满足的。那么验证€p能转换为:找到一个 Q∈(Σ#),满足γ(Q)F(γ(Q))且前提(I2): F(γ(Q)) ⊆p.

类似地,给定逆向算子B[R]P,能得到近似算子B#[R#]P#: (Σ#)→(Σ#)满足γ$\circ $B#B $\circ $γ(为了描述方便,B[R]PB#[R#]P#简写为BB#)。如果能找到Q∈(Σ#),满足QB#(Q)且前提(I1): Iγ(Q),那么也能验证€p。由于γ(Q)满足I1-I3,故€p满足。从而通过使用抽象框架得到近似算子F#B#,找到F#(Q)⊆QQB#(Q)的解。

构造近似操作符依赖于抽象域。由于F使用集合并和前向转换post构造,则F#在(Σ#)中也可通过类似的操作构造。假定抽象域(Σ#)是含有的并(join)操作的向上子格,也就是Q1,Q2∈(Σ#),γ(Q1)∪γ(Q2) ⊆ γ(Q1Q2)。令post#: (Σ#)→(Σ#)满足post $\circ $γγ$\circ $post#,I#∈(Σ#)满足I→γ(I#),定义前向近似计算F#(Q)$\triangleq $I# post#[R#](Q)满足F$\circ $γγ$\circ $F#。更形式化地,post#可定义为post#= α $\circ $post $\circ $γ。

类似如果(Σ#)是含有交(meet)操作的向下半格,也就是Q1,Q2∈(Σ#),γ(Q1Q2) ⊆γ(Q1)∩γ(Q2)。令pre#: (Σ#)→(Σ#)满足γ$\circ $pre#→pre $\circ $γ,P#∈(Σ#)满足γ(P#)⊆P,则定义逆向近似计算B#(Q)$\triangleq $P# pre#[R#](Q)满足γ$\circ $B#B$\circ $γ

5 基于抽象不动点的不变式验证

对无限和大规模状态系统,前向或逆向计算可能不终止,为了解决此问题,通常采用抽象得到近似模型。 文[16]采用了模拟框架获取抽象模型,而本文将采用抽象解释框架,并通过不动点抽象定理求解不动点。

给定具体域(Σ)和抽象域(Σ#),((Σ),α,γ,(Σ#))满足Galois连接。时态操作算子f可用其他时态算子g的最小或最大不动点表示,例如 f=λX.lfp⊑λY.g(X,Y),但其在抽象域上的最精确近似α$\circ $f$\circ $γ可能不能用最小或最大不动点描述,比如EU(X,Y)=lfpλZ.Y∪(X∩EX Z),其中EX表示具体转换系统的前向转换。EU在抽象域 (Σ#)上的最精确近似是α$\circ $EU $\circ $γ:(Σ#)→(Σ#),无法使用最小不动点来表示。但通过抽象解释框架,可使用最小不动点抽象lfpλZ#.Y#∪(X#∩EX# Z#)去计算,EX#为抽象模型上的前向转换。从而λ(X,Y). lfpλZ.Y∪(X∩EX Z)的最精确近似能用λ(X#,Y#). lfpλZ#.Y#∪ (X#∩EX# Z#)表示,且保留与具体不动点函数相同的形式。

定理8 给定状态转换系统M和M#,满足Galois连接((Σ),α,γ,(Σ#)),PΣ,P#Σ#,如果γ(P#) ⊆P,且M#$\vDash $P#,那么M $\vDash $P

由定理8可见,需要证明转换系统M满足不变式P,只需构造抽象转换系统M#且满足M#$\vDash $P#即可,也就是能够使用辅助不变式γ(Reach(M#))来证明。

在不变式验证中,辅助不变式和有效性质的搜索限制在抽象域(Σ#)中,通过前向转换找到最小不动点或者逆向转换找到最大不动点的抽象。 假定不动点计算在抽象域满足升链条件,抽象不动点通过迭代计算可得。 具体描述如下:

$\begin{align} & \forall X\subseteq \Sigma :\alpha \left( X\cup post\left[ R \right]\left( X \right) \right)\subseteq \\ & \alpha \left( X \right)\cup \left[ {{R}^{\#}} \right]\left( \alpha \left( X \right) \right). \\ \end{align}$

由定理4可知:

$\begin{align} & \alpha \left( lf_{I}^{\subseteq }\lambda X.X\cup post\left[ R \right]\left( X \right) \right)\subseteq \\ & lf_{{{I}^{\#}}}^{\subseteq }\lambda X.X\cup post\left[ {{R}^{\#}} \right]\left( X \right). \\ \end{align}$

可得

$post\left[ {{R}^{*}} \right]I\subseteq \gamma \left( lfp_{{{I}^{\#}}}^{\subseteq }\lambda X.X\bigcup post\left[ {{R}^{\#}} \right]\left( X \right) \right).$

且γ(lfpI# λX.X ∪post[R#](X)) ⊆ P,

从而获得

$post\left[ {{R}^{*}} \right]I\subseteq P$

然而,如果计算在抽象域不满足升链条件,则抽象算子F#[R#]I#可能不能在有限步收敛于不动点lfp F#[R#]I#。为了描述方便,下文中在没有歧义的情况下,采用F代替F[R]IF#代替F#[R#]I#。故采用加宽近似操作(符号为▽∈ L#'L#L#)来加速收敛,具体描述如下:∀x,y∈ L#: x⊑xyy⊑xy.则对任意升链x0x1⊑…⊑xi⊑…重新定义为y0=x0⊑…⊑yi+1 = yixi+1⊑…,得到的链不是严格的升链。同样使用加宽近似操作的向上迭代序列从初始集I#开始:F0$\triangleq $I#; 如果 F#(Fi)⊑Fi,则Fi+1$\triangleq $Fi,否则Fi+1$\triangleq $FiF#(Fi)。通过▽操作,迭代序列将收敛于一个近似点即lfp F#F,从而能在有限步完成。

如果F#⊂(F)F且迭代:${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$0$\triangleq $F${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$δ+1$\triangleq $F#(${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$δ),则${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$λ$\triangleq \underset{\delta <\lambda }{\mathop{\bigcap }}\,$${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$δ可能不收敛。可使用收窄近似操作(符号为△∈ L#'L#L#)来加速收敛。△操作满足如下:⊂x,y∈ L#: x⊑y⇒x⊑xy⊑y,则对任意降链x0⊒x1 ⊒…⊒xi⊒…重新定义为y0=x0⊒…⊒yi+1 =yixi+1⊒…,得到的链不是严格的降链。向下迭代序列的收窄近似操作定义为:${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$0$\triangleq $F; 如果F#$\left( {{{\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}}^{i}} \right)$=${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$i,则${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$i+1$\triangleq {{{\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}}^{i}}$,否则${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$i+1$\triangleq \overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}$iF#(${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$i)。通过▽操作,迭代序列将收敛于优于F的近似点即lfp F#$\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}\sqsubseteq \overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\frown}$}}{F}$F,满足于post[R]I = lfpI λX.X ∪post[R](X) ⊆ γ(${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$)⊆ γ(F)。从而可选post[R]I的向上近似γ(${\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\smile}$}}{F}}$)作为近似不动点。

设((Σ),⊆,⊥,丅,∪,∩)是完备格,lfp F是函数F∈(Σ)→ (Σ)的不动点,则不动点检验问题可描述为lfp FP。通过迭代计算lfp F,从而可检查lfp FP。采用加宽近似或收窄近似操作加速收敛,求解lfp λX.PF(X)的向上近似Q,收敛准则为PF(Q) ⊆ Q,不变式验证可表示为:F(Q) ⊆ P

定理9 设((Σ),⊆,⊥,丅,∪,∩)是完备格,F∈(Σ)→ (Σ) 是单调函数,P,Q∈(Σ),如果PF(Q) ⊆ QF(Q) ⊆ P,则lfp FP

在文[11-13]的基础上,通过不变式验证和不动点检查来改进CGR算法,构造基于抽象不动点检查的验证不变式算法Abstract-Fixpoint(),其中init为初始状态,safe为安全状态。 通过约束搜索空间,提高搜索速度,从而优化验证,如图 6所示。

图 6 基于抽象不动点检查的验证不变式算法

6 结 论

本文通过Tableau方法构造所验证公式的谓词图,获得辅助不变式的验证规则,并通过抽象框架,优化不变式验证规则; 基于抽象解释给出抽象不动点定理,为求解抽象不动点,使用加宽近似操作和收窄近似操作加速收敛,从而完成程序不变式的自动验证。

参考文献
[1] Podelski A, Rybalchenko A. Transition invariants and transition predicate abstraction for program termination[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Saarbrücken, Germany:Springer Verlag, 2011:3-10. http://cn.bing.com/academic/profile?id=1496222849&encoded=0&v=paper_preview&mkt=zh-cn
[2] Bensalem S, Bozga M, Legay A, et al. Incremental component-based construction and Verification using invariants[C]//Proceedings of the IEEE/ACM Conference on Formal Methods in Computer-Aided Design. Lugano, Switzerland:IEEE Computer Society, 2010:257-266.
[3] Chockler H, Ivrii A, Matsliah A, et al. Incremental formal verification of hardware[C]//Proceedings of the IEEE/ACM Conference on Formal Methods in Computer-Aided Design. Austin, Texas, USA:IEEE Computer Society, 2011:135-143.
[4] Bensalem S, Legay A, Nguyen T. H, et al. Incremental invariant generation for compositional design[C]//Proceedings of The 4th Theoretical Aspects of Software Engineering Conference. Taipei, Taiwan, China:IEEE Computer Society, 2010:157-167.
[5] I Dillig, T Dillig, B Li, et al. Inductive invariant generation via abductive inference[J]. Acm Sigplan Notices , 2013, 48 (48) : 443–456.
[6] Lakhnech Y, Bensalem S, Berezin S. Incremental verification by abstraction[C]//Proceeding of the Tools and Algorithms for the Construction and Analysis of Systems. Genova, Italy:Springer Verlag, 2001:98-112. http://cn.bing.com/academic/profile?id=1515363397&encoded=0&v=paper_preview&mkt=zh-cn
[7] Bj?rner N, Browne A, Manna Z. Automatic generation of invariants and intermediate assertions[J]. Theoretical Computer Science , 1997, 173 (1) : 49–87. DOI:10.1016/S0304-3975(96)00191-0
[8] Bensalem S. Automatic generation of invariants[J]. Formal Methods in System Design , 1999, 15 (1) : 75–92. DOI:10.1023/A:1008744030390
[9] Loiseaux C, Graf S, Sifakis J, et al. Property preserving abstractions for the verification of concurrent systems[J]. Formal methods in System Design , 1995, 13 (6) : 1–35.
[10] Cousot P. Formal verification by abstract interpretation[C]//Proceedings of the 4th NASA Formal Methods Symposium. Norfolk, VA, USA:Springer Verlag, 2012:3-7.
[11] Cousot P, Ganty P, Raskin F. Fixpoint-guided abstraction refinements[C]//Proceedings of the Fourteenth International Symposium on Static Analysis. Kongens Lyngby, Denmark:Springer Verlag, 2007:333-348. http://cn.bing.com/academic/profile?id=1514640333&encoded=0&v=paper_preview&mkt=zh-cn
[12] Ranzato F, Rossi Doria, Tapparo F. A forward-backward abstraction refinement algorithm[C]//Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation. San Francisco, CA, USA:Springer Verlag, 2008:248-262. http://link.springer.com/10.1007/978-3-540-78163-9_22
[13] Gantya P, Maquetb N, Raskinb F. Fixed point guided abstraction refinement for alternating automata[J]. Theoretical Computer Science , 2010, 411 (38-39) : 3444–3459. DOI:10.1016/j.tcs.2010.05.037
[14] Malkis A, Podelski A, Rybalchenko A. Thread-Modular Counterexample-Guided Abstraction Refinement[J]. Lecture Notes in Computer Science , 2011, 6337 : 356–372.
[15] Meng W, He F, Wang B. Y, Liu Q. Thread-modular model checking with iterative refinement[C]//Proceedings of the NASA Formal Method. Berlin, Heidelberg:Springer-Verlag, 2012:237-251. http://cn.bing.com/academic/profile?id=102496483&encoded=0&v=paper_preview&mkt=zh-cn
[16] Bensalem S, Graf S, Lakhnech Y. Abstraction as the key for invariant verification[J]. Lecture Notes in Computer Science , 2003, 2772 : 67–99. DOI:10.1007/b12001
[17] Gulwani S, Srivastava S, Venkatesan R. Constraint-based invariant inference over predicate abstraction[J]. Lecture Notes in Computer Science , 2009, 5403 : 120–135. DOI:10.1007/978-3-540-93900-9
[18] Patrick C, Radhia C. Parsing as abstract interpretation of grammar semantics[J]. Theoretical Computer Science , 2003, 290 : 531–544. DOI:10.1016/S0304-3975(02)00034-8