许多安全关键领域如航空航天、轨道交通、芯片设计等, 由于涉及人类生命、重大财产安全, 对系统的安全性十分重视. 以芯片为例, 无论是自动驾驶汽车、智能手机, 还是微小的心脏起搏器, 都有芯片的身影, 如果芯片出现问题, 可能会造成严重的后果, 给当事人或相关企业带来极大的生命或财产损失. 为解决此类问题, 从芯片设计到生产为成品进入市场的过程中, 有诸多流程以保证安全芯片的质量, 如仿真(simulation)、验证(verification)、可测性设计(design for test, DFT)等^[1]. 形式化验证是一种将数学方法应用在计算机安全领域的科学方法. 简单来讲, 形式化验证利用数学方法将目标系统进行形式化建模, 在此基础上, 用数学推理的方法(定理证明)或者自动化穷举所有行为的方式(模型检测)对目标模型检测其是否符合某种设计者编写的性质. 无论输入是什么, 形式化验证提供了一种确保硬件或软件系统满足某些关键性质的方法. 在某些情形下, 过去20年里开发的自动化方法可以使用最小的用户交互去验证大型复杂系统的性质, 并检测这些系统中的错误. 这些自动化程度非常高的方法可以作为设计验证过程中仿真和测试的辅助手段, 使设计的系统更健壮、更可靠.

使用合适的工具对目标迁移系统进行建模, 并用逻辑(例如线性时态逻辑, linear temporal LogicF, LTL^[2])指定系统性质之后, 就能够以自动化方式来形式化地验证这些性质. 作为一种完全自动化的验证技术, 模型检测技术由Clarke和Emerson首次提出^[3]. 该种技术不仅可以证明系统是满足性质的, 还能在系统不满足性质时提供反例, 即一条从初始状态到违反性质状态的路径. 反例可以用于追踪错误的系统行为, 这对诊断系统问题非常有价值. 一般地, 给定一个系统模型M和一个性质P, 模型检测回答了P是否满足模型M的问题.模型检测技术的基本原理是: 利用自动化搜索技术(算法)对待检查模型的整个状态空间进行遍历, 查看待检查模型是否符合给定的性质. 模型检测器作为模型检测算法的实现实体, 其作用如图 1所示. 它将要验证的性质P和待检测的模型M作为输入, 若性质成立, 则找到一个不变式证明性质P在模型M上始终成立; 否则, 提供一个反例作为系统违反性质的证据. 这里, 反例通常是一个输入序列, 通过该序列可以还原系统到达违反性质的路径. 特别的, 若P为所谓的安全性质(safe property), 模型检测找到的反例长度就一定是有限的. 本文主要关注的是安全性质的模型检测技术.

作为一种有效的形式化验证技术, 模型检测在硬件设计界中受到越来越多的关注^{[1, 4]}, 已应用于软硬件开发生命周期的大多数阶段以确保正确性, 如在电子设计自动化(electronic design automation, EDA)领域应用广泛. 除此之外, 模型检测可以用于验证软件需求^[5−8]、软件设计模型^[9−11], 甚至用于测试和调试^{[12, 13]}. 最后, 模型检测还可以用于验证广泛的应用程序, 如Web、设备驱动程序^[14−16]、GUI^{[17, 18]}、分布式程序^[19−21]、嵌入式系统^[22−24]、数据库^[25]和恶意软件^[26]. 这些场景表明, 模型检测在软件工程中扮演了重要的角色^[27].

虽然模型检测已广泛应用于软件和硬件验证, 但为了能帮助解决更多的工业实例, 继续改进性能仍然是迫切需要. 众所周知的是: 在模型检测领域, 没有一种最佳技术是优于所有其他技术的; 而且不同的算法在不同的基准上表现不同的性能^[28]. 尽管在近30年前发明了有界模型检测(bounded model checking, BMC)^[29], 但其依然被认为是检测性质违反或bug的最有效的技术. 同时, 插值模型检测(IMC)^[30]和IC3^[31], 或性质有向可达性(PDR)^[32], 在证明正确性方面具有更强的能力. 因此, 学术界和工业界通常会维护一个模型检测技术的组合来解决不同的问题.

在本文中, 我们提出一种全新的安全性质模型检测算法UAIR (UC-based approximate incremental reachability), 它使用可满足性判定得到的不可满足核来构造候选安全不变式, 并在检查不安全性的同时对候选安全不变式进行改进, 直到找到一个真正的不变式证明系统是安全的, 或者找到一个反例来证明系统不安全. 与之前的模型检测算法IC3/PDR或是CAR^{[33, 34]}相比, UAIR的主要特征是不需要维护从起点或终点可达的(向上近似的)状态序列, 而是通过计算一组候选安全不变式(本质上也是真实状态空间的超集), 并将它们组合在一起最终收敛得到一个真实的系统不变式. 我们基于2015年^[35]和2017年^[36]硬件模型检测大赛的749个工业实例进行了综合实验评估. 限定实验时间1 h, 实验结果显示: 本方法可以求解179个案例, 其中包括3个其他几个方法在相同时间内无法求解的案例.

本文第1节讨论模型检测技术的相关工作. 第2节列出模型检测及其前置知识. 第3节介绍UAIR的设计并对UAIR进行高层次的分析展示. 第4节给出实验过程及实验结果. 最后, 第5节对本文进行讨论和总结.

1 模型检测相关工作

给定一个迁移系统(例如芯片的设计), 模型检测在状态空间中自动探索以验证给定性质是否在系统上成立. 现有的模型检测算法大多数都基于展开公式, 或利用上近似和下近似并且显式地维护一个或多个状态序列. 目前, 流行的硬件模型检测技术包括有界模型检测(BMC)、插值模型检测(IMC)、IC3/PDR以及互补近似可达性分析(CAR).

BMC将搜索归约为一个SAT调用序列^[37], 每个SAT调用对应于某个步骤中的检查. 若其中一个SAT调用可满足, 则证明了模型违背给定的性质. BMC只能用于寻找反例不能用于证明系统的正确性, IMC在此基础上通过引入Craig插值作为一种抽象技术, 从而维护了一个从初始状态可达的向上近似的状态序列, 并通过检查该状态序列是否收敛实现了证明正确性的目标. IC3/PDR^{[31, 32]}是近年来主流、完备的模型检测技术, 它也像IMC一样维护了向上近似的状态序列来证明正确性. 然而与IMC相比, IC3/PDR最大的优势就是不需要对系统进行展开, 从而避免了给底层求解器造成的负担, 也可以获得更好的验证性能.

现今已有相当多的基于IC3/PDR的扩展优化工作. 比如, AVY^[38]将IC3/PDR与BMC结合, 代替求插值的方法从而得到一个新的完备算法; QUIP^[39]探索更加灵活且高效的约束学习技巧来提高证明的效率; simpleic3^[28]给出了一组IC3/PDR内部不同参数的最优组合, 使得IC3/PDR的性能表现(实验性)最优; Seufert等人^[40]研究了将正向与反向IC3/PDR结合的方式, 可以比单一方向的效果要更佳; Dureja等人^[41]提出, 可以通过学习包含内部组合变量(之前都只包含内部状态变量)来提升IC3/PDR证明的效率; Seufert等人^[42]还提出, 可以通过限制部分输入变量的方式快速找到反例; 否则, 在此基础上逐步放松对输入变量的约束, 从而得到一个完备的算法.

这3种模型检测方法(BMC, IMC, IC3/PDR)已经被证明是高度可扩展的, 并且是今天现代符号模型检测器算法组合的一部分, 例如ABC^[43]和NuSMV/NuXmv^[44].

互补近似可达性(complement approximate reachability, CAR)是一种相对较新的基于SAT的安全性模型检测方法, CAR本质上是一种受IC3/PDR启发的可达性分析算法. 与IC3/PDR相比, CAR摒弃了状态序列的单调性质, 从而得到一种更加灵活高效的寻找反例的完备算法. 实验结果表明: CAR在寻找反例上有比IC3/PDR更优异的性能, 在证明正确性上也可以作为IC3/PDR的一个补充.

本文所介绍的UAIR是一种全新、完备的模型检测算法, 与之前的IMC, IC3/PDR和CAR相比, UAIR不需要维护一个向上近似的状态序列来帮助做证明, 而是采用近似逼近的方式, 通过求解一系列的候选安全不变式直至生成最终的不变式, 实现对系统正确性的证明或是反例查找.

2 基础知识

本文所提方法主要基于布尔迁移系统、SAT求解器和符号模型检测方法, 下面就相关概念和基本知识予以介绍.

2.1 布尔迁移系统

基于SAT的模型检测技术将布尔迁移系统视为模型. 布尔迁移系统Sys定义为三元组(V, I, T), 其中, V是布尔变量的集合, 系统中的每个状态s属于2^V, 即给V中变量真值赋值的集合; I是初始状态的集合; 如果把V的拷贝标记为V′以表示后继变量的集合, T表示系统中基于V∪V′的迁移关系, 那么我们把状态s₂称为状态s₁的后继, 当且仅当${s_1} \cup {s'_2} \vDash T$, 标记为(s₁, s₂)∈T.

有限序列s₀, s₁, …, s_k被称为一条长度为k的路径, 当每个(s_i, s_i+1)对0≤i≤k−1都属于T. 我们称状态t是从状态p出发k步可达的, 当存在一条有限长度为k的路径使得s₀=p以及s_k=t成立. 所有从初始状态I出发可以到达的状态都称为Sys的可达状态. 给定一个安全性质P(通常表示为布尔公式)和一个布尔迁移系统Sys=(V, I, T), 若每个Sys的可达状态s满足P, 我们称该系统对P是安全的^[45], 也就是说s$ \models$P; 否则, 这个系统是不安全的. 我们把违反性质P的状态称为坏状态, 并且用¬P(等价bad)代表包含所有坏状态的集合. 一条从I中初始状态出发到某个¬P中坏状态的路径称为反例(counterexample).

令X⊆2^V表示Sys中状态的集合. 我们定义关系R(X)表示X中状态的后继的集合, 即R(X)=s′|(s, s′)∈T对s∈X. 对i > 1, 我们定义Rⁱ(X)=R(Rⁱ⁻¹(X)). 类似地, 定义R⁻¹(X)作为X中状态的前驱集合, i > 1时则对应R⁻ⁱ(X).

举例来说, 电路就是一种典型的迁移系统, 可以建模为多种格式. 如图 2所示的迁移模型是某个电路建模后的展示, 建模格式为与非图(and-inverter graph, aig). 图 2底部三角形表示变量输入, 椭圆形表示常量输入, 矩形表示锁存器存储周期信息; 实线为当前值, 虚线为当前值取反; 中间层圆形为与运算符; 顶部为输出, 三角形为输出目标即要验证的目标, 矩形为锁存输出, 表示对应序号锁存器下个周期的值.

2.2 标记符号

V中的每个变量a称为原子. 我们把布尔变量a或其否定¬a称为文字(literal) l. 令L表示literal的集合. cube表示∧l形式的布尔公式, 其中, l∈L, 即若干个literal的合取式, 例如l₁∧l₂∧…∧l_k, k≥1. 对应地, clause表示∨l形式的布尔公式, 其中, l∈L, 即若干个literal的析取式, 例如l₁∨l₂∨…∨l_k, k≥1. 很明显, cube的否定是clause; 反之亦然. 且并不难看出: Sys中的任意状态是cube, 即literal的合取式. 为了便于描述, 在本文后面的章节, 我们也会混用术语状态(state)和cube.

令C是cube的集合(与此相对应的是clause), 我们定义布尔公式f(C)=∨_c∈Cc(对应地, f(C)=∧_c∈Cc). 为了简单些, 当它出现在布尔公式中时, 我们用C表示f(C). 例如, 公式ϕ∧C和ϕ∨C是ϕ∧f(C)和ϕ∨f(C)的简写.

一个cube(或clause) c视为literal的集合、一个布尔公式还是一个状态集合, 取决于它使用的上下文. 如果c出现在一个布尔公式中, 例如c⇒ϕ, 则它被视为一个布尔公式. 如果我们称集合c₁是c₂的子集, 那么我们把c₁和c₂视为literal的集合. 如果我们说一个状态st属于c, 那么我们把c视为一个状态(state).

我们使用符号s(x)/s′(x′)表示状态s的当前/下个版本. 类似地, 使用符号ϕ(x)/ϕ′(x′)表示布尔公式ϕ的当前/下个版本. 对于迁移公式T, 我们用标记T(x, x′)突出它同时包含当前和下个变量. 考虑一个布尔公式ϕ, 它的字母表是V∪V′并且是合取范式(CNF). 若ϕ是可满足的, 即有一个完整赋值A∈2^V∪V′使得A$ \models$ϕ. 另外, 存在一个部分解A^p⊆A, 使得对于每个全解A′⊇A^p有A′$ \models$ϕ始终成立. 在后续章节, 我们使用标记pa(ϕ)表示ϕ的一个部分解, 并且用pa(ϕ)|_x表示通过只投影变量到V得到的pa(ϕ)的子集. 另一方面, 若ϕ是不可满足的, 存在一个最小不可满足核(MUC) C⊆ϕ(这里ϕ被视为clause的集合)使得C是不可满足的, 并且每个C′⊂C都是可满足的. 在后续章节, 我们使用标记muc(ϕ)表示这样的一个ϕ的MUC, 并且使用muc(ϕ)|_c′代表通过把clause只投影到c′得到的muc(ϕ)的子集. 由于c′是一个cube, 因此muc(ϕ)|_c′也是一个cube.

2.3 布尔可满足性求解

SAT问题指的是: 给定一个布尔公式, 公式中的变量是否存在一组赋值, 使得公式值为真. SAT问题也是第一个被证明的NP完全问题, 许多问题可以归约为SAT问题, 因此, 这个问题也是自动化验证的基础过程.

现代符号模型检测方法常用到SAT求解器, SAT求解器是一种可以用来判定布尔可满足性问题的程序. 给定一个布尔公式, 送给SAT求解器求解, 若公式是可满足的, 求解器可以返回一组赋值, 这组赋值能够使得布尔公式的值为真. 若公式是不可满足的, 即不存在这样一组赋值, 使得公式的值为真, 求解器会返回公式中的部分内容, 称为不可满足核, UC表示了该公式不可满足的原因.

为了提高求解效率, 在求解布尔可满足性问题的时候, 通常把合取范式作为输入, 若输入不是合取范式的形式, 可以通过Tseitin转换得到合取范式的形式. 把若干个clause的合取式作为条件, 交给SAT求解器求解, 即可判定该公式是否是可满足的. 实践中, 往往把模型及要验证的性质以布尔公式的形式建模为若干个clause合取的形式, 这样就可以通过SAT求解器求解当前状态可以转移到的状态以及进行可达性分析.

布尔公式可满足性求解示例如图 3所示. 图中左侧为一个合取范式的公式, 每个原子的值可以为0或1.对于这样的一个公式, 要判定其是否是可满足的, 目前有多种算法用于可满足性判定, 如DPLL^[46]、冲突驱动的子句学习(conflict driven clause learning, CDCL)^[47]. 通过这些算法判定, 能够得到一组值使得该公式为真, 原子赋值如图 3右侧所示, 即该公式是可满足的.

目前有多种开源SAT求解器可供使用, 如MiniSAT^[48], Glucose等^[49]. 一款SAT求解器通常支持以下API调用.

● IsSAT(ϕ), 判定输入公式ϕ的可满足性;

● AddClause(clause), 向SAT求解器中添加子句;

● SATAssume(assumption, ϕ), 判定基于额外假设(给一些原子变量预设的值)assumption下的公式ϕ的可满足性;

● GetModel(⋅), 当IsSAT(ϕ)或SATAssume(assumption, ϕ)为真时, 通过该方法可以获得该调用的一个模型, 模型中包含该次调用的待判定公式中每个原子变量的值(true或false). 并且, GetModel|_V返回该模型在V上的投影结果;

● GetUNSATAssumptions(⋅), 当IsSAT(ϕ)或SATAssume(assumption, ϕ)为假时, 通过该方法可以获得一该调用的假设文字的不可满足核(unsatisfied core, UC). 该不可满足核可以为假设文字的一个子集, 该子集足够使得公式不可满足.

利用布尔可满足性的判定, 可以进行可达性分析, 以此进行模型检测.

2.4 符号模型检测

利用自动机理论, 我们可以进行模型检测. 自动机的状态图可能非常大. 在最坏的情况下, 系统自动机的状态数是系统中寄存器(或其他状态保持元件)可能配置的数量, 它是指数的. 对于大多数性质语言来说, 自动机中与性质对应的状态数量也与性质literal的大小呈指数相关. 因此, 上述蛮力方法对于大型硬件设计是没有希望的. 从理论上讲, 模型状态空间的大小随着模型的规模呈指数增长. 我们将模型检测领域的这个瓶颈称为“状态空间爆炸”^[50]. 正是因为这个瓶颈的存在, 模型检测的实际应用受到极大限制. 过去模型也一般是显式表示, 即拿到一个模型, 该模型直接包含了所有状态及状态间的迁移关系. 这种表示方式使得模型检测算法无法处理非常大规模的问题.

为了解决这个问题, 学者们已经开发了许多启发式方法来避免显式地构建状态图. 因此, 现在模型一般用隐式表示, 即模型中不包含所有状态, 而是把状态间的迁移关系编码为布尔公式, 每次通过计算得到状态.目前流行的模型检测算法都是符号模型检测算法, 即将目标迁移系统建模为符号表示, 例如硬件迁移系统. 每个变量用一个值为0或1的数字表示, 即false和true. 在符号模型检测中, 安全性检测是通过符号可达性分析来实现的.

在显式模型检测中, 模型中任意两个状态的迁移关系被显式存储, 占用空间大, 难以适用到大规模的问题中. 而符号模型检测^[51]把模型符号化, 并且把状态间的迁移关系通过隐式的方式存储. 给定一个状态s, 可以通过计算的方式, 通过求解器和迁移关系T得到后继状态. 现代大部分模型检测方法都使用符号模型检测的方式取代了过去的显式模型检测, 使得模型检测适用的问题规模得到大幅度提高.

如图 4, 我们可以通过T计算s的后继状态, 也可以通过T判定可达性.

把模型符号化, 还支持对模型进行抽象和简化, 更多的优化技术使得模型检测应用的规模能够不断提高.

3 UAIR框架

在本节, 我们会展示UAIR的方法概览, 并介绍UAIR设计框架和相关定义、定理及证明.

3.1 方法概览

在基于SAT的模型检测方法中, 经常会得到SAT求解器返回的不可满足核, 而不可满足核蕴含的信息往往被忽略或利用一部分作为优化. 我们发现: 可以直接利用SAT求解器返回的不可满足核来逐步地构造不变式, 并基于这样的不变式进行安全性证明和不安全性检测. 基于以上的思路, 下面通过例子对本文提出的可达性分析方法进行说明. 总的过程如图 5−图 8所示, 图中可达状态空间仅表示当前已探测可达状态空间.

初始目标为检测从初始状态I出发是否可以转移到bad状态空间. 图 5中, 我们以bad为目标, 基于不可满足核构造的候选安全不变式包含一步可达不满足C的状态n, 且n可以一步转移到bad状态. 接下来, 以n为目标, 以相同方式检测从I出发是否可以转移到n, 这是一个递归过程.

如图 6所示, 若从I出发经过若干步可以转移到n, 则证明从I出发存在一条路径可以转移到违反性质的状态, 则检测出系统不安全且找到一个反例. 该反例表示从初始状态I出发, 可经过若干步转移到状态n, 再经过一步转移到违反安全性质P的bad状态空间.

如图 7所示, 若从初始状态I出发, 经过若干步无法转移到n, 且能够证明n是从I出发不可达的状态(该过程会构造一个针对n的安全不变式, 而对于整个bad空间来说则是候选安全不变式), 则不再把n作为待检测状态(通过候选安全不变式来实现). 继续到图 8所示状态, 由于从候选安全不变式C出发, 可转移状态除了n之外为空, 且n已经被排除在外, 因此归纳得到C为安全不变式, 证明系统是安全的, 即从初始状态I出发不可达bad空间.

图 9是一个抽象实例, 其中, s₀, s₁, s₂, s₃, s₄为从初始状态s₀出发实际可达的状态, 而s₅, s₆, s₇, s₈是可以转移到违反安全性质P(即bad)的状态.

在我们提出的可达性分析中, 假设已经拿到了一个目标为bad的候选安全不变式C, C包含多个UC, 如{−23, 5}等, 其含义为: 如果一个状态中序号为23和5的变量值分别为false和true, 则这个状态不可能在一步之内转移到bad. 在此案例中, 候选安全不变式C当前已经把状态s₀, s₁, s₂, s₃, s₄, s₇, s₈包含在内.

在改进C的过程中, 会发现C中存在状态s₇能够转移到¬C的s₅, 因此, 检测变为判定从s₀到s₅的可达性. 经过检测发现: 从s₀到s₅不可达, 得到一个针对s₅不可达的安全不变式C₁. 因此, C₁可以在后续检测中作为一个约束来减少不必要的探索.

继续改进C, 发现C中存在状态s₈能够转移到¬C的s₆, 因此, 检测变为判定从s₀到s₆的可达性. 经过检测发现: 从s₀到s₆不可达, 得到一个针对s₆不可达的安全不变式C₂. 因此, C₂也可以在后续检测中作为一个约束来减少不必要的探索. 此时, C中包含的所有状态在C₁和C₂的约束下, 这些状态都无法转移到¬C, 因此得到结论, C也是一个安全不变式. 因为从I出发可达的所有状态都无法转移到bad, 该系统是安全的.

3.2 理论框架

总的来说, 与其他现有模型检测算法不同, UAIR利用不可满足核来对模型进行检测, 包括安全性证明和不安全性检测. 我们使用从SAT求解器的可满足性判定中获得的不可满足核构造候选安全不变式, 随后, 在检测过程中, 以递归的方式改进候选安全不变式, 直到获得安全不变式, 证明系统是安全的, 或找到一个反例证明系统不安全. 我们相信, 这个方法可以作为现代模型检测工具集中一个有价值的补充.

从初始状态I开始, UAIR在检测的同时构造候选安全不变式. 即: 在检测的过程中, 利用不可满足核把所有无法一步转移到¬P(即bad)的状态集合添加进不变式; 同时, 遍历当前状态可以转移到的在不变式之外的状态. 继续此过程, 直到找到反例, 或完成候选安全不变式构造. 候选安全不变式保证范围内的状态都是无法一步转移到¬P的状态, 但可能存在状态能够转移到候选安全不变式之外. 通过候选安全不变式求解是否存在状态s和状态n, 其中: s属于候选安全不变式, n不属于候选安全不变式, s可一步转移到n. 若n可以一步转移到¬P, 屏蔽状态n, 以相同方式判断I是否能够转移到n. 如果I可以转移到n, 则找到一条路径可以从I到¬P; 否则, 继续寻找新的n. 直到没有状态能够转移到不变式之外, 此时, 该候选安全不变式为安全不变式, 可以证明系统的安全性.

在本文中, 我们引入了候选安全不变式的概念, 即该不变式可以通过后续的改进过程成为一个真实的不变式.

定义1(安全不变式及候选安全不变式). 给定一个布尔迁移系统Sys=(V, I, T)和安全性质P, 我们称Sys中的状态空间集合C是一个安全不变式, 当它同时满足以下3个条件时:

(1) I⇒C, 即初始状态包含在C里;

(2) C∧T⇒P′, 即C中所有状态的后继都满足P;

(3) C∧T⇒C′, 即C中所有状态的后继也都在C中.

特别的, 我们称C为一个候选安全不变式, 当它仅满足条件(1)和条件(2)时.

若一个Sys中的状态集合C在给定P的情况下满足定义1, 我们用术语“C是关于(Sys, P)的安全不变式(或候选安全不变式)”来表示.

定理1. 给定一个布尔迁移系统Sys=(V, I, T)和安全性质P, Sys满足P当且仅当存在Sys中的一个状态集合C为(Sys, P)的安全不变式.

证明:

● (⇐) 我们证明: (a) C中包含从初始状态I出发所有的可达状态; (b) C中的每个状态s都满足P, 即s⇒P. 对于条件(a), 根据定义1中的条件(1)和条件(3)可以推导出结论; 对于条件(b), 根据定义1中的条件(1)和条件(2)可以得出结论. 由于条件(a)和条件(b)均成立, 所以Sys满足P;

● (⇒) 若Sys满足P, 则存在一个状态集合C, 使得: (a) C中包含从初始状态I出发所有的可达状态; (b) C中的每个状态s都满足P. 将满足条件(a)、条件(b)的C代入定义1, 可以发现, C是一个安全不变式.

证毕.

显然, 如果我们能找到一个安全不变式, 那么就可以证明系统Sys是满足P的. 但一般来说, 要同时满足安全不变式的3个条件可能较难达到, 所以我们可以先构造候选安全不变式, 再得到最后的安全不变式. 具体地, 根据以上候选安全不变式的定义, 我们可以得到定理2.

定理2. 给定一个布尔迁移系统Sys=(V, I, T)和安全性质P, 若C₁为(Sys, P)的候选不变式, 而C₂为(Sys, P₁)的候选不变式, 这里C₁⇒P₁成立, 那么C₁∩C₂也为(Sys, P)的一个候选安全不变式.

证明: 容易证明: I⇒C₁∩C₂和(C₁∩C₂)∧T⇒P′在C₁为(Sys, P)的候选不变式, C₂为(Sys, P₁)的候选不变式的前提下都成立. 所以, C₁∩C₂也为(Sys, P)的候选不变式.

定理2表明: 我们可以构造一个严格单调的候选安全不变式序列, 使得它最终会逼近安全不变式. 这也构成了本文的核心定理.

定理3(核心定理). 给定一个布尔迁移系统Sys=(V, I, T)和安全性质P, Sys满足P当且仅当存在一个有限的状态序列C₁, C₁∩C₂, C₁∩C₂∩C₃, …, C=C₁∩C₂∩…∩C_n(n≥1)使得: (a) C为安全不变式; (b) C₁为(Sys, P)的候选不变式; 且(c) C₁∩C₂∩…∩C_k+1为(Sys, C₁∩C₂∩…∩C_k)的候选不变式(n−1≥k≥1).

证明:

● (⇐) 由于C是安全不变式, 所以根据定义1直接可以得出Sys是满足P的;

● (⇒) 当Sys满足P时, 我们提出以下构造算法来构造该候选安全不变式的序列:

(1) 首先构造C₁, 使得它满足I⇒C₁和C₁∧T⇒P成立, 即C₁中的状态都是一步不可达¬P. 根据定义1, 我们知道C₁是一个候选安全不变式;

(2) 若存在某个状态t的后继在¬P中并且它是C₁中某个状态s的后继, 那么我们构造C₂, 使得它满足I⇒C₂和C₂∧T⇒¬t成立, 即C₂中的状态都是一步不可达t的. 根据定义1, 我们知道C₂为(Sys, C₁)的候选不变式. 根据定理2, 可以证明C₁∩C₂是(Sys, P)一个候选安全不变式, 并且C₁∩C₂是严格小于C₁的, 因为s包含在C₁但不包含在C₂中;

(3) 重复以上的过程, 我们就可以不断地构造该候选安全不变式序列, 直至最终求得安全不变式.

通过以上构造方法, 我们保证了该候选安全不变式序列是严格单调的, 所以它最终一定会收敛到安全不变式上.

下面的算法1具体实现了我们构造候选安全不变式和安全不变式的过程.

算法1. UC-based Approximately Incremental Reachability (UAIR).

Input: 模型M和安全性质P;

Output: 系统不安全和反例, 或者是系统安全.

1: function MAIN(M, bad)

2:   inv←∅

3:   s₀←I

4:   t←bad

5:   bigCList←∅ //存储已获得安全不变式

6:   blockNList←∅ //存储求解中获得的可一步转移到目标t的状态n

7:   if CHECK(t, inv, 0) then

8:     return UNSAFE

9:   else

10:     return SAFE

11:   end if

12: end function

1: function BOOL CHECK(t, inv, depth)

2:   block each n in blockNList in current solver, except t

3:   add each C in bigCList to current solver

4:   C_depth←∅

5:   if TRYSOLVE(initState, t, C_depth) then //initState: 全局变量, 来自对M的解析

6:     return True

7:   else

8:     while $SAT({C_{depth}} \wedge T \wedge \neg {C'_{depth}})$ do

9:       n←n∈¬C_depth

10:       if SAT(n∧T∧t′) then

11:         inv2←∅

12:         block n in current solver

13:         blockNList←blockNList∪n

14:         if CHECK(n, inv2, depth+1) then

15:           return UNSAFE

16:         else

17:           add each C not added in bigCList to current solver

18:           block each n not blocked in blockNList in current solver, except t

19:         end if

20:       else

21:         c←uc∈n //uc来自SAT求解器(如MiniSAT)

22:         C_depth←C_depth∪c

23:       end if

24:     end while

25:     bigCList←bigCList∪C_depth

26:     inv←C_depth

27:     return SAFE

28:   end if

29: end function

1: function BOOL TRYSOLVE(s, t, C)

2:   if SAT(s∧T∧t′) then

3:     return True

4:   else

5:     c←uc∈s

6:     C←C∪c

7:     while SAT(s∧T∧¬C′) do

8:       m←m∈¬C

9:       if TRYSOLVE(m, t, C) then

10:         return True

11:       end if

12:     end while

13:     return False

14:   end if

15: end function

算法结束

Main作为程序的入口, 其中, bad是P的取反, I是初始状态. Check和TrySolve是算法的两个主要过程.

算法中, TrySolve函数的作用是求出定理3中所述的单个C_i(i≥1). 该函数接收3个参数: 第1个参数s是出发状态, t是目标状态, C是作为引用返回的候选安全不变式. 首先判定s是否可以一步转移到t: 若公式可满足, 则s可以一步转移到t, 返回true; 否则, 从SAT求解器拿到一个不可满足核c(此处对应于算法中函数TrySolve的第2−5行), 表示从s无法转移到t的原因, 也代表多个状态. 接下来遍历状态s可以一步转移到的状态m(m∈¬C), 把m作为新的s调用TrySolve递归求解, 判定m是否可达t(此处对应于算法中函数TrySolve的第7−12行): 若检测过程中某个m_i可达t, 则s可达t, 返回true; 否则, 返回false和C.

Check函数是检测的主函数, 负责检查构造的候选安全不变式是否已经是一个安全不变式. 它的第1个参数t是目标状态, inv是当从s₀出发不可达t时返回的安全不变式, C_depth是当前递归深度. 在Check过程中, 若TrySolve返回的为true, 则说明从s₀到t可达, 即找到了一条路径, s₀出发可以转移到t. 若TrySolve返回的为false, 则获得一个候选安全不变式C, C中所有状态满足无法1步或0步转移到状态t(此处对应于算法中函数Check的第5−8行). 但由于C是候选安全不变式, 所以要进一步判定C是否是安全不变式, 通过$SAT({C_{depth}} \wedge T \wedge \neg {C'_{depth}})$遍历可以从C中转移到的不满足C的状态, 若无此类状态或已遍历所有此类状态且未检测到unsafe, 则说明C是安全不变式(此处对应于算法中函数Check的第8−27行); 否则, 检测到违反性质P的状态, 且该状态从s₀出发可达.

定理4(算法正确性和完备性). 算法1返回SAFE当且仅当模型M满足性质P.

证明: 在以¬P为目标的不变式C的归纳过程中, 通过TrySolve过程可以得到初始候选安全不变式C. 第2步, 在C中检查每个满足其他安全不变式的状态s能够转移到的状态n, n∈¬C且SAT(n∧T∧¬P′)可满足. 判定I是否可达n: 若I可达n, 即找到一个反例证明系统是不安全的; 若不可达, 则重复第2步. 随着检测过程中得到的安全不变式的增加和待检测n的减少, 待检测空间严格缩小, 再根据定理3, 我们可以得出算法最终或是检测出漏洞, 或是证明系统安全而终止.

3.3 UAIR中的优化方法

一个候选安全不变式C, 总是从初始状态I和目标t开始构建. C满足的性质, 即包含初始状态I, 同时, C所包含的状态均无法在一步之内转移到t. 由于这是一个候选安全不变式, C中可能存在状态能够转移到C之外. 因此, 接下来对能够转移出去的C之外的状态继续进行检测. 通过TrySolve过程得到的候选安全不变式C, 可以用于后续的检测过程.

给定一个候选安全不变式C, 其基于目标t构建, 若从C出发可以转移到C之外的状态n, 那么就对n进行判定, 判定其是否可以一步转移到t(公式n∧T∧t′是否可满足). 若n可以一步转移到t, 即公式n∧T∧t′是可满足的, 则以之前相同的方式判定从初始状态I出发是否可达n. 若n是可达的, 即找到了一条路径, 从I出发, 经过若干步可达n, 再经过一步可以转移到t, 证明系统是不安全的.

部分解优化(partial assignment optimization)^[52], 对于check过程中的状态n而言, 若n可以一步转移到目标t, 则会继续以n为目标进行检测. 此时, 若能够在对n进行检测前得到一个表示范围更大且与n等功能的n, 则能够加快检测速度.

除部分解优化以外, 在检测过程中, 我们利用了检测过程中针对¬P之外的目标得到的安全不变式, 称为安全不变式约束优化. 首先, 对于一个包含初始状态I的安全不变式C, 无论其目标为哪个状态, 从I出发可达的状态均处于C的范围之内. 因此, 对于检测过程中得到的任意一个安全不变式C_i, 均可用于其他安全不变式的归纳过程.

具体实施如下: 在对当前候选安全不变式C进行归纳的过程中, 假设有状态m可以转移到状态n, 其中, m∈C且n∈¬C, 为了剪枝以加快检测速度, 若m无法同时满足其他所有安全不变式C_i, 则从I出发, m必定不可达, 即不需要判定从I到n是否是可达的. 即: 仅当可满足性判定IsSAT(C∧C₁∧C₂∧…∧T∧¬C′)可满足, m∈C, n∈¬C, 才继续检测公式IsSAT(I∧T∧T∧…∧T∧n′)是否可满足.

4 实验分析 4.1 评估准备

我们在公开基准数据上进行实验, 评估数据基于来自2015年和2017年硬件模型检测比赛(HWMCC 2015和HWMCC 2017)^[53]Aiger^[54]格式的749个基准, 针对安全性进行检测. 749个基准包含2015年和2017年比赛的所有案例. 2015年和2017年的HWMCC竞赛之后的2019年和2020年竞赛都使用的是Aiger新格式, 使用新格式, 不同的工具对约束的支持不同, 结果会有偏差, 所以我们在这篇论文里就暂不比较新格式的AIGER模型, 因此使用2015年及2017年的基准.

在工具方面, 我们实现了上文所描述的方法; 同时, 以ic3-ref, pdr, imc, forward-car和backward-car作为我们实验的评估基准.

我们关注的有两个方面: 一是我们方法的求解能力和求解速度; 二是我们的方法能否求解出其他几个方法都无法求解出来的例子. 对比结果方面, 我们以其他主要方法没有分歧的结果为参考, 且认为他们的结果都是正确的.

在实验结果方面, 我们所实现的工具(后面简称UAIR)所找出的所有反例已经经过第三方工具验证.

部署实验的硬件集群拥有190个计算节点, 机器类型为SUGON, 每个节点拥有2颗64位Intel Xeon Gold 6130 CPU, 主频为2.1 GHz. 每颗CPU为16核, 内存类型为DDR4, 8×16 GB.

实验对比的其他方法运行命令及参数见表 1.

4.2 实验结果

本节主要对本方法的运行时间、求解效率进行分析和对比.

在上述实验环境, 我们设置运行时间为1 h, 设置运行日志级别为最少, 求解结果如图 10所示.

由图 10可见: 在1 h内, 全部749个案例中, UAIR可以求解出179个案例. 179个案例中的大部分, UAIR都在非常短时间内求解得到结果. 这179个案例的细节见表 2.

4.3 实验对比与分析

为了评估UAIR的有效性, 我们研究了以下问题: UAIR与其他方法相比, 求解效率和求解性能如何.

为了验证这个问题的结果, 我们将UAIR与其他流行的符号模型检测方法进行了对比实验, 以UAIR为基准, 展示本方法相对其他方法能够多解出的案例数, 运行时间同样为1 h, 实验的结果见表 3.

如表 3所示:

● 与backward-car相比, 有1个Unsafe和8个Safe案例是其无法求解而UAIR可以解决的;

● 与forward-car相比, UAIR能够单独求解出4个Unsafe和3个Safe案例;

● 与IC3相比, 有1个Unsafe和3个Safe案例是其无法求解而UAIR可以解决的;

● 与PDR相比, UAIR能够单独求解出3个Unsafe和3个Safe案例;

● 与IMC相比, 有2个Unsafe和6个Safe案例是其无法求解而UAIR可以解决的.

从上面结果可以看出: 和这些发展时间久、比较成熟的方法相比, UAIR无论与哪个方法相比都有独特的能够解出的案例. 作为一个全新的方法, 这样的结果表现很不错.

图 11同时呈现了UAIR和其他几个方法的实验结果.

如图 11所示: 在可求解案例的速度方面, UAIR与其他方法表现相近, 求解速度很快.

在运行1 h所求解的案例中, 有3个UAIR可求解案例是其他几个流行方法在相同时间内都无法求解出结果的, 我们对这几个案例进行了分析.

这3个案例规模都比较小, 分别包含24, 28, 28个锁存器, 包含的逻辑个数分别为149, 143, 148, 内部结构似乎并不复杂. 而有些案例可能包含成百上千个锁存器, 且包含的逻辑更多, 其他方法求解能力比较强, 应该能很快求解出这几个案例, 而实际情况是无法在设定时间内解出.

通过分析日志文件发现: 这3个案例在构造候选安全不变式C的过程中, 状态空间的大量状态在检测的初期很快被SAT求解器返回的不可满足核所覆盖, 且在后续检测过程中, 能够转移到满足¬P的状态路径较少, 据此进一步推测出能够转移到bad的状态总数较少, 因此能够更快收敛完成检测.

归纳来讲, 本文方法基于不可满足核来探索模型的状态空间, 而非通过存储可达状态探索模型状态空间, 每次求解不可满足时, SAT求解器返回的不可满足核表示许多状态, 这些状态包括了当前状态, 也表示不可转移到目标状态的原因. 如果模型状态空间中的状态不可达¬P的原因类型数量较少, 本方法求解会更快, 利用了UC蕴含的信息, 少数UC就能覆盖大量状态空间. 依赖于UC来实现检测过程, UC所能覆盖的状态空间越大越好, 尽可能多地覆盖未检测空间, 符合这样特征的模型检测更快. 而$SAT({C_{depth}} \wedge T \wedge \neg {C'_{depth}})$过程是从¬P前向搜索的过程, 可达¬P的状态较少、从¬P前向探索的路径较短时检测更快, 否则会有大量时间在无用、琐碎的空间探索上, 因为在前向搜索的过程中大量状态从初始状态出发不可达. 而对于模型规模较大且状态不可达¬P原因的种类数比较多的案例, 本方法可能不适合求解. 因为这种情况下, 每次求解不可满足时, SAT求解器返回的UC覆盖的状态较少, 效率会比较低; 另外, 若模型中可达¬P的状态数较多, 或存在较多从可达¬P的状态前向搜索较长的路径, 也会有大量时间在无用、琐碎的空间探索上, 可能本方法效率会比较低.

在实验过程中, 我们也采用了多种优化方法改进UAIR, 实现待探索状态空间的缩减以加快检测速度. 下面进行优化前后对比分析.

采用部分解优化前后对比结果如图 12所示.

如图 12所示: 加入部分解优化后, UAIR在1 h可以求解的数量为179, 而未加部分解优化时为160, 求解数量提高约12%, 并且求解速度有所提高, 证明部分解优化是一个有效的优化方法.

综上, 本方法基于不可满足核构造候选安全不变式并进行后续检测, 相比其他方法, UAIR不需要显式存储状态, 主要思想是利用UC能够表示包含多个状态的状态空间来实现快速收敛, 帮助进行安全性证明和不安全性检测. 作为一个全新方法, 和其他已经发展多年甚至数十年的方法相比, 尽管总的求解数量与其他成熟方法如IC3, CAR等相比还存在一定距离, 但众所周知, 模型检测领域没有最好的方法, UAIR求解效率表现优秀, 求解案例的数量让人眼前一亮, 并且能够求解出3个其他方法均无法求解的案例, 而基于不可满足核的可达性分析也有许多探索空间, 有很好的发展前景.

5 总结

现代模型检测方法中, 不可满足核经常作为求解器的求解结果出现, 虽然蕴含着丰富的信息, 但是不可满足核的价值容易被忽略或仅是作为模型检测算法优化的一部分来挖掘. 在本文中, 我们提出了基于不可满足核设计的模型检测算法. 本方法利用了求解器返回的不可满足核的信息, 通过不可满足核构造候选安全不变式, 并在后续过程中不断改进候选安全不变式来实现安全性证明和漏洞查找, 设计思路直观. 作为一种全新的方法, 在实验中取得了较好的效果, 在基准集中的求解数量和求解速度都很不错, 并且相同时间内能够求解出3个其他对比方法都无法求解的案例, 证明了本方法的有效性, 也反映了挖掘不可满足核中蕴含的信息是模型检测可以继续探索的思路. 通过在大量基准上的测试及与其他现有工具的对比, 验证了本文提出的方法具有很好的前景和实际应用价值. 未来计划在本方法的基础上进行更多的改进, 加入更多对算法和实现的优化, 或是结合其他方法尝试以得到更好的效果, 相信在接下来的后续工作中, UAIR可以赶上甚至超越其他方法的综合表现, 且本方法可以作为模型检测工具集很有价值的补充.