论文阅读——《Model Checking Turotial Overview》

文章目录

【1】介绍
【2】密码协议分析
- 【2.1】协议描述
- 【2.2】PROMELA模型
- 【2.3】model checking the protocol
【3】System and Properties
- 【3.1】Transition Systems
- 【3.2】Properties and Temporal Logic
- 【3.3】ω-Automata

这是师兄给的我一篇文章

摘要
我们调查了反应系统自动分析的模型检验技术原理。通过对Needham-Schroeder公钥协议的分析来举例说明模型检查的使用。然后，我们正式定义过渡系统，时间逻辑，ω-自动机及其关系。定义了线性和分支时间时序逻辑的基本模型检查算法，然后介绍了符号模型检查和偏序约简技术。本文以一些更高级主题的参考列表结尾。

【1】介绍

计算系统遍及我们的日常生活。我们依靠数字控制器来监督汽车，飞机和工业厂房的关键功能。数字交换技术已取代电信行业中的模拟组件，并且安全协议使电子贸易应用程序成为可能并且保护它的隐私。
在重要的投资甚至人类的生命受到威胁的情况下，底层硬件和软件组件的质量保证变成了最重要的东西，这需要正式的模型在一个适当的抽象层次来描述系统的相关部分。
我们关注的系统呈现出持续地与环境进行交互（例如，受控系统或通信网络的其他组件），因此该系统被称为反应性系统[60，94]。将计算机程序描述为根据给定输入值计算某些结果的传统模型不足以描述反应性系统。
相反，反应性系统的行为通常由过渡系统建模。

术语——模型检查指明了用于自动分析反应性系统的技术的集合。
可以（已经发现）以这种方式发现安全关键系统设计中的细微错误，而这些错误通常是传统的仿真和测试技术所无法企及的。
由于它已被证明具有成本效益，并且可以与传统设计方法很好地集成在一起，因此模型检查已被用作反应性系统质量保证的标准程序。

模型检查器的输入是被分析系统的一个描述，也是大量的性质，通常被表达为时序逻辑的公式，这些公式有望被保留在系统中。
模型检查器也可以确认某些性质是否保留，或者举报那些违法的性质。
在后一种情况下，它提供了一个反例：违反该性质的运行。这样的运行可以提供有价值的反馈并指出设计错误。实际上，这种观点似乎有些理想化：经常，可用资源仅允许分析系统的较粗略模型。这样，来自模型检查器的肯定判断就没有什么价值了，因为错误很可能会被必须应用于模型的简化所隐藏。
像代码审查之类的标准流程是十分重要的，它可以确保抽象模型充分地反映出实际系统的行为，为了确保利益的性质被建立或篡改。
模型检查器在此验证任务中可能会有所帮助，因为可以执行“健全性检查”，例如，确保一定可以进行某些运行或确保模型没有死锁。

本文旨在基于对大量模型检查文献的主观选择，对模型检查的一些基本原理进行教程概述。

我们从第2节中的案例研究开始，其中从用户的角度考虑模型检查的应用。

第三部分回顾了过渡系统，时间逻辑和自动机理论技术，这些技术是模型检查的基础。第4节介绍了线性时间和分支时间逻辑的基本模型检查算法。最后，第5节收集了一些对更高级主题的粗略参考。有关该卷的其他文章以及有关该主题的教科书和调查报告[27，28，69，97，124]中可以找到更多的材料。

本文包含对相关文献的许多参考，希望该调查也可以用作带注释的书目。

【2】密码协议分析

【2.1】协议描述

让我们首先以示例方式考虑使用模型检查器SPIN对Needham和Schroeder建议的公钥身份验证协议进行分析。

两个代理A（lice）和B（ob）试图通过不安全的通道建立一个共钥，以使双方都确信彼此的存在，并且没有入侵者可以在不破坏底层加密算法的情况下掌握该秘钥。
这是密码学中的基本问题之一：例如，共享秘钥可用于生成会话密钥，以进行代理之间的频繁通信。

该协议如图1.1所示。它要求参与的代理之间交换三个消息。诸如 c之类的符号表示messageM是使用agentC的公钥加密的。在整个过程中，我们假设底层加密算法是安全的，那个诚实的代理的私钥是不受影响的。
因此，只有代理C可以解密<M>c来获得M。

爱丽丝通过生成一个随机数NA并将消息<A，NA> B发送给Bob来启动协议（在密码术语中，诸如NA之类的数字称为现时数，表示任何诚实代理仅应使用它们一次）。消息的第一部分通知Bob发起者的身份。第二部分代表秘密的“一半”。
鲍勃类似地生成一个随机数NB并以消息<NA, NB>A响应。
由于第一步中生成的随机数NA的存在（只有Bob可以解密）使Alice确信消息的真实性。
因此，她接受<NA，NB>对作为共同的秘钥。
最后，爱丽丝以消息<NB>B响应。
通过与上述相同的论点，Bob得出结论，此消息必须起源于Alice，因此也接受<NA，NB>作为公共秘密。

我们假设所有消息都是通过不安全的媒体发送的。攻击者可能会截获消息，进行存储，甚至可能稍后再播。他们还可以参与协议的常规运行，启动运行或响应由诚实的代理发起的运行，这些代理不需要知道其伙伴的真实身份。但是，即使是攻击者也只能解密使用自己的公共密钥加密的消息。

该协议包含一个严重的缺陷，请读者在继续之前先找到它。在协议首次发布后约17年，使用模型检查技术发现了该错误[91]。

【2.2】PROMELA模型

我们以PROMELA（“协议元语言”）（SPIN模型检查器的输入语言）表示协议。为了使分析可行，我们做了一些简化的假设。

我们考虑了一个只有三个代理的网络：A、B、I（入侵者）。
诚实代理A和B只能参加一个运行的协议。代理A只能充当发起者，代理B只能充当响应者。因此，A和B需要最多生成一个随机数。
代理I的内存仅限于一条消息。

尽管协议很简单，但这个化简后的协议是通过模型检查来分析“现实世界”系统的典型代表：通常要求模型为有限状态，分析的复杂度通常取决于这些模型的大小。当然，我们的假设暗示在协议的多次运行中可能发生的某些错误（例如“混乱”）在我们的模型中将不会被检测到。这解释了为什么将模型检查视为调试而不是验证技术。如果在小型模型上未发现任何错误，则可以考虑在可用资源允许的情况下不太严格的限制。无论如何，重要的是要清楚地识别系统模型基础的假设，以评估分析的覆盖范围。

有了这些警告，从第2.1节的非正式描述中为诚实代理人A和B编写模型是非常简单的。 PROMELA是一种具有类似C语法的保护命令语言；它提供消息通道的原语以及发送和接收消息的操作。我们首先声明一个包含符号常量的枚举类型，以使模型更具可读性。因为每个代理都有一个随机数满足，所以我们简单地假设它们已经过预先计算，并用符号名引用它们。

mtype = { ok, err, msg1, msg2, msg3, keyA, keyB, keyI, agentA, agentB, agentI, nonceA, nonceB, nonceI };

我们将加密消息表示为包含密钥和两个数据条目的记录。然后可以将解密这个过程建模为密钥条目上的模式匹配。

typedef Crypt { mtype key, data1, data2 };

网络被建模为由三个代理共享的单个消息通道。为简单起见，我们假设网络上的同步通信由缓冲区长度0表示；这不会影响可能的通信模式，但有助于减小模型的大小。网络上的消息被建模为一个三元组，由一个识别标签（消息号），预期的接收者（入侵者可以随意忽略）和一个“加密的”消息主体组成。

图2包含代理A的PROMELA代码。最初，不确定地选择伙伴（B或I）用于后续运行（令牌::引入了不确定性选择的不同选择），并查找其公钥。然后将类型为1的消息发送到所选的伙伴，此后，代理A等待类型2的消息，以便于她可以到达网络。她验证消息主体已用她的密钥加密，并且它包含第一个消息中发送的随机数。（PROMELA允许布尔条件作为语句出现；如果发现条件为假，则该语句将阻塞。）如果是这样，她会提取伙伴的随机数，并以类型3的消息进行响应，然后声明成功。（变量statusA稍后将用于表达有关模型的正确性说明。）

代理B的代码相似，交换消息的发送和接收。

相比之下，入侵者无法使用固定的协议进行建模-分析的目的是让SPIN查找是否存在攻击。取而代之的是，对代理I进行高度不确定的建模：我们描述在任何给定状态下可能发生的操作，然后让SPIN在其中进行选择。图3所示代码的整体结构是一个无限循环，可在网络上接收和发送消息之间进行选择。

第一种选择是对消息的接收或拦截进行建模（“无关”变量“ _”反映了一个事实——入侵者无需关心消息的原本接收者）。消息正文可以存储在截取的变量中，即使它不能被解密。此外，如果消息已为代理I加密，则可以对其进行分析以提取随机数；由于该模型基于固定的随机数集，因此足以让入侵者给到目前为止已了解的随机数设置布尔标志。

第二种选择表示代理I正在发送消息。有两个子情况：或者重播先前截获的消息，或者根据到目前为止学到的信息来构造新消息。请注意，对于消息的未加密字段，我们允许任意（“类型正确”）条目。当然，诚实代理人可以立即将大多数结果组合视为不适当的组合。因此，我们的模型包含许多死锁，在下面的分析中我们将其忽略。

【2.3】model checking the protocol

该协议的目的是在确保保密性的同时，确保诚实代理之间维持互相认证。换句话说，只要A和B都成功完成了该协议的一次运行，则当且仅当B相信与A交谈时，A才应相信她的伴侣为B。此外，如果A成功与B完成了运行，则入侵者应该没有得到过A的随机数，对于B也是如此。这些性质可以用时间逻辑表示（参见第3.2节），如下所示：

G (statusA = ok ∧statusB = ok ⇒ (partnerA = agentB ⇔partnerB = agentA))
G (statusA = ok ∧partnerA = agentB ⇒¬knows nonceA)
G (statusB = ok ∧partnerB = agentA⇒¬knows nonceB)

我们向SPIN输入协议模型和第一个公式。在不到一秒钟的时间内，SPIN声明该性质被侵犯，并输出包含攻击的运行。运行被可视化为一条消息序列图，如图4所示：Alice启动与Intruder的协议运行，而Intruder使用第一条消息中接收到的随机数，反过来（伪装成A）开始与Bob进行运行。Bob回复了一条类型2的消息，该消息同时包含A和B的随机数，并为A加密。尽管代理I无法解密该消息本身，但仍将其转发给A。A毫不怀疑，发现了她的随机数，将第二个随机数返回给她的伙伴I，并宣布成功。这次，代理I可以解密消息，提取B的随机数，然后将其发送给也满意的B。结果，我们已经达到一种状态，在这种状态下，A正确地相信已经完成了与I的一次运行，而B却愚蠢地认为它在与A对话。分析第三个公式时，将产生相同的反例，而第二个公式被声明为包含该模型。

SPIN产生的反例可以很容易从第二条消息里跟踪协议中的错误来意识到这缺乏明确性：预期随机数的存在不足以证明消息的来源。为避免攻击，第二条消息因此应替换为<B，NA，NB>。修改之后，SPIN确认模型的所有三个公式均成立，这当然不能证明协议的正确性（例如，关于使用交互定理证明进行密码协议的形式验证的工作，请参见[106]）。

【3】System and Properties

反应性系统可以大致分为分布式系统（其子组件在空间上是分离的），以及共享资源（例如处理器和内存）的并发系统。分布式系统通过消息传递进行通信，而并发系统可以使用共享变量。并发进程可以共享一个公共时钟，并以锁定步骤（时间同步系统，通常用于硬件验证问题）执行，或者异步运行，共享一个公共处理器。在后一种情况下，通常会采用公平性条件，以确保可以最终计划执行的进程。过渡系统的概念提供了表示这些不同类型系统的通用框架。（运行）过渡系统的性质可以方便地用时序逻辑表示。

【3.1】Transition Systems

Definition1. 过渡系统T =（S，I，A，δ）由一组状态S，初始状态的非空子集I⊆S，一组动作A和总过渡关系δ⊆S×A×S给出（也就是说，我们要求对于每个状态s∈S，都存在a∈A和t∈S，使得（s，a，t）∈δ）。

过渡系统指定了系统允许的演化：从某个初始状态开始，系统通过执行action将系统带入新状态。文献中对过渡系统的定义略有不同。例如，有时无法明确识别动作。为了简化下面的某些定义，我们假设过渡关系是总的。可以通过包括不会改变状态的stuttering动作来确保总体。stuttering动作仅在死锁或静态状态使用。定义1通常由公平条件来补充，请参见第4.2节。一些论文使用术语Kripke结构代替过渡系统，以纪念逻辑学家Saul A. Kripke使用过渡系统来定义模态逻辑的语义[78]。

在实践中，反应式系统是使用建模语言（包括（伪）编程语言，例如PROMELA）描述的，但也使用过程代数或Petri网描述的。这些形式的操作语义可以通过过渡系统方便地定义。然而，对应于这样描述的过渡系统通常在描述的长度上具有指数级别大小。例如，共享变量程序的状态空间是变量域的乘积。建模语言及其关联的模型检查器通常针对特定类型的系统（例如同步共享变量程序或异步通信协议）进行优化。

特别是，对于由多个流程组成的系统，利用流程结构并避免显式构造表示流程联合行为的单个过渡系统是有利的。这将在4.4节中进一步探讨。

In particular, for systems composed of several processes it is advantageous to exploit the process structure and avoid the explicit construction of a single transition system that represents the joint behavior of processes. This will be further explored in section 4.4.

【3.2】Properties and Temporal Logic

给出一个过渡系统T，我们可以问如下几个问题：

T中是否有不需要的可达状态，例如死锁、互斥僵局等。
是否存在T的run，从而使系统从某个时刻开始，存在希望达到却无法达到的state或无法执行的action。这样的run意味着活锁，例如，尽管系统的其他组件仍在运行，但是一些进程不被允许进入临界区。
T的某些初始系统状态是否可以从每个状态到达？换句话说，可以重置系统吗？（类似闭包）

时序逻辑[45、79、94、95、117]是一种正式表达此类性质的便捷语言。让我们首先考虑线性时间的时序逻辑，其公式表示过渡系统的运行特性。假设给定了一个有限的原子命题集合set V，它代表各个独立状态的性质。

Deﬁnition 2. 线性时间的命题时序逻辑命题公式（P）归纳定义如下：

每一个属于 V 的原子命题 v 都是一个公式。
公式的布尔组合也是公式
如果ϕ和ψ是公式，则Xϕ（“ next ϕ”）和ϕ Uψ（“ ϕ直至ψ”）也是如此。

PTL公式是针对行为（即状态的ω序列）进行解释的。我们假设原子命题v∈V可以在状态s∈S处求值，并写s（V）表示在状态s处正确的命题集。对于行为σ= s0s1 …，我们让σi表示状态si，而σ| i表示σ的状态si si+1…。

Definition 3.
关系a |= b归纳定义如下：

略
布尔组合的语义照常定义
略
略

可以引入其他有用的PTL公式作为缩写：Fϕ（“最终ϕ”，“最终ϕ”）定义为真实U ϕ；它断言ϕ拥有一定的满足。对偶公式G ϕ¬Fϕ ϕ（“全局ϕ”，“总是ϕ”）要求all包含所有后缀。公式ϕ Wψ（“ ϕ等待ψ”，“ ϕ除非ψ”）被定义为（ϕ Uψ）∨Gϕ，并且要求ϕ保持只要ψ不成立；与ϕ Uψ不同，它不需要最终成为真。

Other useful PTL formulas can be introduced as abbreviations: Fϕ (“ﬁnally ϕ”, “eventually ϕ”) is deﬁned as true U ϕ; it asserts that ϕ holds of some sufﬁx. The dual formula Gϕ ≡ ¬F¬ϕ (“globally ϕ”, “always ϕ”) requires ϕ to hold of all sufﬁxes. The formula ϕ W ψ ( “ϕ waits for ψ”, “ϕ unless ψ”) is deﬁned as (ϕ U ψ)∨Gϕ and requires ϕ to hold for as long as ψ does not hold; unlike ϕ U ψ, it does not require ψ to become true eventually.

以下公式是有关双进程资源管理器的典型正确性声明的示例。当进程i请求资源或拥有资源时，我们认为reqi和ownsi是原子命题。

PTL公式断言了单个行为的属性，但是我们对系统有效性感兴趣：如果ϕ包含T的所有运行，我们说公式ϕ包含T（写T | = ϕ）。从这个意义上讲，PTL公式表示系统的正确性。在PTL中无法表达满足某个属性的运行的存在。这样的可能性属性是分支时间逻辑（例如逻辑CTL）（计算树逻辑[25]）的领域。

Definition 4. 命题CTL的公式归纳定义如下：

CTL公式在转换系统的状态下进行解释。 T中的路径是与δ有关的状态的ω-sequence σ= s0s1…。如果s = s0，则为s路径。

Definition 5. 关系T，s | = ϕ归纳定义如下

… 略，见笔记本
交替时间时序逻辑[6]通过允许引用无功系统的不同过程（或代理）来完善分支时间时序逻辑的路径量化器。

例如，可以断言资源管理器可以确保客户端之间的互斥，或者资源管理器和客户端1可以合作以阻止客户端2访问资源。

【3.3】ω-Automata

我们已经看到了如何解释过渡系统上的时间逻辑公式。另一方面，可以构造一个表示给定PTL公式模型的有限自动机。时序逻辑与自动机之间的这种紧密联系是PTL决策程序和模型检查算法的基础，因为有限自动机的许多属性都是可决定的，即使将其应用于ω词也是如此。无限词和树的自动机理论是由Buchuch [19]，Muller [101]和Rabin [110]发起的。我们介绍它的一些基本元素；有关更全面的论述，请参阅托马斯的精彩调查文章。

Buchi自动机与不确定有限自动机一样[68]。 “最终位置”这一概念显然不适用于ω word，但已被要求经常无限次通过接受位置的要求所取代。图6显示了两个位置的Buchi自动机，其初始位置为q0，接受位置为q1，其语言是{a，b}上的ω word集合，仅包含有限个a。

Buchi automata are presented just as ordinary (non-deterministic) ﬁnite automata over ﬁnite words [68]. The notion of “ﬁnal locations”, which obviously does not apply to ω-words, is replaced by the requirement that a run passes inﬁnitely often through an accepting location. Figure 6 shows a two-location B¨uchi automaton with initial location q0 and accepting location q1 whose language is the set of ω-words over {a,b} that contain only ﬁnitely many a’s.