第八讲模型检验

第八讲模型检验主要考虑如何发现设计缺陷！1一、例子二、模型检测概述三、模型检测算法概览四、模型检测工具内容2Needham-Schroeder身份认证协议[N,S1]Z[S1,S2]N[S2]Z通信过程可能被窃听！加密可以防止窃听！如何约定加密数字？每人有自己的标识：N每人公布自己的公钥:只有N才能解开的消息：[****]N每个对话过程用一对数字对内容加密:S1,S2每次对话前需要首先建立这对数字该协议于1978年被提出并得到广泛应用NZ一、例子3[N,S1]W[S1,S2]N[S2]W[N,S1]Z[S1,S2]N[S2]Z1996年，发现该协议存在设计缺陷：攻击者可以伪装一方的身份利用模型检测方法！被欺骗！不可信！开始伪装ZWN4In1992ClarkeandhisstudentsatCMUusedSMVtoverifytheIEEEFuture+cachecoherenceprotocol.•Theyfoundanumberofpreviouslyundetectederrorsinthedesignoftheprotocol.•ThiswasthefirsttimethatformalmethodshavebeenusedtofinderrorsinanIEEEstandard.•Althoughthedevelopmentoftheprotocolbeganin1988,allpreviousattemptstovalidateitwerebasedentirelyoninformaltechniques.5In1992DillandhisstudentsatStanfordusedMurphitoverifythecachecoherenceprotocoloftheIEEEScalableCoherentInterface.•Theyfoundseveralerrors,rangingfromuninitializedvariablestosubtlelogicalerrors.•Theerrorsalsoexistedinthecompleteprotocol,althoughithadbeenextensivelydiscussed,simulated,andevenimplemented.6In1995researchersfromBullandVerimagusedLOTOStodescribetheprocessors,memorycontroller,andbusArbiterofthePowerScalemultiprocessorarchitecture.•Theyidentifiedfourcorrectnessrequirementsforproperfunctioningofthearbiter.•Thepropertieswereformalizedusingbisimulationrelationsbetweenfinitelabeledtransitionsystems.•CorrectnesswasestablishedautomaticallyinafewminutesusingtheCÆSAR/ALDÉBARANtoolbox.7AHigh-levelDataLinkControllerwasbeingdesignedatAT&TinMadridin1996

•ResearchersatBellLabsofferedtochecksomepropertiesofthedesignusingtheFormalCheckverifier.•Withinfivehours,sixpropertieswerespecifiedandfivewereverified.

•Thesixthpropertyfailed,uncoveringabugthatwouldhavereducedthroughputorcausedlosttransmissions!8RichardRaimiusedMotorola’sVerdictmodelcheckertodebugahardwarelaboratoryfailure.•InitialsiliconofthePowerPC620microprocessorCrashedduringbootofanoperatingsystem.•Inamatterofseconds,VerdictfoundaBIUdeadlockcausingthefailure.9In1994Bosscher,Polak,andVaandragerwonabest-paperawardforprovingmanuallythecorrectnessofacontrolprotocolusedinPhilipsstereocomponents.•In1995HoandWong-ToiverifiedanabstractionofthisprotocolautomaticallyusingHyTech.•Laterin1995DawsandYovineusedKronostocheckallthepropertiesstatedandhandprovedbyBosscher,etal.10TheNewCoReProject(89-92)wasthefirstapplicationofformalverificationinasoftwareprojectwithinAT&T.•AspecialpurposemodelcheckerwasusedinthedevelopmentoftheCCITTISDNUserPartProtocol.•Five“verificationengineers”analyzed145requirements.•Atotalof7,500linesofSDLsourcecodewasverified.•112errorswerefound;about55%oftheoriginaldesignrequirementswerelogicallyinconsistent.11In1995theConcurrencyWorkbenchwasusedtoanalyzeanactivestructuralcontrolsystemtomakebuildingsmoreresistanttoearthquakes.•Thecontrolsystemsampledtheforcesbeingappliedtothestructureandusedhydraulicactuatorstoexertcountervailingforces.•Atimingerrorwasdiscoveredthatcouldhavecausedthecontrollertoworsen,ratherthandampen,thevibrationexperiencedduringearthquakes.12ACM2007年度图灵奖（TuringAward）EdmundM.Clarke,EAllenEmerson,JosephSifakis1981年，美国的EdmundClarke和AllenEmerson以及在法国的Sifakis分别提出了模型检测（ModelChecking）的最初概念他们开发了一套用于判断硬件和软件设计的理论模型是否满足规范的方法当系统检测失败时，还能利用它确定问题存在的位置13软件设计模型？•Statecharts……用于软件？软件代码？Usestaticanalysistoextractafinitestatesynchronizationskeletonfromtheprogram.Modelchecktheresult.•Bandera--KansasState•JavaPathFinder--NASAAmes•SlamProject(Bebop)--Microsoft14二、模型检测概述1、基本情况2、什么是模型检测3、基本思想4、过程描述15产生

20世纪80年代初，Clarke,Emerson等提出了用于并发系统性质的CTL逻辑，设计了检测有穷状态系统是否满足给定CTL公式的算法特性能给出反例自动化程度高应用计算机硬件、通信协议、控制系统、安全认证协议、软件安全等1、基本情况16定义[Clarke&Emerson1981] “Modelcheckingisanautomatedtechniquethat,givenafinite-statemodelofasystemandalogicalproperty,systematicallycheckswhetherthispropertyholdsfor(agiveninitialstatein)thatmodel.”给定一个系统的有限状态模型，和一个逻辑性质，系统地检测：这个模型（含初始状态）满足该性质2、什么是模型检测173、基本思想（1）用状态迁移系统(S)表示系统的行为，用模态/时序逻辑公式(F)描述系统的性质。（2）“系统是否具有某种期望的性质”就转化数学问题“状态迁移系统S是否是公式F的一个模型？”公式表示：S|=F?

对于有限状态迁移系统，这个问题是可以判定的。184、过程描述OKErrortraceor1、建立模型Finite-statemodel2、描述系统性质Temporallogicformula3、输入工具ModelChecker(FW)Line5:…Line12:…Line15:…Line21:…Line25:…Line27:……Line41:…Line47:…19三、模型检测算法概览1、系统的表示2、属性的表示3、搜索状态空间2个例子：CTL与LTL20例子:微波炉系统~Start~Close~Heat~ErrorStart~Close~HeatError~StartClose~Heat~Error~StartCloseHeat~ErrorStartClose~HeatErrorStartClose~Heat~ErrorStartCloseHeat~Error1324675startovenopendooropendoorclosedooropendoorcookwarmupstartovenresetstartcookingclosedoor1、系统的表示212、属性表示(PropertySpecification)用各种模态/时序逻辑表示：计算树逻辑（CTL:ComputationTreeLogic）线性时序逻辑（LTL:LinearTemporalLogic）模态命题u--演算（u-Calculus）Foranyreachablestate:if“Start”holds,thenalongalloutgoingpaths,“Heat”eventuallyholds.AG(Start→AFHeat)主要检测属性类型：安全性（safety）：坏的事情不会发生。例如：无死锁活性（liveness）：好的事情终会发生。例如：请求响应公平性（fairness）：一致性（consistency）：223、搜索状态空间逻辑表达式转换：E(Exist):对于某一个分支U(Until):直到某一状态G(Global):现在和以后所有状态A(Always):对所有分支F(Future):现在和以后某一状态X(Next-Time):¬EF(StartΛEG¬

Heat)AGα=¬EF(¬α)AFα

=A(trueUα)A(αUβ)=….AG(Start→AFHeat)23~Start~Close~Heat~ErrorStart~Close~HeatError~StartClose~Heat~Error~StartCloseHeat~ErrorStartClose~HeatErrorStartClose~Heat~ErrorStartCloseHeat~Error1324675startovenopendooropendoorclosedooropendoorcookwarmupstartovenresetstartcookingclosedoor¬EF(StartΛEG¬

Heat)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=Ø24Needham-Schroeder身份认证协议mtype={msg1,msg2,msg3,alice,bob,intruder,nonceA,nonceB,nonceI,keyA,keyB,keyI,ok};typedefCrypt{/*theencryptedpartofamessage*/mtypekey,d1,d2;}channetwork=[0]of{mtype,/*msg#*/mtype,/*receiver*/Crypt};mtypepartnerA,partnerB;mtypestatusA,statusB;/*Knowledgeaboutnoncesgainedbytheintruder.*/boolknowNA,knowNB;()利用Promela（protocolmetalanguage）语言描述系统模型：25activeproctypeAlice(){/*honestinitiatorforoneprotocolrun*/mtypepartner_key,partner_nonce;Cryptdata;if/*nondeterministicallychooseapartnerforthisrun*/::partnerA=bob;partner_key=keyB;::partnerA=intruder;partner_key=keyI;fi;d_step{/*Constructmsg1andsendittochosenpartner*/data.key=partner_key;data.d1=alice;data.d2=nonceA;}network!msg1(partnerA,data);26/*waitforpartnertosendbackmsg2anddecipherit*/network?msg2(alice,data);end_errA:/*makesurethepartnerusedA'skeyandthatthefirstnoncematches,otherwiseblock.*/(data.key==keyA)&&(data.d1==nonceA);partner_nonce=data.d2;d_step{/*respondwithmsg3anddeclaresuccess*/data.key=partner_key;data.d1=partner_nonce;data.d2=0;}network!msg3(partnerA,data);statusA=ok;}/*proctypeAlice()*/27activeproctypeBob(){/*honestresponderforonerun*/mtypepartner_key,partner_nonce;Cryptdata;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'thappen*/::(partnerB==intruder)->partner_key=keyI;fi;/*respondwithmsg2*/data.key=partner_key;data.d1=partner_nonce;data.d2=nonceB;}network!msg2(partnerB,data);/*waitformsg3,checkthekeyandthenonce,anddeclaresuccess*/network?msg3(bob,data);end_errB2:(data.key==keyB)&&(data.d1==nonceB);statusB=ok;}28activeproctypeIntruder(){mtypemsg;Cryptdata,intercepted;mtypeicp_type;/*typeofinterceptedmessage*/do::/*Sendmsg1toB(sendingittoanybodyelsewouldbefoolish).MayuseownidentityorpretendtobeA;sendsomenonceknowntoI.*/if/*eitherreplayinterceptedmessageorconstructafreshmessage*/::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;……29network?msg(_,data)->if/*Perhapsstorethedatafieldforlateruse*/::d_step{ intercepted.key=data.key; intercepted.d1=data.d1; intercepted.d2=data.d2;icp_type=msg; }::skip;fi;d_step{ if/*Trytodecryptthemessageifpossible*/ ::(data.key==keyI)->/*Havewelearntanewnonce?*/ 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检验性质：G((statusA=okΛst