freeBuf
鉴源论坛 · 观模丨模型检查综述
2023-03-10 09:57:52
所属地 上海

作者 |李建文 华东师范大学软件工程学院博导

版块 |鉴源论坛 · 观模


01 模型检查的历史

模型检查是一种起源于20世纪70年代末的形式化验证技术。该技术最初由Edmund M. Clarke、E. Allen Emerson和Joseph Sifakis提出,他们因在模型检查领域的贡献而获得了2007年的图灵奖。模型检查的提出最初是为了对并发和分布式系统做自动化验证,这些系统越来越复杂,手动验证则变得越来越困难。模型检查涉及系统地探索系统的所有可能状态,并检查每个状态是否满足某些属性。

在早期阶段,模型检查可以通过显示地计算Kripke结构上的不动点(针对CTL描述的性质) [1]或者是在由模型和LTL性质构造的乘积自动机上做状态搜索 [2]来完成。尽管这些技术非常直观且易于理解,但它们处理大型系统的能力非常有限,现在它们已经被以BDD [3]和SAT求解器 [4]为计算核心的符号模型检查技术所取代。事实上,基于SAT求解器的模型检查技术是目前最有前景的自动化验证技术。目前最先进的基于SAT求解器的模型检查技术包括BMC [5],IMC [6],IC3/PDR [7],和CAR [8]。

模型检查已被应用于各种系统,包括硬件电路、通信协议、操作系统和软件程序。它已被用于在部署之前检测系统中的错误和缺陷,这可以在开发过程中节省时间和金钱。今天,模型检查是一个活跃的研究和开发领域,研究人员正在不断努力,以提高其拓展性、准确性和可用性。


02 模型检查问题描述

模型检查问题是说:给定一个模型M,或者说一个状态迁移系统,如何判断M是否满足安全性质P。在具体算法实现中,我们往往是从初始状态I出发,判断┐P代表的状态是否可达,即是否所有I可达的状态都是满足安全性质P的。如果我们在算法中找到了反例,即从I出发,经过一系列状态,可以到达┐P,则我们返回反例,用以说明安全性质P不成立;如果我们找到了一个不变式,即证明了从I出发,所有可达的范围都在一个满足P的状态集合中,则我们返回验证通过,安全性质P成立。下面我们先简要介绍几个常见的模型检查算法。

图1 模型检查问题示例图

03 模型检查算法介绍

3.1 Bounded Model Checking (BMC)

BMC是一个简单但是高效的模型检查算法,类似于图搜索中的广度优先搜索。BMC从初始状态出发,先判断是否可以直接一步转移到┐P,也就是不安全的状态中,若可以,则找出了一个长度为1的反例;若不行,则说明在初始状态一步的范围内,安全性质成立,接着,BMC增大步数,判定从初始状态出发,是否可以两步转移到┐P,同样地,若可达则返回反例,若不可达,则继续增大步数,直到找到反例或者达到限定的时间为止。

如下图所示,从S0出发,先确定一步可达的S1和S2满足性质,接着增大步数,确定两步可达的S3满足性质,再确定三步可达的S4和S5满足性质,最终步数为4时,检查出四步可达的S6不满足性质,从而得到反例。

使用BMC算法可以很快地找到长度最短的反例,但是它的局限性也很大,假设BMC在k步之内找不到反例,这只能说明初始状态k步可达的状态满足安全性质,而不能证明初始状态可达的状态都是满足安全性质的,也就是说,BMC只适用于反例的寻找,而不适合证明模型满足安全性质。

图2:BMC算法示例图

3.2 Interpolation Model Checking (IMC)

IMC是在BMC的基础上改进来的模型检查算法,它不仅可以查找反例,也可以证明模型是满足安全性质P的,弥补了BMC算法的缺陷。

简要地说,在查找反例上,IMC和BMC一样,都是靠确定从初始状态出发,┐P代表的非安全状态是否是k步可达的,如果是,则找到了反例,若不是,则继续增大k的值。和BMC不同的是,对于每一个步数k,IMC都维持了一个初始状态k步之内可达的状态的超集R,即R里面也包含了一些其他的状态,且R里面的元素都满足安全性质,在寻找反例的过程中,IMC不断扩大集合R,若在某个时刻,R不能被扩大,即R里面的元素只能转移到R里面,则我们找到了一个不变式,即证明了从初始状态出发,可达的所有状态都是满足安全性质的,从而证明了模型是满足安全性质P的。

如下图所示,从初始状态S0出发,我们找到了一个状态集合R,使得S0可达的状态S1、S2和S3都在集合R中,且R中的元素都满足安全性质,因此我们证明了模型是满足安全性质的,集合R就是证据。

图3 IMC算法示例图

3.3 Property Directed Reachability (PDR)

PDR是一个较为复杂的模型检查算法,简要地说,它维持了一个满足安全性质P的状态集合的序列F,其中F(0)是初始状态I,而F(1)则是初始状态一步之内可达的集合的超集,即它里面除了有初始状态一步之内可达的状态,也包含了一些其他的状态,以此类推,后面每一个F(i)集合都是前一个F(i-1)集合的一步之内可达的集合的超集,PDR算法不断地在F(i)集合中寻找那些可以一步转移到┐P的元素S,若F(i)中的其他元素可以一步转移到S,则PDR接着判断F(i-1)中的元素可不可以两步转移到S,以此类推,若在F(0),即初始状态中,有元素可以多步转移到S,则找到了一个反例,即性质P不成立,如果在这个过程中,我们找到一个F(i)集合,使得它里面的元素都不能转移到S,则我们可以把S从这个集合及它之前的集合中删除,我们不断重复这个过程,如果在某一步,存在某个F(i)使得F(i)=F(i-1),即F(i-1)里面的状态只能转移到F(i-1)里面时,我们就找到了一个不变式,即所有初始状态可达的状态都满足了性质P,证明了性质P成立。

如下图所示,在集合F(i+1)中,状态S4可以一步转移到非安全状态S6,但是集合F(i+1)中的其他集合不能转移到S4,因此我们把S4从Fi+1及其之前的集合中删除,删除S4后,我们发现集合F(i+1)和F(i)相等,即此时F(i)里面的状态只能转移到F(i)里面,因为F(i)是初始状态可达的状态的超集,从而初始状态可达的元素都在F(i)中,因此模型的安全性质就得到了满足,F(i)就是证据。

图4 PDR算法示例图

3.4 Complementary Approximate Reachability (CAR)

CAR算法也是一个较为复杂的模型检查算法,可以有两个搜索方向(Forward CAR和Backward CAR),后续我们以Backward CAR为例。CAR维护了两个序列,B序列和F序列,F序列是从初始状态I出发可达的状态的子集的集合,B序列则是可以到达非安全状态的!P的状态的超集的集合,且F(0)= I , B(0)= !P。维护子集与超集的原因是F序列和B序列都是动态的,Fi的元素会随着算法运行不断增多,子集会越来越接近原集。而B(i)的元素则会不断减少,超集也会越来越接近原集。CAR算法就是不断地去做类似的SAT调用,然后根据结果去更新F和B序列。例如CAR算法会不断地通过SAT来判断某个状态s能否一步转移到B(i),若成立,则可以拿到s的一个后继状态s'并把其加入到F序列,随后CAR则递归询问s'是否可以转移到B(i-1);若不成立,CAR则会拿到一个uc(最小不满足核),并把这个uc来更新B(i+1)。

若存在某个B(i),其是所有B(j) (j < i) 的并集的子集,那么模型是安全的。安全性条件生效表明B序列不会再扩大,即使继续扩展B序列,新的B(i+1)中的元素,只会是下标更小的B(i)中出现过的元素,这意味着初始状态I不可能到达B(0),因此模型是安全的。此时从B0至B(i)的并集构成了一个不变式。如果某一个状态空间F(i)中,存在一个状态s,此状态属于非安全状态!P,则得到一条以I为起点,状态s为终点路径,这条路径是待验证性质的反例,将被返回。

如下图所示,我们发现集合B(i+1)包含在所有B(j) (j < i+1) 的并集中,因此安全性条件生效,B(j) (j < i+1) 的并集就是我们要找的不变式(安全性证明)。

图5 CAR算法示例图


参考文献:

[1] E. Clarke and H. Schlingloff, “Model checking,” in Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. MIT Press, 2001, pp. 1635–1790.

[2] O. Kupferman, N. Piterman, and M. Y. Vardi, “An automata-theoretic approach to infinite-state systems,” in Time for Verification: Essays in Memory of Amir Pnueli, Z. Manna and D. A. Peled, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, pp. 202–259.

[3] K. L. McMillan, Symbolic Model Checking. Boston, MA: Springer US, 1993.

[4] Y. Vizel, G. Weissenbacher, and S. Malik, “Boolean satisfiability solvers and their applications in model checking,” Proceedings of the IEEE, vol.103, no. 11, pp. 2021–2035, 2015.

[5] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, “Symbolic model checking without BDDs,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), W. R. Cleaveland, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999, pp. 193–207.

[6] K. L. McMillan, “Interpolation and SAT-based model checking,” in Computer Aided Verification, W. A. Hunt and F. Somenzi, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003, pp. 1–13.

[7] A. R. Bradley, “SAT-based model checking without unrolling,” in Verification, Model Checking, and Abstract Interpretation, R. Jhala and D. Schmidt, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 70–87.

[8] J. Li, R. Dureja, G. Pu, K. Y. Rozier, and M. Y. Vardi, “Simplecar: An efficient bug-finding tool based on approximate reachability,” in Computer Aided Verification, H. Chockler and G. Weissenbacher, Eds. Cham: Springer International Publishing, 2018, pp. 37–44.

本文为 独立观点,未经允许不得转载,授权请联系FreeBuf客服小蜜蜂,微信:freebee2022
被以下专辑收录,发现更多精彩内容
+ 收入我的专辑
+ 加入我的收藏
文章目录