k-归纳模型检测结果的认证器

A Certifier for k-Induction Model Checking Results

摘要: 基于k-归纳的模型检测可以验证许多重要的系统，但在具体的实现过程中仍可能存在缺陷，所以对其结果进行认证是非常必要的。目前最有效的方法是利用k-证据电路的概念扩展给定的模型检测问题，然后使用认证器进行判定，但是在部分情况下，QBF的验证大大增加了认证时间。为了解决这一问题，本文提出对复位检测的算法进行优化，创建了一个新的复位条件并添加了带映射的原始电路来减小QBF。并且本文还使用C语言实现了认证器。实验结果表明：利用优化算法生成的QBF有效减少了认证时间，利用C语言实现的认证器也为之后的研究提供了有力工具。

Abstract: Model checking based on k-induction can verify many important systems, but there may still be de-fects in the implementation process, so it is very necessary to verify the results. At present, the most effective method is to extend the given model checking problem by using the concept of k-witness circuit, and then use the certifier to determine. However, in some cases, the verification of QBF greatly increases the certification time. In order to solve this problem, this paper proposes to opti-mize the reset checking algorithm, create a new reset condition and add the original circuit with mapping to reduce QBF. And this paper also uses C language to achieve the certification. The ex-perimental results show that the QBF generated by the optimization algorithm effectively reduces the certification time, and the certifier implemented by C language also provides a powerful tool for future research.

1. 引言

随着科学技术的不断发展，计算机系统的规模和功能得到了不断扩充，因此，对计算机系统正确性的验证日益重要。目前，计算机系统的验证主要采用模拟法和形式化验证。其中，形式化验证采用数学化的方法证明计算机系统的正确性，相对于严重依赖测试向量的模拟法来说，更能保证验证的完备性。

形式化验证主要分为两大类：定理证明和模型检测。其中，模型检测是指通过显式状态搜索或隐式不动点计算来验证有穷状态并发系统的命题性质。相比于定理证明而言，模型检测的自动化程度更高，所以模型检测的应用更为广泛。

为了完全自动化的证明系统的正确性，验证算法是研究的核心内容。通过验证算法，将需要验证的问题转化为逻辑公式，再借助于自动化的逻辑推理工具证明逻辑公式的正确性。事实上，验证算法有很多，例如谓词抽象、路径抽象、k-归纳 [1] 等等。

k-归纳可以将模型检测简化为一系列SAT问题。基于k-归纳的模型检测可以通过对状态机进行安全可靠的分析，从而验证许多重要的系统。但在具体的实现过程中，开发人员在处理异常方面拥有很大的自由度，这就意味着即使规范已经被证明，但仍可能存在缺陷。所以为了弥补可能存在的缺陷，即提高模型检测结果的可信度，于是提出对基于k-归纳的模型检测结果进行认证。

为了认证基于k-归纳的模型检测结果，人们花费了大量时间提出了各种方法 [2] - [8]，但是有些方法无法直接适用于普通形式的k-归纳，有些方法产生的k-归纳特定证书不提供归纳不变式，还有些方法产生的认证证书是指数级的。所以，目前来说Emily Yu等人 [9] 所介绍的认证方法是最有效的，他们利用k-证据电路的概念，扩展给定的模型检测问题，得到一个更大电路的简单归纳不变式作为原始电路的k-归纳证明，将认证简化为固定数量的SAT问题和一个QBF问题，然后利用独立的认证机构进行判定，从而得到基于k-归纳的模型检测结果的认证结果。

Emily Yu等人所研发的认证器Certifiger [10] 独立于任何模型检测器，工作效率很高，但还是有一些不足之处。他们使用python语言编写认证器代码，使认证器整体有两种编程语言，故语法结构较为松散随便，非常不利于后期的调试和开发。

因此，本文致力于在Emily Yu等人的基础上利用C语言 [11] 重新实现基于k-归纳的模型检测结果的认证器。由于认证器调用的所有组件都由C语言进行编译，所以本文利用C语言编写代码从而统一认证器的编程语言，使认证器更加完整，为之后的使用、维护、调试、开发和优化都提供了便利。

2. 基本概念

设 $B\left(V\right)$ 是布尔变量V上的布尔表达式集，给定两个布尔表达式 $f\left(V\right),g\left(V\right)\in B\left(V\right)$，如果它们有相同的模型，则称它们为等价物，写为 $f\left(V\right)\equiv g\left(V\right)$。用“ $\simeq$ ”表示语法等价 [12]，“ $\to$ ”表示语法蕴涵，“ $\Rightarrow$ ”表示语义蕴涵，以及等式 $“=”$。在本文中，只关注简单的安全属性 [5]。

定义2.1. 电路 $C=\left(I,L,R,F,P\right)$ 的定义如下：

1) I是布尔输入变量集；

2) L是布尔锁存变量集；

3) $R=\langle r_l\left(L\right)|l\in L\rangle$ 是复位函数公式集；

4) $F=\langle f_l\left(I,L\right)|l\in L\rangle$ 是转换函数集，对于每个锁存器 $l\in L$，都有对应的转换函 $f_l\left(I,L\right)\in B\left(I,L\right)$ ；

5) $P\left(I,L\right)\in B\left(I,L\right)$ 是编码(好状态)属性的公式。

定义2.2. 对于展开深度 $m\in {\rm N}$，长度为m的电路C的展开定义为 $U_m=\underset{i\in \left[0,m\right)}{{\displaystyle \wedge }}\left(L_{i+1}\simeq F\left(I_i,L_i\right)\right)$。

定义2.3. 给定电路 $C=\left(I,L,R,F,P\right)$ 和 $C^{\prime }=\left(I^{\prime },L^{\prime },R^{\prime },F^{\prime },P^{\prime }\right)$，C'组合扩展C，若 $I=I^{\prime }$ 和 $L\subseteq L^{\prime }$。

定义2.4. 给定电路 $C=\left(I,L,R,F,P\right)$ 和 $C^{\prime }=\left(I^{\prime },L^{\prime },R^{\prime },F^{\prime },P^{\prime }\right)$，当C'组合扩展C时，则C'组合仿真C，如果以下条件成立：

1) $f_l\left(I,L\right)\equiv f_l{}^{\prime }\left(I,L^{\prime }\right)$ ；

2) $P^{\prime }\left(I,L^{\prime }\right)\Rightarrow P\left(I,L\right)$ ；

3) $R\left(L\right)\Rightarrow \exists \left(L^{\prime }\backslash L\right)R^{\prime }\left(L^{\prime }\right)$。

定义2.4. 1) 称为转换检测，定义2.4. 2)称为属性检测，定义2.4. 3)称为复位检测。

定义2.5. 一个公式 $\varphi$ 为电路C的归纳不变式，如果 $\varphi$ 满足以下条件：

1) $R\left(L\right)\Rightarrow \varphi \left(I,L\right)$ ；

2) $\varphi \left(I,L\right)\Rightarrow P\left(I,L\right)$ ；

3) $U_1\wedge \varphi \left(I_0,L_0\right)\Rightarrow \varphi \left(I_1,L_1\right)$。

定义2.5. 1) 称为初始性检测，定义2.5. 2) 称为一致性检测，定义2.5. 3) 称为连续性检测。

定义2.6给定一个性质为P的电路C，定义公式 $S_k=\underset{i\in \left[0,k\right)}{{\displaystyle \wedge }}P\left(I_i,L_i\right)$。当且仅当以下两个条件成立时，P在C中称为k-归纳的：

1) $U_{k-1}\wedge R\left(L_0\right)\Rightarrow S_k$ ；

2) $U_k\wedge S_k\Rightarrow P\left(I_k,L_k\right)$。

当 $\varphi \left(I,L\right)\equiv P\left(I,L\right)$ 时，1-归纳不变式等价于归纳不变式。

3. k-证据电路

在下面的定义中，用 $L^i$ 中的上标i表示锁存器L在空间方向上的副本，其中 $l^i\in L^i$ 是 $l\in L$ 的相应副本，输入也是如此。初始化位B取决于各自的初始化状态。

定义3.1. 给定电路 $C=\left(I,L,R,F,P\right)$，和 $k\in {{\rm N}}^{+}$，C的k-证据电路 $\boxed{C^{\prime }=\left(I^{\prime },L^{\prime },R^{\prime },F^{\prime },P^{\prime }\right)}$ 定义如下：

1) $\boxed{I^{\prime }}=I$ 为了简单可见，我们也称 $I^{\prime }$ 为 $X^{k-1}$ ；

2) $\boxed{L^{\prime }}=X^0\cup \cdots \cup X^{k-2}\cup L^0\cup \cdots \cup L^{k-1}\cup B$ ：

a) $X^i$ 是原始输入的副本，对于所有的 $i\in \left[0,k-2\right]$ ；

b) $L^i$ 是原始锁存器的副本，对于所有的 $i\in \left[0,k-1\right]$ ；

c) $B=\left\{b^0,\cdots ,b^{k-1}\right\}$ 是初始化位的集合；

3) 重置函数 $\boxed{R^{\prime }}=\left\{{r^{\prime }}_l\left(L^{\prime }\right)|l\in L^{\prime }\right\}$ 定义如下：

a) 对于 $x\in X^{\text{0}}\cup \cdots \cup X^{k-\text{2}}$， ${r^{\prime }}_x=x$ ；

b) 对于 $i\in \left[1,k-1\right)$， $u^i=R\left(L^i\right)\vee u^{i+1}$，且 $u^{k-1}=R\left(L^{k-1}\right)$ ；

c) 对于 $l\in L^{\text{0}}$， ${r^{\prime }}_l=ite\left(u^{\text{1}},l,r_l\left(L^{\text{0}}\right)\right)$ ；

d) 对于 $i\in \left[1,k\right)$， ${r^{\prime }}_{l^i}=ite\left(u^i,l^i,f_{l^i}\left(X^{i-1},L^{i-1}\right)\right)$ ；

e) ${r^{\prime }}_{b^{k-1}}={\rm T}$ ；

f) ${r^{\prime }}_{b^0}=\neg u^1$ ；

g) 对于 $i\in \left[1,k-1\right)$， ${r^{\prime }}_{b^i}=b^{i-1}\vee \left(R\left(L^i\right)\wedge \neg u^{i+1}\right)$ ；

4) $\boxed{F^{\prime }}=\left\{{f^{\prime }}_l\left(I^{\prime },L^{\prime }\right)|l\in L^{\prime }\right\}$ 被定义如下：

a) 对于 $i\in \left[0,k-1\right)$， ${f^{\prime }}_{x^i}\left(I^{\prime },L^{\prime }\right)=x^{i+1}$ ；

b) 对于 $l\in L^{k-1}$， ${f^{\prime }}_l\left(I^{\prime },L^{\prime }\right)=f_l\left(X^{k-1},L^{k-1}\right)$ ；

c) 对于 $i\in \left[0,k-1\right)$， ${f^{\prime }}_{l^i}\left(I^{\prime },L^{\prime }\right)=l^{i+1}$ ；

d) 对于 $i\in \left[0,k-1\right)$， ${f^{\prime }}_{b^i}\left(I^{\prime },L^{\prime }\right)=b^{i+1}$ 且 ${f^{\prime }}_{b^{k-1}}\left(I^{\prime },L^{\prime }\right)=b^{k-1}$ ；

5) 性质 $\boxed{P^{\prime }}$ 被定义为 $P^{\prime }\left(I^{\prime },L^{\prime }\right)=\underset{i\in \left[0,4\right]}{{\displaystyle \wedge }}{p}_i\left(I^{\prime },L^{\prime }\right)$ ：

a)对于 $i\in \left[0,k-1\right)$， $h^i=\left(L^{i+1}\simeq F\left(X^i,L^i\right)\right)$ ；

b) $p_0\left(I^{\prime },L^{\prime }\right)=\underset{i\in \left[0,k-1\right)}{{\displaystyle \wedge }}\left(b^i\to b^{i+1}\right)$ ；

c) $p_1\left(I^{\prime },L^{\prime }\right)=\underset{i\in \left[0,k-1\right)}{{\displaystyle \wedge }}\left(b^i\to h^i\right)$ ；

d) $p_2\left(I^{\prime },L^{\prime }\right)=\underset{i\in \left[0,k\right)}{{\displaystyle \wedge }}\left(b^i\to P\left(X^i,L^i\right)\right)$ ；

e) $p_3\left(I^{\prime },L^{\prime }\right)=\underset{i\in \left[1,k\right)}{{\displaystyle \wedge }}\left(\left(\neg b^{i-1}\wedge b^i\right)\to R\left(L^i\right)\right)$ ；

f) $p_4\left(I^{\prime },L^{\prime }\right)=b^{k-1}$。

定理3.1. 电路C组合仿真其k-证据电路。

定理3.2. 给定电路C，一个固定的 $k\in {{\rm N}}^{+}$，以及它的k-证据电路 $C^{\prime }$，P在C中是k-归纳的，当且仅当P'在C'中是1-归纳的。

Figure 1. The structure of input and latch variables in C and C'

图1. C和C'中输入和锁存变量的结构

图1显示了原始电路及其k-证据电路的可变结构的比较，标记为黄色的区域(左框和位于右侧的右上框)是由同一组变量组成。

4. 认证器

4.1. 认证原理

基于k-归纳的模型检测结果的认证原理是首先利用k-证据电路的概念，得到给定电路C的k-证据电路C'，由定理3.1可知C'组合仿真，然后根据定理3.2可知，当P在C中是k-归纳的，当且仅当P'在C'中是1-归纳的，故P'是C'的归纳不变式。所以为了得到认证结果，对归纳不变式P'的初始性检测、连续性检测和一致性检测逐一判定，而其中为了保证认证的正确性，对组合仿真概念的转换检测、属性检测和复位检测也进行判定，如果组合仿真和归纳不变式的六个检测都验证成功，那么这意味着电路C'组合仿真C，并且P'是C'的归纳不变式，故基于k-归纳的模型检测结果的认证是成功的。

认证器是为了符合上述认证原理而且能够证实基于k-归纳的模型检测结果的正确性而设计的。故认证器应具备以下功能：

1) 可以读取输入文件；

2) 可以选择任意组件进行操作；

3) 能够返回任意组件运行所生成的文件；

4) 对返回的文件进行操作；

5) 可以得到认证是否正确。

根据需求分析，需要实现一个由多个组件组成的认证器，该认证器将包含一个AIGER格式 [13] 的电路和一个由开源的基于k-归纳的模型检测器Mcaiger [14] 所提供的k值作为输入，输出一个积极的模型检测结果的认证结果。

4.2. 优化算法

本文对认证器组合仿真的复位检测提出了优化算法。由于在部分情况下，QBF的求解过程比其他公式复杂很多，使整个认证过程花费了过多的时间、空间和计算量。所以为了解决这个问题，本文创建一个新的复位条件并添加了带映射的原电路，利用C和C'的复位值和其负值动态的为电路C添加与门直到添加结束，并将带映射的电路放入到指针变量中。这种算法大大减少了验证复位检测时所需的时间、空间和计算量。

算法1给出了复位检测的优化算法。此算法主要包括以下几个步骤：1) 将C的与门与C的输入个数、与C的输入个数与C的锁存个数的和与C的总个数分别进行比较，再向ci中添加带映射的电路；2) 对锁存个数进行比较，若锁存个数为0，则将终止符1写入到输出文件中；3) 若锁存个数不为0，则将ci作为与门的和值，将C的锁存器的复位值或者其负值作为与门的左值，并将C'的锁存器的复位值负值或者其原值作为与门的右值，通过循环变量的增加动态地增加做与门的次数，而锁存器变量个数的有限性保证了循环过程最终得以终止；4) 将得到的复位条件写入到输出文件中，以便提供给求解器进行计算。若计算结果为不可满足的，则复位检测条件认证成功，否则认证失败。

与原来的算法相比较而言，本文所提出的优化算法直接根据C的锁存器的复位值作与门，不需要像原来算法对C的输入、锁存和与门以及C'的输入、锁存还有与门等全部复制 $k-1$ 次，进而出现重复遍历的情况。本文所提出的算法提高了认证器的性能，使整个认证过程更加清晰明了。

4.3. C语言实现

本文使用C语言对认证器重新实现，由于认证器的输入和需要调用的所有组件都是由C语言编译的，所以本文利用C语言编译认证器的代码，使之整个认证器的代码更加完整，并且为相关研究人员之后的使用、维护、调试以及开发都提供了一个有力工具。

本文利用C语言对基于k-归纳的模型检测结果的认证器进行实现，利用函数popen()通过建立管道启动各个组件，然后利用函数fread()从各个组件运行后所得到的文件中读取数据到内存缓冲区。并且使用函数gettimeofday()得到各个组件运行花费的时间，从而得到整个认证器运行各个实例所花费的时间。本文还利用函数fopen()打开并读取文件，从而得到C、C'以及六个检测的电路大小、输入个数、与门个数等信息。

在认证器的运行过程中，首先为了读取输入文件，调用主函数将AIGER格式的具体实例传递给认证器。之后通过mcaiger-n调用开源的基于k-归纳的模型检测器Mcaiger，使Mcaiger对实例进行模型检测并且返回k值。再利用aigcertify_kind-o将C和k值传入到k-证据生成器中，从而生成k-证据电路C'。接着通过mapping_check-k调用组合仿真检测器，该检测器生成两个AIGER格式和一个QAIGER格式的文件。随后使aigcertify-o调用归纳不变式检测器，该检测器生成三个AIGER格式的文件。然后调用工具aigtocnf将AIGER格式的文件转换为CNF，利用kissat-q调用求解器Kissat [15] 对CNF求解。最后使用文件qaiger2qcir将QAIGER格式的QBF转换为QCIR格式，然后调用求解器QuAbs [16] 对QBF求解，当求解全部完成，就可得到认证是否成功的结论。认证器的工作流程如图2所示。

Figure 2. The Dataflow diagram of the Certifier

图2. 认证器的数据流程图

4.3. 实验结果

本文实验选择TIP suite [17] 和HWMCC10 [18] 两种测试基准。本次实验使用了一台带有Ubuntu18.04虚拟机的电脑，配备Intel i5-8250U 1.60 GHz CPU和4 GB主内存。实验中所用的时间都是以秒为单位，电路的规模是就门的个数而言。

本文在使用TIP suite基准进行实验前，通过调用AIGER库中的smvtoaig，将基准从SMV文件转换为AIGER格式的文件。在TIP suite基准中，为了确保一个正确的认证器的正常运行，事先对因为k值无意义或者k值过大导致运行时花费的时间过长从而认证失败的实例进行了预先过滤。实验中要求所选取的实例满足k值在4和96之间变化，并且SAT求解器能够处理而不出现超时情况。表1报告了TIP suite基准的实验结果。

Table 1. Experimental results for the TIP suite

表1. TIP suite的实验结果

本文还使用了2010年硬件模型检测竞赛(HWMCC10)的基准。通过将各个实例分别在Mcaiger上运行15分钟，从而对基准进行预先过滤，并且从中排除了无意义k值的实例和需要简单路径约束的实例。由于同一组的基准k值基本相同，所以尽量挑选不在同一组的各个基准。表2报告了HWMCC10的部分基准的认证结果。

Table 2. Experimental results for the HWMCC10

表2. HWMCC10的实验结果

如表1和表2所示，对于基于k-归纳的模型检测结果的认证，展示了两种不同类型基准的实验结果。实验结果表明：本文利用C语言重新实现的认证器可以对模型检测结果进行认证，而且得到不同实例的k值、C的电路大小和认证所花费的时间。

5. 结论

本文通过C语言重新实现了基于k-归纳的模型检测结果的认证器，为后续的研究提供了一个有力的认证工具。在以后的工作中，我们希望可以将该方法扩展到常见的预处理技术，甚至扩展到更具挑战性的无限状态的系统中。

NOTES

^*通讯作者。