基于Büchi自动机化简的JavaMOP监控器构造方法

叶玲玲， 钱俊彦， 查显伟

(桂林电子科技大学 计算机与信息安全学院，广西 桂林 541004)

随着软件系统规模和复杂性的不断增加，验证软件系统正确性和安全性的难度也越来越大。对于大规模的软件系统，传统的验证技术(如模型验证[1]和测试[2])会出现状态爆炸和难以覆盖系统所有执行分支等问题。运行时验证[3-4]是一种轻量级的形式化验证方法，它根据软件系统的实际执行情况来验证系统的正确性，能够为人们提供系统运行时行为的准确信息。运行时验证技术通过分析系统的一个或多个执行轨迹来验证系统，避免了传统形式化验证技术复杂性高的问题。运行时验证的核心部分是监控器[3]，对系统进行运行时验证就是将待验证的系统置于监控下，监控器通过验证系统的执行轨迹是否满足给定的属性来判断系统是否正确。

近年来，为了确保软件系统的正确性，运行时验证得到了广泛的应用。Asadollah等[5]在多核并行软件环境下，提出了一种基于运行时验证的漏洞检测模型，用于检测系统故障；Incki等[6]运用运行时验证技术来防止物联网中的网络攻击。然而，对系统进行运行时验证，通常会产生一些额外的验证开销，因此，减少运行时验证工具的监控开销成为了一个非常重要的研究内容。

为了减少运行时验证的开销，Reger等[7]提出MARQ验证工具，通过索引技术和对监控对象的冗余删除来减少运行时开销；Reger[8]运用静态分析去除运行时验证不可达对象，减少需检测的对象，从而减少监控开销；Chen等[9]提出了弱监控性的定义，排除不可监控的属性，以减少运行时监控开销。这些控制运行时验证开销的方法，主要考虑的是找到并删除无用的监控对象。为了达到减少运行时监控开销的目的，还可以对JavaMOP[10]、TraceMatches[11]等运行时验证工具生成监控器代码的过程进行优化，进而控制监控器在构造过程中的开销。鉴于此，提出一种基于Büchi自动机化简的监控器构造方法,降低JavaMOP运行时验证的时间和内存开销。

1 相关知识

1.1 线性时态逻辑

线性时态逻辑(linear temporal logic，简称LTL)是一种与时间有关的模态时序逻辑。引入LTL公式来描述系统行为属性，通过使用原子命题、析取操作符(∨)、next算子(X)、until算子(U)和否定操作符号()定义LTL公式的集合。

定义2(LTL语义) 令u=u0u1…∈Σω是一个无限状态序列，且Σ=2P，u满足LTL公式φ，当且仅当uφ，LTL公式的语义定义为：

utrue；

up，当且仅当p∈u；

uφ，当且仅当u/φ；

uφ1∨φ2，当且仅当uφ1或者uφ2；

uφ1∧φ2，当且仅当uφ1且uφ2；

uXφ，当且仅当ui+1φ；

uφ1Uφ2，当且仅当∃k≥0,ukuk+1…φ2和∀0≤i

使用这些定义能够推导出eventually算子(F)、always算子(G)和release算子(R)：Fφ等价于trueUφ；Gφ等价于Fφ；φ1Rφ2等价于(φ1Uφ2)。

1.2 Büchi自动机

Büchi自动机是ω自动机的一种，它将有限状态自动机扩展到无限，接受一个无限的输入序列，可以替代和处理ω正则语言。由于Büchi自动机在布尔操作[12]下是封闭的，它常被用于基于自动机的形式化验证方法。

定义3(Büchi自动机) Büchi自动机是一个五元组B=(Σ,Q,I,δ,F)。其中：Σ为非空有限字母表，且Σ′⊆2Σ；δ⊆Q×2Σ′×Q是迁移关系；Q为非空有限状态集合；I⊆Q为初始状态集合；F⊆Q为接受状态集合。

1.3JavaMOP

JavaMOP是一种基于Java语言、支持软件开发与分析的运行时验证工具，它支持多种逻辑，如线性时态逻辑(LTL)、上下无关文法(CFG)、扩展正则表达式(ERE)等，并将形式化规约以逻辑插件的形式集成在JavaMOP工具中，实现对不同形式化规约的监控。其中，LTL插件用于验证软件系统运行时是否满足给定的LTL属性。JavaMOP是目前最高效的运行时验证工具之一，在软件运行时验证中，将LTL语言描述的属性转换成监控器代码插装到待监控的系统程序中，实现实时监控系统程序的运行并返回监控结果。JavaMOP运行时监控软件系统程序的过程如图1所示。

图1 JavaMOP运行时监控软件系统程序的过程

JavaMOP在验证软件系统时，根据给定的属性规约会自动生成相应的监控器代码，并插装到目标程序中进行实时监控。JavaMOP生成监控器基于自动机的验证算法，对于给定的LTL属性，通过转换算法[13]将LTL公式转化为Büchi自动机，再将Büchi自动机转化为确定性有限自动机(determine finite automata，简称DFA)，生成监控器的抽象表示，之后得到监控器代码，实现对软件系统程序验证的功能。

2 自动机化简规则与算法

在生成监控器的过程中，减小Büchi自动机的大小，能够减少内存消耗并加快监控器代码的生成。为此，提出自动机化简规则对由LTL公式转化得到的Büchi自动机进行化简。首先对自动机中接受语言为空的状态进行移除操作；再将满足合并规则的状态进行合并化简，使得目标Büchi自动机最小化。

规则1(移除规则) 设Büchi自动机B=(Σ,Q,I,δ,F)，对自动机中的任一状态q，若从状态q开始的自动机接受语言为空，则状态q为冗余状态可移除。

规则1即取自动机中的任意一个状态，判断Büchi自动机接受的语言是否为空，若接受的语言为空，则进行冗余标记，并移除操作将其删除。移除冗余算法描述如下。

算法1RemoveRedundant(B)

输入：Büchi自动机B=(Σ,Q,I,δ,F)；

输出：新的Büchi自动机B′=(Σ′,Q′,I′,δ′,F′)，且有L(B′)=L(B)。

1 fors∈Qdo；

2 计算从状态s出发的后继状态集合nodes(s)；

3 if nodes(s)∩F=∅ then//状态s开始的自动机语言为空；

4 标记状态s为冗余状态；

5 移除状态s；

6 返回Büchi自动机B′。

规则2(合并规则) 设Büchi自动机中状态a和状态b都有n条迁移关系，若状态a的下一个状态是b,且状态a迁移到状态b的条件也是状态b的自旋条件，同时状态a剩下n-1条迁移与状态b的另外n-1迁移相同，则状态a和状态b可以合并。

合并规则对自动机冗余删除后进一步化简自动机，用于得到状态数更少的自动机。首先将自动机中的状态集分为2个集合S1和S2，集合S1用于存储接受状态，集合S2存储除了接受状态的自动机状态；然后分别对集合S1和集合S2中的状态s和s′进行判断，是否符合合并规则；若满足，则可将状态s′合并到状态s，状态s′的环移动到状态s。具体执行过程如下。

算法2Merge(B)

输入：Büchi自动机B′=(Σ′,Q′,I′,δ′,F′)；

输出：新的Büchi自动机B″=(Σ″,Q″,I″,δ″,F″)，且有L(B″)=L(B′)。

1 fors∈Qdo；

2 ifs∈Fthen；

3S1:=S1∪s//把s加入到接受状态集合S1中；

4 else；

5S2:=S2∪s//把s加入到非接受状态集合S2中；

6 //对S1集合中状态进行合并操作；

7 fors∈S1do；

8 fors′∈S1do；

9 ifs,s′满足合并规则 then；

10 合并状态s和状态s′；

11 //对S2集合中状态进行合并操作；

12 fors∈S2do；

13 fors′∈S2do；

14 ifs，s′满足合并规则then；

15 合并状态s和状态s′；

16 返回Büchi自动机B″。

图2为运用合并规则化简自动机状态的例子。使用一个三元组δ表示2个状态之间的迁移关系，如δ=(s1,c,s2)表示从状态s1迁移到状态s2的条件是c。图2(a)为化简之前的自动机，它有6个状态和13条迁移关系，其中状态s0有3条迁移关系δ1=(s0,a,s1)，δ2=(s0,c,s2)，δ3=(s0,b,s3)。状态s1也有3条迁移关系δ4=(s1,a,s1)，δ5=(s1,c,s2)，δ6=(s1,b,s3)。状态s0迁移到状态s1与状态s1到自身的条件相同，并且剩下的2条迁移也相同，因此，状态s0和s1满足合并规则，可将s0与s1合并。同样地，状态s3和s4满足合并规则，可以合并。化简得到新的自动机如图2(b)所示，它包含4个状态和7条迁移关系，与化简前相比简单了很多。

图2 运用合并规则化简自动机的例子

3 实验与分析

为了验证自动机化简规则的可行性，用Java语言实现了基于自动机的监控器构造过程，并与JavaMOP中原有构造运行时监控器的方法进行比较。为了使2种监控器构造方法的实验数据具有可比性和公平性，采用相同的测试用例，所有实验在相同的环境下进行。实验运行环境的配置如下：处理器为Inter (R) Core (TM) i5-4690 CPU@3.5 GHz和内存为8 GiB的台式电脑，电脑配备的操作系统为Ubuntu 14.04，同时配置了Sun Java SE 8环境。使用DaCapo[14]数据集，选取其中4个测试属性作为实验的测试对象，分别为：

HasNext：对于每个迭代器对象，要求在执行函数next()前调用函数hasnext()，并且hasnext()的返回值为true；

SafeSyncColl：若一个集合是同步的，则它的迭代器也应是同步访问的；

UnSafeIterator：在使用迭代器接口迭代集合元素时不能更新集合元素；

UnSafeMapIterator：在集合上对映射的键值迭代时，Map无法进行更新操作。

表1为2种监控器构造方法的性能比较。从表1可看出，在内存开销方面，化简Büchi自动机能够减少运行时监控器在构造过程中的内存消耗；在时间开销上，简化的Büchi自动机加速了生成监控器的过程，从而节省了构造监控器代码的时间，降低了整个监控器构造的时间开销。对于测试的属性HasNext，化简操作前JavaMop时间和内存开销分别为92.88 s和629.71 MiB，本方法时间和内存开销分别为89.92 s和612.23 MiB，在时间和内存开销分别降低了3.19%和2.78%。对于属性UnSafeIterator，本方法时间和内存开销分别降低4.93%和5.32%，比属性HasNext性能提升更多，这是因为属性UnSafeIterator操作更加复杂，经过化简操作后移除和约减的状态和迁移关系更多，因此，性能提升也相对更多。

表1 2种监控器构造方法的性能比较

4 结束语

对于运行时验证中基于自动机理论构造监控器的方法，通过化简Büchi自动机来减小运行时验证在监控器构造过程中的时间和内存开销，能够提高监控器生成的效率和运行时验证的性能。针对运行时验证工具JavaMOP中构造监控器的方法进行研究实验，实验结果表明，本方法在提升运行时监控性能上有一定的效果。今后研究监控器代码生成后对程序进行实时监控过程中监控算法的优化，提高监控算法效率，以进一步降低运行时验证的时间和内存开销。