软件构件和中间件ppt课件

1、模型检验模型检验 1/36高级软件工程高级软件工程主要考虑如何发现设计缺陷！模型检验模型检验 2/36高级软件工程高级软件工程一、例子二、模型检测概述三、模型检测算法概览四、模型检测工具模型检验模型检验 3/36高级软件工程高级软件工程Needham-Schroeder 身份认证协议身份认证协议N, S1ZS1, S2NS2Z通信过程可能被窃听！加密可以防止窃听！如何约定加密数字？每人 有自己的标识：N每人 公布自己的公钥: 只有N才能解开的消息： *N每个对话过程 用一对数字对内容加密: S1, S2每次对话前 需要首先建立这对数字该协议于1978年被提出并得到广泛应用NZ一、例子一、例子模

2、型检验模型检验 4/36高级软件工程高级软件工程N, S1WS1, S2NS2WN, S1ZS1, S2NS2Z2019年，发现该协议存在设计缺陷：年，发现该协议存在设计缺陷：攻击者可以伪装一方的身份攻击者可以伪装一方的身份利用模型检测方法！利用模型检测方法！被欺骗！被欺骗！不可信！不可信！开始伪装开始伪装ZWN模型检验模型检验 5/36高级软件工程高级软件工程In 1992 Clarke and his students at CMU used SMV to verify the IEEE Future+ cache coherence protocol. They found a numb

3、er 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.模型检

4、验模型检验 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, altho

5、ugh it had been extensively discussed, simulated, and even implemented.模型检验模型检验 7/36高级软件工程高级软件工程 In 2019 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 requir

6、ements 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.模型检验模型检验 8/36高级软件工程高级软件工程A High-level Data Link Controller

7、was being designed at AT&T in Madrid in 2019 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 throu

8、gh put or caused lost transmissions!模型检验模型检验 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 c

9、ausing the failure.模型检验模型检验 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 2019 Ho and Wong-Toi verified an abstraction of this protocol automatically using HyTech. Late

10、r in 2019 Daws and Yovine used Kronos to check all the properties stated and hand proved by Bosscher, et al.模型检验模型检验 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 de

11、velopment 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.模型检验模型检验 12/36高级软件工程高级软件工程In 2019 the Concu

12、rrency 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 ca

13、used the controller to worsen, rather than dampen, the vibration experienced during earthquakes.模型检验模型检验 13/36高级软件工程高级软件工程Edmund M. Clarke, E Allen Emerson, Joseph Sifakis1981年，美国的年，美国的Edmund Clarke和和Allen Emerson以及以及在法国的在法国的Sifakis分别提出了模型检测分别提出了模型检测Model Checking的最初概念的最初概念他们开发了一套用于判断硬件和软件设计的理论模型是他们

14、开发了一套用于判断硬件和软件设计的理论模型是否满足规范的方法否满足规范的方法当系统检测失败时，还能利用它确定问题存在的位置当系统检测失败时，还能利用它确定问题存在的位置模型检验模型检验 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 -NAS

15、A Ames Slam Project (Bebop) -Microsoft模型检验模型检验 15/36高级软件工程高级软件工程1、基本情况、基本情况2、什么是模型检测、什么是模型检测3、基本思想、基本思想4、过程描述、过程描述模型检验模型检验 16/36高级软件工程高级软件工程l产生产生l 20世纪世纪80年代初，年代初，Clarke, Emerson等提出等提出了用于并发系统性质的了用于并发系统性质的CTL逻辑，设计了逻辑，设计了检测有穷状态系统是否满足给定检测有穷状态系统是否满足给定CTL公式公式的算法的算法l特性特性l能给出反例能给出反例l自动化程度高自动化程度高l运用运用l计算机硬件

16、、通信协议、控制系统、安全计算机硬件、通信协议、控制系统、安全认证协议、软件安全认证协议、软件安全 等等模型检验模型检验 17/36高级软件工程高级软件工程l定义定义Clarke & Emerson 1981l“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)

17、 that model.”l给定一个系统的有限状态模型，和一个逻辑给定一个系统的有限状态模型，和一个逻辑性质，系统地检测：这个模型含初始状态性质，系统地检测：这个模型含初始状态满足该性质满足该性质2、什么是模型检测、什么是模型检测模型检验模型检验 18/36高级软件工程高级软件工程3、基本思想、基本思想 （1用状态迁移系统用状态迁移系统(S)表示系统的行为，表示系统的行为，用模态用模态/时序逻辑公式时序逻辑公式(F)描述系统的性质。描述系统的性质。 （2）“系统是否具有某种期望的性质就转系统是否具有某种期望的性质就转化数学问题化数学问题“状态迁移系统状态迁移系统S是否是公式是否是公式F的一的一

18、个模型？个模型？” 公式表示：公式表示：S |= F? 对于有限状态迁移系统，这个问题是可以判定对于有限状态迁移系统，这个问题是可以判定的。的。模型检验模型检验 19/36高级软件工程高级软件工程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:模型检验模型检验 20/36高级软件工程高级软件工

19、程1、系统的表示、系统的表示2、属性的表示、属性的表示3、搜索状态空间、搜索状态空间2个例子：CTL 与 LTL模型检验模型检验 21/36高级软件工程高级软件工程StartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatError1324675start ovenopen dooropen doorclose dooropen doorcookwarmupstart ovenresetstart

20、cookingclose door1、系统的表示、系统的表示模型检验模型检验 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, “Hea

21、t” eventually holds.AG( Start AF Heat )主要检测属性类型：主要检测属性类型：安全性安全性safety）：坏的事情不会发生。例如：无死锁）：坏的事情不会发生。例如：无死锁活性活性liveness）：好的事情终会发生。例如：请求响应）：好的事情终会发生。例如：请求响应公平性公平性fairness）：）：一致性一致性consistency）：）：模型检验模型检验 23/36高级软件工程高级软件工程逻辑表达式转换：E(Exist): 对于某一个分支U(Until): 直到某一状态G(Global): 现在和以后所有状态 A(Always):对所有分支F(Futur

22、e): 现在和以后某一状态X(Next-Time):EF( Start EG Heat )AG = EF()AF = A(true U)A( U)= .AG( Start AF Heat )模型检验模型检验 24/36高级软件工程高级软件工程StartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatErrorStartCloseHeatError1324675start ovenopen dooropen doorclose dooro

23、pen 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=模型检验模型检验 25/36高级软件工程高级软件工程mtype = msg1, msg2, msg3, alice, bob, intruder, nonceA, nonceB, nonceI,

24、 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;(loria.fr/merz/papers/

25、NeedhamSchroder.spin)利用 Promela （protocol meta language语言描述系统模型：模型检验模型检验 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

26、; : 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);模型检验模型检验 27/36高级软件工程高级软件工程 /* wait for partner to send back msg2 and decipher it */ network ? msg2(alic

27、e, 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

28、 ! msg3(partnerA, data); statusA = ok; /* proctype Alice() */模型检验模型检验 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; i

29、f : (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, c

30、heck the key and the nonce, and declare success */ network ? msg3(bob, data); end_errB2: (data.key = keyB) & (data.d1 = nonceB); statusB = ok;模型检验模型检验 29/36高级软件工程高级软件工程active proctype Intruder() mtype msg; Crypt data, intercepted; mtype icp_type; /* type of intercepted message */ do : /* Send ms

31、g1 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

32、= intruder;fi;if: knowNA - data.d2 = nonceA;: knowNB - data.d2 = nonceB;: data.d2 = nonceI;fi; network ! msg1(bob, data); fi;模型检验模型检验 30/36高级软件工程高级软件工程network ? msg (_, data) - if /* Perhaps store the data field for later use */ : d_step intercepted.key = data.key; intercepted.d1 = data.d1; intercep

33、ted.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; : els

34、e - skip; fi;: else - skip;fi; od;模型检验模型检验 31/36高级软件工程高级软件工程检验性质：检验性质：G( (statusA = ok statusB = ok) = (partnerA = bob partnerB = alice) )模型检测缺点用于软件模型检测）：模型检测缺点用于软件模型检测）：空间爆炸：值域太泛空间爆炸：值域太泛模型检验模型检验 32/36高级软件工程高级软件工程1、SMV2、SPIN3、其它工具模型检验模型检验 33/36高级软件工程高级软件工程1、SMV美国美国CMU计算机学院的计算机学院的L.McMillian 博士于博士于1992年开发年开发基于基于“符号模型检验符号模型检验”（Symbolic Model Checking技术技术SMV早期是为了研究符号模型检测应用的可能早期是为了研究符号模型检测应用的可能性而开发的性而开发的一种对硬件进