模型检验模型检验 1/36高级软件工程高级软件工程第八讲第八讲模型检验模型检验主要考虑如何发现设计缺陷！1模型检验模型检验 2/36高级软件工程高级软件工程一、例子二、模型检测概述三、模型检测算法概览四、模型检测工具内内 容容2模型检验模型检验 3/36高级软件工程高级软件工程Needham-Schroeder 身份认证协议身份认证协议N, S1ZS1, S2NS2Z通信过程可能被窃听！加密可以防止窃听！如何约定加密数字？每人 有自己的标识：N每人 公布自己的公钥: 只有N才能解开的消息： *N每个对话过程 用一对数字对内容加密: S1, S2每次对话前 需要首先建立这对数字该协议于1978年被提出并得到广泛应用NZ一、例子一、例子3模型检验模型检验 4/36高级软件工程高级软件工程N, S1WS1, S2NS2WN, S1ZS1, S2NS2Z1996年，发现该协议存在设计缺陷：年，发现该协议存在设计缺陷：攻击者可以伪装一方的身份攻击者可以伪装一方的身份利用模型检测方法！利用模型检测方法！被欺骗！被欺骗！不可信！不可信！开始伪装开始伪装ZWN4模型检验模型检验 5/36高级软件工程高级软件工程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.5模型检验模型检验 6/36高级软件工程高级软件工程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.6模型检验模型检验 7/36高级软件工程高级软件工程 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 CSAR/ ALDBARAN toolbox.7模型检验模型检验 8/36高级软件工程高级软件工程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!8模型检验模型检验 9/36高级软件工程高级软件工程Richard Raimi used Motorolas 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.9模型检验模型检验 10/36高级软件工程高级软件工程 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.10模型检验模型检验 11/36高级软件工程高级软件工程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.11模型检验模型检验 12/36高级软件工程高级软件工程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.12模型检验模型检验 13/36高级软件工程高级软件工程ACM 2007年度图灵奖（Turing Award）Edmund M. Clarke, E Allen Emerson, Joseph Sifakisl1981年年，美国的，美国的Edmund Clarke和和Allen Emerson以及以及在法国的在法国的Sifakis分别提出了模型检测（分别提出了模型检测（Model Checking）的最初概念）的最初概念l他们开发了一套用于判断硬件和软件设计的理论模型他们开发了一套用于判断硬件和软件设计的理论模型是否满足规范的方法是否满足规范的方法l当系统检测失败时，还能利用它确定问题存在的位置当系统检测失败时，还能利用它确定问题存在的位置13模型检验模型检验 14/36高级软件工程高级软件工程软件设计模型？ 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) -Microsoft14模型检验模型检验 15/36高级软件工程高级软件工程二、模型检测概述二、模型检测概述1、基本情况、基本情况2、什么是模型检测、什么是模型检测3、基本思想、基本思想4、过程描述、过程描述15模型检验模型检验 16/36高级软件工程高级软件工程l产生产生 20世纪80年代初，Clarke, Emerson等提出了用于并发系统性质的CTL逻辑，设计了检测有穷状态系统是否满足给定CTL公式的算法l特性特性能给出反例自动化程度高l应用应用计算机硬件、通信协议、控制系统、安全认证协议、软件安全 等1、基本情况、基本情况16模型检验模型检验 17/36高级软件工程高级软件工程l定义定义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.”给定一个系统的有限状态模型，和一个逻辑性质，系统地检测：这个模型（含初始状态）满足该性质2、什么是模型检测、什么是模型检测17模型检验模型检验 18/36高级软件工程高级软件工程3、基本思想、基本思想 （1）用状态迁移系统(S)表示系统的行为，用模态/时序逻辑公式(F)描述系统的性质。 （2）“系统是否具有某种期望的性质”就转化数学问题“状态迁移系统S是否是公式F的一个模型？” 公式表示：S |= F? 对于有限状态迁移系统，这个问题是可以判定的。18模型检验模型检验 19/36高级软件工程高级软件工程4、过程描述、过程描述OKError traceor1、建立模型、建立模型Finite-state model2、描述系统性质、描述系统性质Temporal logic formula3、输入工具、输入工具Model Checker (F W)Line 5: Line 12: Line 15:Line 21:Line 25:Line 27: Line 41:Line 47:19模型检验模型检验 20/36高级软件工程高级软件工程三、模型检测算法概览三、模型检测算法概览1、系统的表示、系统的表示2、属性的表示、属性的表示3、搜索状态空间、搜索状态空间2个例子：CTL 与 LTL20模型检验模型检验 21/36高级软件工程高级软件工程例子例子例子例子: :微波炉系统微波炉系统微波炉系统微波炉系统StartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatError1324675start ovenopen dooropen doorclose dooropen doorcookwarmupstart ovenresetstart cookingclose door1、系统的表示、系统的表示21模型检验模型检验 22/36高级软件工程高级软件工程2、属性表示、属性表示(Property Specification)用各种模态用各种模态/时序逻辑表示：时序逻辑表示：计算树逻辑（计算树逻辑（CTL: Computation Tree Logic）线性时序逻辑线性时序逻辑 （LTL: Linear Temporal Logic）模态命题模态命题 u -演算（演算（u-Calculus）For any reachable state: if “Start” holds, then along all outgoing paths, “Heat” eventually holds.AG( Start AF Heat )主要检测属性类型：主要检测属性类型：安全性（安全性（safety）：坏的事情不会发生。例如：无死锁）：坏的事情不会发生。例如：无死锁活性（活性（liveness）：好的事情终会发生。例如：请求响应）：好的事情终会发生。例如：请求响应公平性（公平性（fairness）：）：一致性（一致性（consistency）：）：22模型检验模型检验 23/36高级软件工程高级软件工程3、搜索状态空间、搜索状态空间逻辑表达式转换：E(Exist): 对于某一个分支U(Until): 直到某一状态G(Global): 现在和以后所有状态 A(Always):对所有分支F(Future): 现在和以后某一状态X(Next-Time):EF( Start EG Heat )AG = EF()AF = A(true U)A( U)= .AG( Start AF Heat )23模型检验模型检验 24/36高级软件工程高级软件工程StartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatError1324675start ovenopen dooropen doorclose dooropen doorcookwarmupstart ovenresetstart cookingclose doorEF( Start EG Heat )1.S(Start) =2,5,6,72.S(Heat)=1,2,3,5,63.S=S(Heat)=1,2,3,5,6 SCC=1,2,3,5T=1,2,3,5 =S(EG Heat)=1,2,3,54.S=2,55.S=1,2,3,4,5,6,76.S=24模型检验模型检验 25/36高级软件工程高级软件工程Needham-Schroeder 身份认证协议身份认证协议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;(http:/www.loria.fr/merz/papers/NeedhamSchroder.spin)利用 Promela （protocol meta language）语言描述系统模型：25模型检验模型检验 26/36高级软件工程高级软件工程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);26模型检验模型检验 27/36高级软件工程高级软件工程 /* wait for partner to send back msg2 and decipher it */ network ? msg2(alice, data); end_errA: /* make sure the partner used As 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() */27模型检验模型检验 28/36高级软件工程高级软件工程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; /* shouldnt 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;28模型检验模型检验 29/36高级软件工程高级软件工程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;if: knowNA - data.d2 = nonceA;: knowNB - data.d2 = nonceB;: data.d2 = nonceI;fi; network ! msg1(bob, data); fi;29模型检验模型检验 30/36高级软件工程高级软件工程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; fi; if : (data.d1 = nonceB | data.d2 = nonceB) - knowNB = true; : else - skip; fi;: else - skip;fi; od;30模型检验模型检验 31/36高级软件工程高级软件工程检验性质：检验性质：G( (statusA = ok statusB = ok) = (partnerA = bob partnerB = alice) )模型检测缺点（用于软件模型检测）：模型检测缺点（用于软件模型检测）：空间爆炸：值域太泛空间爆炸：值域太泛31模型检验模型检验 32/36高级软件工程高级软件工程1、SMV2、SPIN3、其它工具四、模型检测工具四、模型检测工具32模型检验模型检验 33/36高级软件工程高级软件工程1、SMV美国美国CMU计算机学院的计算机学院的L.McMillian 博士于博士于1992年开发年开发基于基于“符号模型检验符号模型检验”（Symbolic Model Checking）技术）技术SMV早期是为了研究符号模型检测应用的可能性而开发的早期是为了研究符号模型检测应用的可能性而开发的一种对硬件进行检测的一种实验工具一种对硬件进行检测的一种实验工具一个一个SMV程序由两部分组成：程序由两部分组成： 一个有限状态转换系统和一组一个有限状态转换系统和一组CTL公式公式把初始状态和转换关系表示成二叉决策树图把初始状态和转换关系表示成二叉决策树图 BDDs(Binary Diciding Diagrams)属性也就是属性也就是CTL公式，也表示成公式，也表示成BDDs，通过模型检测算法搜索系统状态空间，给出结果：通过模型检测算法搜索系统状态空间，给出结果：一个声明的属性是正确的，一个声明的属性是正确的，或者是不正确的并给出一个反例或者是不正确的并给出一个反例33模型检验模型检验 34/36高级软件工程高级软件工程2、SPIN由贝尔实验室的形式化方法与验证小组由贝尔实验室的形式化方法与验证小组于于1980年开始开发的模型检测工具年开始开发的模型检测工具建模方式：使用建模方式：使用Promela语言建模，整个系统可以看作是一组语言建模，整个系统可以看作是一组同步的可扩展的有限状态机同步的可扩展的有限状态机模型检测器：可当做一个完整的模型检测器：可当做一个完整的LTL（Linear Temporal Logic）模型检验系统来使用，支持所有的可用的线性时态逻辑）模型检验系统来使用，支持所有的可用的线性时态逻辑表示的正确性验证要求，也可以在有效的表示的正确性验证要求，也可以在有效的on-the-fly检验系统中检验系统中用来检验协议的安全特征用来检验协议的安全特征其他的特征：将偏序简约（其他的特征：将偏序简约（partial order reductions）技术、）技术、Bit State Hashing方法和线性时序逻辑有效的结合使用方法和线性时序逻辑有效的结合使用适合用于：通信协议的检测和线性时序逻辑模型检测适合用于：通信协议的检测和线性时序逻辑模型检测 34模型检验模型检验 35/36高级软件工程高级软件工程3、其它工具、其它工具PROD建模方式：基于Pr/T Petri网，有自己的对Pr/T Petri网的描述语言 分析方式：实现可达图的CTL模型检测以及基于on-the-fly方法的LTL验证 Perti 网工具：INA、Lola、PEP、Design/CPNUppaal和Kronos：是用于时控系统的模型检测工具Caesar Aldebaran(CADP)：是基于LTSs的一组模型检测工具Java Pathfinder 2：是Java程序检测器Slam：一个检测C程序的检测工具35