基于树语义的异步动态下推网络可达性分析方法

摘要

基于树语义的异步动态下推网络可达性分析方法属于软件安全、可靠性技术领域，其特征在于将树语义引入到异步动态下推网络中，通过构建一个中间模型模拟模型的树语义，并采用上下文限界方法使模型的可达性为可判定，计算有限的k次上下文执行内的可达格局集合，通过计算可达格局集合与目标格局集合的交集是否为空，判断出目标格局集合是否可达，从而确定程序的抽象模型中是否存在设计错误或漏洞，保证模型的正确与可靠。

说明书

技术领域

本发明属于软件安全性、可靠性研究领域，涉及并发程序的验证方法，具体是一种并发 程序抽象模型的可达性求解技术，针对一个异步动态下推网络模型，构造一个中间模型来模 拟树语义执行方式，采用上下文限界技术对模型的逆向可达问题进行求解的一种自动化方法。

背景技术

随着多核处理器的发展，对并发程序的研究已成为程序设计的热点。然而并发程序执行 的不确定性，导致传统测试方法很难发现程序中隐匿的错误。模型检验作为一种自动验证技 术，已成为保证并发程序安全性与可靠性的重要手段之一。可达性分析通过分析某一状态是 否可达来判定程序的正确性，是模型检验的重要核心技术。

通常，并发程序使用并发下推系统或并行过程调用建模，然而这两种模型都不能很好的 模拟带有动态线程创建的程序。Bouajjani等人于2005年提出了动态下推网络，适用于含有递 归过程或带有线程动态创建的并发程序建模(A.Bouajjani,M.Müller-Olm,T.Touili.Regular  symbolic analysis of dynamic networks of pushdown systems.Proceedings of the 16th International  Conference on Concurrency Theory.LNCS 3653,San Francisco:Cisco Syst,2005,473-487)，其模 型的集合保持正则性质(Regularity)，可分析位向量问题(bitvector problem)和逆向可达问 题。通常动态下推网络的执行语义为交错语义，但交错语义下进行逆向可达分析效率不高， 为了高效的进行逆向可达分析，Lammich等人于2009年提出了动态下推网络的树语义，将程 序的执行建模为一棵树状形式，更符合程序的实际运行，并给出了树语义下的动态下推网络 的可达性分析方法，但没有考虑线程之间相互通信(P.Lammich,M.Müller-Olm,and A.Wenner. Predecessor sets of dynamic pushdown networks with tree-regular constraints.In Proc.of ICCAV 2009,LNCS 5643,Grenoble:ArtistDesign,2009,525-539)。Bouajjani在动态下推网络模型基础 上提出了异步动态下推网络模型，能建模线程基于共享内存的异步通信，但其可达性问题是 不可判定的(A.Bouajjani,J.Esparza,S.Schwoon,and J.Strejcek.Reachability analysis of  multithreaded software with asynchronous communication.In Proc.of FSTTCS 2005,LNCS 3821,Hyderabad:Springer,2005,348-359)。Faouzi于2009年提出针对带动态线程创建程序的上 下文限界分析方法，并证明其是可判定的(M.Faouzi Atig,A.Bouajjani,and S.Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads.15^thInternational Conference on TACAS LNCS 5505,Univ York:European Assoc,2009,107-123)。 Wenner于2010年将动态下推网络扩展到加权动态下推网络，增强了模型的建模能力(A. Wenner.Weighted dynamic pushdown networks.Programming Languages and Systems,LNCS 6012,Heidelberg:Springer,2010,590–609)。

发明内容

本发明目的在于提供一种针对异步动态下推网络的可达性求解方法，所述异步动态下推 网络为一种并发程序的抽象模型，通过对此模型的某些错误状态或者格局的可达性判定分析， 确定模型的执行是否会运行到错误状态，从而检测出此模型中的错误或漏洞。

本发明研究基于异步动态下推网络的可达性问题。通常异步动态下推网络的执行语义为 交错语义，但交错语义下进行逆向可达分析效率不高，为了高效的进行逆向可达分析，引入 树语义到模型中。再通过采用上下文限界方法使模型的可达性为可判定，并对其进行逆向可 达分析，最后在此模型上给出了基于树语义的上下文限界逆向可达算法。算法中构造一个中 间模型来模拟树语义执行方式，穷尽地计算k次上下文切换内中间模型的逆向可达格局，通过 投影操作得出原模型上的逆向可达格局集合。最后对目标格局集合与可达格局集合的交集进 行判空，从而解决异步动态下推网络的可达性问题。

为实现上述目的，本发明采取以下技术方案：

整个技术方案包括以下四个步骤：

步骤(1)、构造接受异步动态下推网络树语义下迁移序列的hedge-自动机，通过构造中 间模型来模拟树语义执行方式，中间模型具体的构造方法是将hedge-自动机状态和对应的模 型局部状态合并为新状态；

步骤(2)、计算此中间模型的K个上下文内的逆向可达格局集合；

步骤(3)、通过投影操作得出原模型下的逆向可达格局集合；

步骤(4)、目标可达性的判定分析。

本发明的特征在于：是一种并发程序的软件可靠性、安全性的验证方法。本发明提出的 基于树语义的异步动态下推网络的可达性分析方法，首次在异步动态下推网络的树语义下实 现了可达性判定方法。可有效地检测模型中的错误，无需用户过多参与，实现了模型可达性 求解的自动化检验，而且格局计算过程简单而有效，并且本发明提出的方法是可判定的，复 杂度为O(|G|^k-1×|Q³|×|△|)。

附图说明

图1为模型树语义下的执行序列：其中l₂₁，l₂₂、l₂₃表示非动态创建规则，l₁表示动态创 建规则，L<g,pw>表示叶子节点，spawn表示对应创建的新线程的迁移。

图2为基于树语义的异步动态下推网络逆向可达算法。该算法的详细步骤说明参见步骤 (1),(2),(3)：其中reachable为可达格局集合。while循环控制k次上下文限界。local()表示异步 动态下推网络格局对应到动态下推网络格局的投影操作。C_i存放第i次上下文计算出的格局 集合。pre_1,M[H]()操作则表示每一个上下文中所有可能的可达格局集合。proj_T()为投影操作， 得出原模型下的格局。

图3为实例分析中模型M的树语义执行序列：此图为一个实例，表示一个程序初始包含 有两个线程。例如，图左的线程起初从非动态创建规则规则N l1迁移到动态创建规则S l2， 由于S l2是动态创建规则，则其两个后继对应有两个规则(两个线程的迁移规则)N l4、N l3， 直到每个线程迁移到叶子节点L<g,p₂γ₂γ₃>，L<g,p₁γ₃>。

图4为实例分析中接收模型M的树语义执行序列的hedge-自动机：此图为自动机状态迁移 图，例如状态s₁接收l₁迁移到状态s₂，状态s₂接收迁移l₂同时迁移到状态s₃状态s₄。依次迁移，此自动 机接收图3中的迁移序列。

图5本文算法(见图2)的程序流程图。

具体实施方式

一种基于树语义的异步动态下推网络可达性分析方法，其特征在于：是一种并发程序的 软件可靠性、安全性的验证方法，是在计算机中依次按以下步骤实现的。

步骤(1)、依次按以下步骤构造中间模型，以便模拟树语义的执行方式：

步骤(1.1)构造并发程序的抽象模型——异步动态下推网络M

所述异步动态下推网络M＝(G,P,Γ,△_l,△_g)，G是全局状态集合，P是局部状态集合，Γ 表示栈符号，Γ*是Γ的幂集，表示栈符号的集合。格局(G,PΓ*)即表示所述中间模型在某一时 刻的状态。△_l是局部迁移规则集合，包括：表示栈符号为γ的某一为局部状 态p经过迁移l_p后转化为栈符号集合Γ*中的某一组栈符号w₁所对应的局部状态ρ₁；表示栈符号为γ的某一为局部状态p经过迁移l_p后同时转化为栈符号组的 第一组栈符号组的Γ*中的第一组栈符号w₁所对应的局部状态ρ₁和第二组栈符号w₂所对应的 局部状态ρ₂，其中ρ,ρ₁,ρ₂∈P,γ∈Γ,w₁,w₂∈Γ*；△_g是全局迁移规则集合：表示栈符号为γ的局部状态ρ所处的全局状态g经过迁移l_g后转换为全局状态g'下某一栈 符号w₁所对应的局部状态ρ₁；示栈符号为γ的局部状态ρ所处 的全局状态g经过迁移l_g后同时转换为栈符号组的集合Γ*中的第一组栈符号w₁所对应的局部 状态ρ₁和第一组栈符号w₂所对应的局部状态ρ₂；其中g,g'∈G,ρ,ρ₁,ρ₂∈P,γ∈Γ,w₁,w₂∈Γ*。

异步动态下推网络的格局是并发程序在某时刻的状态，表示为(g,α)∈G×(PΓ*)，其中g 为全局状态，α是一个字符串表示对应于全局状态g，由几个栈符号各自所对应的n个局部 状态为ρ_n组成的一个字符串，称之为异步动态下推网络格局相应的动态下推网络格局。

异步动态下推网络的格局集合C∈G×(PΓ*)，表示栈符号组集合Γ*下的局部状态集合P 所对应的各全局状态g的集合G，其中：ρ_iw_i∈PΓ*，(g,α)∈C，i表示一个栈符号组所对应的 局部状态的序号。

步骤(1.2)、构造hedge-自动机来接收所述中间模型树语义下的执行序列，其中，hedge- 自动机是一种树篱式自动机，树语义下的执行序列称为执行树，步骤如下：

步骤(1.2.1)执行树h是所述中间模型中的迁移序列的集合，迁移规则用表示，适 用于表示初始状态仅会有单个线程T_M的一个执行树h，此时迁移规则PΓ*>×T_M×<g′,Conf_N>，表示从栈符号组集合Γ*所对应的局部状态集合经过线程T_M后下推到 一个用Conf_N所对应的动态下推网络格局α所处的全局状态g′时的迁移规则执行树h亦 适用于当初始状态含有多个线程T_M时，从格局C出发通过执行一组树h迁移到格局C′时的 状态，表示为其中h＝t1,…,tn，n是执行树中线程T_M反映的状态t的序号。当仅有 单个线程时，通过动态创建规则L创建新线程，新创建线程的迁移序列对应创建节点S左边 的一部分执行树，创建节点S右边的迁移序列对应原来线程。执行树h可以用一个树状的线 程T_M表示为：T_M::＝N L T_M|S L T_MT_M|L<G,PΓ*>，其中TM为树状的线程集合；N L T_M为非动 态创建节点，该节点只有一个孩子，创建规则用字母组合N L表示，后继为T_M；S L T_MT_M为 动态创建节点，该节点有两个孩子，创建规则用字母组合S L表示，后继为一个动态创建出 的新线程T_M和原来的线程T_M；L<G,PΓ*>为叶子节点，其对应此线程运行终止时的格局，此 时格局为<G,PΓ*>。所述中间模型就是这种树状执行模型，用于判别迁移所属的进程，其中L 为线程创建规则，L₁对应动态创建规则，L₂为非动态创建规则。

步骤(1.2.2)依次按一下步骤用所述hedge-自动机创建执行树h

步骤(1.2.2.1)设定：

hedge-自动机T＝(S,A₀,D)，其中S为有限状态集合；A₀为一个的初始自动机，用L(A₀)表 示自动机A₀的接收语言簇，A₀∈S*；规则集合D＝D_L∪D_N∪D_S，其中D_L、D_N、D_S分别表示 叶子节点，非动态创建节点和动态创建节点的迁移规则集合。其中：规则s→A₁∈D_L表示叶子 节点，其中s∈S，自动机A₁接收所有格局集合(例如：L(A₁)∈(G,(PΓ*)⁺))。规则表示非动态创建节点，其中s,s′∈S，l∈L。规则表示动态创建节点，其中 s,s′,s_s∈S,l∈L。

步骤(1.2.2.2)按下述步骤判断执行树h＝t₁…t_n是否被hedge-自动机接收，其中t为线程， t∈T_M，T_M*为线程组。

步骤(1.2.2.2.1)判断执行树h＝t₁…t_n是否被hedge-自动机的规则集合D模拟。 对于叶子节点表示执行树t的叶子节点的 状态<g,pw>与自动机的状态s相对应时，应满足规则：

对于各个非动态创建节点nlt：表示非动态创建节 点nlt的状态与自动机的状态相对应时，应满足规则以及执行树t与相应的自动 机状态s′相对应，表示为lab_T(s′,t)。

对于各个动态创建节点slt_st，表 示动态创建节点slt_st的状态与自动机的状态相应时应满足规则在下推同 时满足非动态创建节点的状态t与自动机的状态s相对应以及动态创建节点的状态t_s与自动机 的状态s_s相对应。其中t∈T_M，l∈L,<g,nw>∈(G,PΓ*)。lab_T(s,t)表示节点在执行树中的状态t 与自动机的状态s相对应。符号“＝”表示等同于；符号∧表示以及。

步骤(1.2.2.2.2)若满足步骤(1.2.2.2.1)中的情况，则通过规则集合D构造接收执行树 h的hedge-自动机，执行树h的全局状态与自动机的所有状态相对应。

表示自动机A接收的语言簇 其中表示自动机的所有状态集合。

步骤(1.3)、将hedge-自动机A的状态和对应异步动态下推网络的局部状态相结合组成 新状态，实现迁移序列的树语义执行方式：

构造一个异步动态下推网络模型M×A来实现迁移序列在树语义下的执行方式：

M×A＝(G,P×S,Γ,L,△_l,△_g)，格局集合其中：

Conf_M×A表示对应于所述异步动态下推网络模型M×A对应的动态下推网络的格局集合。

C′×A:＝{(g,(p₁,s₁)w₁...(p_n,s_n)w_n)|(g,p₁w₁...p_nw_n)∈C′∧

其中：s_i为序号为i的hedge-自动机状态。

所述异步动态下推网络模型M×A的全局迁移规则△_g定义如下：

非动态创建规则：

动态创建规则：

所述异步动态下推网络模型M×A的全局迁移规则△_l定义如下：

非动态创建规则：

成立，

当且仅当成立。

动态创建规则：

其中：γ′，w′均为结合后的栈符号和栈符号组。

步骤(2)、依次按下述步骤计算所述中间模型的K个上下文内的正则逆向可达格局集合 pre_M[H](C′)，其中H为正则的执行树，C′为正则集合，

C′为异步动态下推网络的格局集合，C′＝(g,A)，α为对应的动态下推网络格局，在该模型 M×A中为(p,s)γ，能被自动机A接收。

pre_M[H](C′)表示模型M下从格局C′出发的逆向可达格局集合，pre_K,M[H](C′)表示模型M 下从格局C′出发的K-上下文限界逆向可达格局集合。

步骤(2.1)、计算从格局C′出发的没发生上下文切换的逆向格局集合pre_1，M[H](C′)

步骤(2.1.1)定义格局之间的迁移关系为

两个局部格局u和v之间的迁移关系为其中：

属于规则集合△_l，且u＝u₁ργu₂,v＝u₁ρ₁w₁u₂,g＝g'，或者

属于规则集合△_l，且u＝u₁ργu₂,v＝u₁ρ₂w₂ρ₁w₁u₂,g＝g'，或者

属于规则集合△_g，且u＝u₁ργu₂,v＝u₁ρ₁w₁u₂，或者

且u＝u₁ργu₂,v＝u₁ρ₂w₂ρ₁w₁u₂；

其中u₁∈(PΓ*)*,u₂∈Γ*(PΓ*)*。全局迁移规则集合和局部迁移规则集合构成了整个迁移系统。

中间模型M×A对应的动态下推网络自动机A接收字符串u₁(p,s)u₂，那么即可构造自动 机Z接收一个符号串u₁(g,(p,s))u₂，其中u₁(p,s)u₂∈L(A)，u₁∈((P,S)Γ*)*，p∈P，u₂∈Γ*((P,S)Γ*)*。

接着可按下式构造出一个自动机Z_pre*接收所述hedge-自动机Z的逆向可达格局集合，其 中，单个上下文中的逆向可达格局为：

${\mathrm{pre}}_{1,M}\left[H\right](g,u)=\underset{g^{\prime }\in G}{U}(g^{\prime },\{w\in {(\mathrm{P\Gamma }*)}^{+}:w={\mathrm{upu}}^{\prime }\cap \exists u(g^{\prime },p)u^{\prime }\in L\left(Z_{\mathrm{pre}*}\right)\left\}\right)$

其中栈符号组w都属于hedge-自动机Z_pre*的接收语言簇中，具体包括栈符号组w＝upu′和 u(g′,p)u′。

最后，将计算出的所述Z_pre*自动机接收的格局集合放入reachable集合中。

步骤(2.2)计算K-上下文限界逆向可达格局集合pre_K,M[H](C′)

若(g′,u′)∈pre_1,M[H](C′)，g′∈G，则按步骤(2.2.1)计算pre_1,M[H](g′,u′)，

步骤(2.2)、计算K-上下文限界逆向可达格局集合，依此递归计算，直到计算完设定的 有限个K个上下文时终止。从而得到中间模型M的K-上下文限界逆向可达格局集合。

步骤(3)、通过投影操作得出原模型下的逆向可达格局集合：

定义投影操作则格局C的投影操作为：

从而得出原模型下的逆向可达格局集合。

步骤(4)、目标可达性的判定分析。

根据所述格局集合C的逆向可达格局集合reachable和初始格局集合I(I为程序初始状 态对应的格局集合)，计算集合reachable和初始集合I的交集是否为空；

步骤(4.1)、若reachable∩I非空，则经过K次上下文切换的运行，某个目标格局c∈C 是可达的。则存在一个起始于初始格局的执行路径能够到达该格局中的状态，进而根据每个 进程的运行格局，尝试查找产生错误的原因；

步骤(4.2)、若reachable∩I为空，则经过K次上下文切换的运行，目标格局集合C中 的所有格局是不可达的。那么即存在两种可能：

a)经过K次上下文切换的运行，搜索的状态空间覆盖度不足以覆盖到初始状态，此时 可以增大K的值并继续求解，直至耗尽所有可用的计算资源；

b)若根据上述步骤仍不能判定目标状态是可达的，则得出结论：在现有计算能力下目 标格局是不可能出现的。

本实例针对异步动态下推网络模型应用本发明提出的求解方法进行可达性求解，仅考虑 全局变量不变的情况。实例模型如下：

异步动态下推网络M＝(G,P,Γ,△_l,△_g)，其中G＝(T,F)，P＝(p₁,p₂)，Γ＝(γ₁,γ₂,γ₃)，其对应 的全局下推规则△_g如下所示：

其中g∈G。

程序的初始格局为线程t1和线程t3的初始格局集合I＝<g,p₁γp₃γ₄>，要判定格局c′＝<g,p₂γ₂γ₃p₁γ₂ p₅γ₅>是否终将可达？

具体实施步骤如下：

步骤(1)、构造自动机T＝(S,A₀,D)接收模型的树语义执行序列，见图3。构造hedge-自动 机接收模型的树语义执行序列,见图4。构造中间模型M′＝(G,P×S,Γ,△_l,△_g)。

步骤(2)、设定一个常数k＝3，计算pre_1,M[H](c′)的格局集合c₁＝{<g,(p₂,s₄)γ(p₁,s₅)γ₂(p₅,s₉)γ₅>,<g,(p₂,s₆)γ₂γ₃(p₁,s₃)γ₃γ₂(p₅,s₉)γ₅>,<g,(p₂,s₆)γ₂γ₃(p₁,s₅)γ₂(p₄,s₈)γ₅>,<g,(p₂,s₆)γ₂γ₃(p₁,s₅)γ₂(p₃,s₇)γ₄>}。接着计算第一次上下文切换后的可达格局c₂＝pre_1,M[H](c₁)＝{<g,(p₂,s₄)γ(p₁,s₃)γ₃γ₂(p₂,s₉)γ₅>,<g,(p₁,s₂)γ₁γ₂(p₅,s₉)γ₅>,<g,(p₁,s₁)γ(p₅,s₉)γ₅>,<g,(p₂,s₄)γ(p₁,s₃)γ₃γ₂(p₄,s₈)γ₅>,<g,(p₂,s₄)γ (p₁,s₃)γ₃γ₂(p₃,s₇)γ₄>}。接着计算第二次上下文切换后的可达格局c₃＝pre_1,M[H](c₂)＝{<g,(p₂,s₄)γ (p₁,s₃)γ₃γ₂(p₄,s₈)γ₅>,<g,(p₂,s₄)γ(p₁,s₃)γ₃γ₂(p₃,s₇)γ₄>,<g,(p₁,s₂)γ₁γ₂(p₄,s₈)γ₅>,<g,(p₁,s₂)γ₁γ₂(p₃,s₇)γ₄>,<g,(p₁,s₁)γ(p₄,s₈)γ₅>,<g,(p₁,s₁)γ(p₃,s₇)γ₄>}。此时已经计算完3个上下文内从格局c′ 出发的所有的逆向可达格局集合。

步骤(3)、对格局集合c_1，c_2，c₃进行投影操作，得到原模型下的逆向可达格局集合{<g, (p₂,s₄)γ(p₁,s₅)γ₂(p₅,s₉)γ₅>,<g,γ₂γ₃p₁γ₃γ₂p₅γ₅>,<g,γ₂γ₃p₁γ₂p₄γ₅>,<g,γ₂γ₃p₁γ₂p₃γ₄>,<g,p₂γp₁γ₃γ₂p₅γ₅>,<g,p₁γ₁γ₂p₅γ₅>,<g,p₁γp₅γ₅>,<g,p₂γp₁γ₃γ₂p₄γ₅>,<g,p₂γp₁γ₃γ₂p₃γ₄>,<g,p₂γp₁γ₃γ₂p₄γ₅>,<g, p₂γp₁γ₃γ₂p₃γ₄>,<g,p₁γ₁γ₂p₄γ₅>,<g,p₁γ₁γ₂p₃γ₄>,<g,p₁γp₄γ₅>,<g,p₁γp₃γ₄>}。

步骤(4)、将初始格局集合I与步骤3计算出来的格局集合进行交集运算。得出交集为 <g,p₁γp₃γ₄>，所以格局c′可达。

上述实施实例，仅为对本发明的目的、技术方案进一步详细说明的具体个例，本发明并 非限定于此。凡在本发明的公开的范围之内所做的任何修改、等同替换、改进等，均包含在 本发明的保护范围之内。