第八讲 模型检验 主要考虑如何发现设计缺陷！

内 容 一、例子 二、模型检测概述 三、模型检测算法概览 四、模型检测工具

Needham-Schroeder 身份认证协议 一、例子 Needham-Schroeder 身份认证协议 通信过程可能被窃听！加密可以防止窃听！如何约定加密数字？ 每人 有自己的标识：N 每人 公布自己的公钥: 只有N才能解开的消息： [****]N 每个对话过程 用一对数字对内容加密: S1, S2 每次对话前 需要首先建立这对数字 N Z [N, S1]Z [S1, S2]N [S2]Z 该协议于1978年被提出并得到广泛应用

1996年，发现该协议存在设计缺陷： 攻击者可以伪装一方的身份 N W Z [N, S1]W [N, S1]Z [S1, S2]N 开始伪装 [N, S1]Z [S1, S2]N [S1, S2]N [S2]W [S2]Z 被欺骗！ 不可信！ 利用模型检测方法！

In 1992 Clarke and his students at CMU used SMV to verify the IEEE Future+ cache coherence protocol. • They found a number of previously undetected errors in the design of the protocol. • This was the first time that formal methods have been used to find errors in an IEEE standard. • Although the development of the protocol began in 1988, all previous attempts to validate it were based entirely on informal techniques.

In 1992 Dill and his students at Stanford used Murphito verify the cache coherence protocol of the IEEE Scalable Coherent Interface. • They found several errors, ranging from uninitialized variables to subtle logical errors. • The errors also existed in the complete protocol, although it had been extensively discussed, simulated, and even implemented.

In 1995 researchers from Bull and Verimag used LOTOS to describe the processors, memory controller, and bus Arbiter of the Power Scale multiprocessor architecture. • They identified four correctness requirements for proper functioning of the arbiter. • The properties were formalized using bisimulation relations between finite labeled transition systems. • Correctness was established automatically in a few minutes using the CÆSAR/ ALDÉBARAN toolbox.

A High-level Data Link Controller was being designed at AT&T in Madrid in 1996 • Researchers at Bell Labs offered to check some properties of the design using the Formal Check verifier. • Within five hours, six properties were specified and five were verified. • The sixth property failed, uncovering a bug that would have reduced through put or caused lost transmissions!

Richard Raimi used Motorola’s Verdict model checker to debug a hardware laboratory failure. •Initial silicon of the PowerPC 620 microprocessor Crashed during boot of an operating system. •In a matter of seconds, Verdict found a BIU deadlock causing the failure.

In 1994 Bosscher, Polak, and Vaandrager won a best-paper award for proving manually the correctness of a control protocol used in Philips stereo components. • In 1995 Ho and Wong-Toi verified an abstraction of this protocol automatically using HyTech. • Later in 1995 Daws and Yovine used Kronos to check all the properties stated and hand proved by Bosscher, et al.

The NewCoRe Project (89-92) was the first application of formal verification in a software project within AT&T. • A special purpose model checker was used in the development of the CCITT ISDN User Part Protocol. • Five “verification engineers” analyzed 145 requirements. • A total of 7,500 lines of SDL source code was verified. • 112 errors were found; about 55%of the original design requirements were logically inconsistent.

In 1995 the Concurrency Workbench was used to analyze an active structural control system to make buildings more resistant to earthquakes. • The control system sampled the forces being applied to the structure and used hydraulic actuators to exert countervailing forces. • A timing error was discovered that could have caused the controller to worsen, rather than dampen, the vibration experienced during earthquakes.

ACM 2007年度图灵奖（Turing Award） Edmund M. Clarke, E Allen Emerson, Joseph Sifakis 1981年，美国的Edmund Clarke和Allen Emerson以及在法国的Sifakis分别提出了模型检测（Model Checking）的最初概念 他们开发了一套用于判断硬件和软件设计的理论模型是否满足规范的方法 当系统检测失败时，还能利用它确定问题存在的位置

用于软件？ 软件设计模型？ •Statecharts …… 软件代码？ Use static analysis to extract a finite state synchronization skeleton from the program. Model check the result. •Bandera --Kansas State •Java PathFinder --NASA Ames •Slam Project (Bebop) --Microsoft

二、模型检测概述 1、基本情况 2、什么是模型检测 3、基本思想 4、过程描述

1、基本情况 产生 20世纪80年代初，Clarke, Emerson等提出了用于并发系统性质的CTL逻辑，设计了检测有穷状态系统是否满足给定CTL公式的算法 特性 能给出反例 自动化程度高 应用 计算机硬件、通信协议、控制系统、安全认证协议、软件安全 等

2、什么是模型检测 定义[Clarke & Emerson 1981] “Model checking is an automated technique that, given a finite-state model of a system and a logical property, systematically checks whether this property holds for (a given initial state in) that model.” 给定一个系统的有限状态模型，和一个逻辑性质，系统地检测：这个模型（含初始状态）满足该性质

3、基本思想 （1）用状态迁移系统(S)表示系统的行为，用模态/时序逻辑公式(F)描述系统的性质。 （2）“系统是否具有某种期望的性质”就转化数学问题“状态迁移系统S是否是公式F的一个模型？” 公式表示：S |= F? 对于有限状态迁移系统，这个问题是可以判定的。

4、过程描述 OK or Error trace 1、建立模型 Finite-state model 3、输入工具 Model Checker (F W) Line 5: … Line 12: … Line 15:… Line 21:… Line 25:… Line 27:… … Line 41:… Line 47:… 2、描述系统性质 Temporal logic formula

三、模型检测算法概览 1、系统的表示 2、属性的表示 3、搜索状态空间 2个例子：CTL 与 LTL

1、系统的表示 例子:微波炉系统 1 4 2 3 5 7 6 open door start oven cook close door ~Heat ~Error open door start oven cook close door open door 4 2 3 Start ~Close ~Heat Error ~Start Close ~Heat ~Error ~Start Close Heat ~Error open door close door start oven start cooking reset 5 7 6 Start Close ~Heat Error Start Close ~Heat ~Error Start Close Heat ~Error warmup

2、属性表示(Property Specification) 用各种模态/时序逻辑表示： 计算树逻辑（CTL: Computation Tree Logic） 线性时序逻辑 （LTL: Linear Temporal Logic） 模态命题 u --演算（u-Calculus） 主要检测属性类型： 安全性（safety）：坏的事情不会发生。例如：无死锁 活性（liveness）：好的事情终会发生。例如：请求响应 公平性（fairness）： 一致性（consistency）： For any reachable state: if “Start” holds, then along all outgoing paths, “Heat” eventually holds. AG( Start → AF Heat )

3、搜索状态空间 逻辑表达式转换： E(Exist): 对于某一个分支 U(Until): 直到某一状态 AG( Start → AF Heat ) 逻辑表达式转换： E(Exist): 对于某一个分支 U(Until): 直到某一状态 G(Global): 现在和以后所有状态 A(Always):对所有分支 F(Future): 现在和以后某一状态 X(Next-Time): AG α = ¬EF(¬α) AF α = A(true Uα) A(α Uβ)= …. ¬EF( Start Λ EG ¬ Heat )

¬EF( Start Λ EG ¬ Heat ) 1 2 4 3 5 7 6 start oven open door cook close 1.S(Start) ={2,5,6,7} 2.S(¬Heat)={1,2,3,5,6} 3.S’=S(¬Heat)={1,2,3,5,6} SCC={1,2,3,5}T={1,2,3,5} =>S(EG ¬Heat)={1,2,3,5} 4.S={2,5} 5.S={1,2,3,4,5,6,7} 6.S=Ø 1 ~Start ~Close ~Heat ~Error start oven open door cook close door open door 2 ~Start Close ~Heat ~Error 4 Start ~Close ~Heat Error 3 ~Start Close Heat ~Error open door close door start oven start cooking reset 5 7 6 Start Close ~Heat Error Start Close ~Heat ~Error Start Close Heat ~Error warmup

Needham-Schroeder 身份认证协议 利用 Promela （protocol meta language）语言描述系统模型： (http://www.loria.fr/~merz/papers/NeedhamSchroder.spin) mtype = {msg1, msg2, msg3, alice, bob, intruder, nonceA, nonceB, nonceI, keyA, keyB, keyI, ok}; typedef Crypt { /* the encrypted part of a message */ mtype key, d1, d2; } chan network = [0] of {mtype, /* msg# */ mtype, /* receiver */ Crypt}; mtype partnerA, partnerB; mtype statusA, statusB; /* Knowledge about nonces gained by the intruder. */ bool knowNA, knowNB;

active proctype Alice() { /* honest initiator for one protocol run */ mtype partner_key, partner_nonce; Crypt data; if /* nondeterministically choose a partner for this run */ :: partnerA = bob; partner_key = keyB; :: partnerA = intruder; partner_key = keyI; fi; d_step { /* Construct msg1 and send it to chosen partner */ data.key = partner_key; data.d1 = alice; data.d2 = nonceA; } network ! msg1(partnerA, data);

/* wait for partner to send back msg2 and decipher it */ network ? msg2(alice, data); end_errA: /* make sure the partner used A's key and that the first nonce matches, otherwise block. */ (data.key == keyA) && (data.d1 == nonceA); partner_nonce = data.d2; d_step { /* respond with msg3 and declare success */ data.key = partner_key; data.d1 = partner_nonce; data.d2 = 0; } network ! msg3(partnerA, data); statusA = ok; } /* proctype Alice() */

active proctype Bob() { /* honest responder for one run */ mtype partner_key, partner_nonce; Crypt data; network ? msg1(bob, data); end_errB1: (data.key == keyB); partnerB = data.d1; d_step { partner_nonce = data.d2; if :: (partnerB == alice) -> partner_key = keyA; :: (partnerB == bob) -> partner_key = keyB; /* shouldn't happen */ :: (partnerB == intruder) -> partner_key = keyI; fi; /* respond with msg2 */ data.key = partner_key; data.d1 = partner_nonce; data.d2 = nonceB; } network ! msg2(partnerB, data); /* wait for msg3, check the key and the nonce, and declare success */ network ? msg3(bob, data); end_errB2: (data.key == keyB) && (data.d1 == nonceB); statusB = ok;

active proctype Intruder() { mtype msg; Crypt data, intercepted; mtype icp_type; /* type of intercepted message */ do :: /* Send msg1 to B (sending it to anybody else would be foolish). May use own identity or pretend to be A; send some nonce known to I.*/ if /* either replay intercepted message or construct a fresh message */ :: icp_type == msg1 -> network ! msg1(bob, intercepted); :: data.key = keyB; if :: data.d1 = alice; :: data.d1 = intruder; fi; :: knowNA -> data.d2 = nonceA; :: knowNB -> data.d2 = nonceB; :: data.d2 = nonceI; network ! msg1(bob, data); ……

network ? msg (_, data) -> if /* Perhaps store the data field for later use */ :: d_step { intercepted.key = data.key; intercepted.d1 = data.d1; intercepted.d2 = data.d2; icp_type = msg; } :: skip; fi; d_step { if /* Try to decrypt the message if possible */ :: (data.key == keyI) -> /* Have we learnt a new nonce? */ if :: (data.d1 == nonceA || data.d2 == nonceA) -> knowNA = true; :: else -> skip; :: (data.d1 == nonceB || data.d2 == nonceB) -> knowNB = true; od;

模型检测缺点（用于软件模型检测）： 空间爆炸：值域太泛 检验性质： G( (statusA = ok Λ statusB = ok) => (partnerA = bob  partnerB = alice) ) 模型检测缺点（用于软件模型检测）： 空间爆炸：值域太泛

四、模型检测工具 1、SMV 2、SPIN 3、其它工具

1、SMV 美国CMU计算机学院的L.McMillian 博士于1992年开发 基于“符号模型检验”（Symbolic Model Checking）技术 SMV早期是为了研究符号模型检测应用的可能性而开发的 一种对硬件进行检测的一种实验工具 一个SMV程序由两部分组成： 一个有限状态转换系统和一组CTL公式 把初始状态和转换关系表示成二叉决策树图 BDDs(Binary Diciding Diagrams) 属性也就是CTL公式，也表示成BDDs， 通过模型检测算法搜索系统状态空间，给出结果： 一个声明的属性是正确的， 或者是不正确的并给出一个反例

2、SPIN 由贝尔实验室的形式化方法与验证小组 于1980年开始开发的模型检测工具 建模方式：使用Promela语言建模，整个系统可以看作是一组同步的可扩展的有限状态机 模型检测器：可当做一个完整的LTL（Linear Temporal Logic）模型检验系统来使用，支持所有的可用的线性时态逻辑表示的正确性验证要求，也可以在有效的on-the-fly检验系统中用来检验协议的安全特征 其他的特征：将偏序简约（partial order reductions）技术、Bit State Hashing方法和线性时序逻辑有效的结合使用 适合用于：通信协议的检测和线性时序逻辑模型检测

3、其它工具 PROD Perti 网工具：INA、Lola、PEP、Design/CPN… 建模方式：基于Pr/T Petri网，有自己的对Pr/T Petri网的描述语言 分析方式：实现可达图的CTL模型检测以及基于on-the-fly方法的LTL验证 Perti 网工具：INA、Lola、PEP、Design/CPN… Uppaal和Kronos：是用于时控系统的模型检测工具 Caesar Aldebaran(CADP)：是基于LTSs的一组模型检测工具 Java Pathfinder 2：是Java程序检测器 Slam：一个检测C程序的检测工具