Model Checking: A Tutorial Overview - USF

1 Model checking : A Tutorial OverviewStephan MerzInstitut f ur Informatik, Universit at M survey principles of Model checking techniques for the automaticanalysis of reactive systems. The use of Model checking is exemplified by ananalysis of the Needham-Schroeder public key protocol. We then formally de-fine transition systems, temporal logic, -automata, and their relationship. Basicmodel checking algorithms for linear- and branching-time temporal logics are de-fined, followed by an introduction to symbolic Model checking and partial-orderreduction techniques. The paper ends with a list of references to some more ad-vanced IntroductionComputerized systems pervade more and more our everyday lives.

2 We rely on digitalcontrollers to supervise critical functions of cars, airplanes, and industrial plants. Dig-ital switching technology has replaced analog components in the telecommunicationindustry, and security protocols enable e-commerce applications and privacy. Whereimportant investments or even human lives are at risk, quality assurance for the under-lying hardware and software components becomes paramount, and this requires formalmodels that describe the relevant part of the systems at an adequate level of abstrac-tion. The systems we are focussing on are assumed to maintain an ongoing interactionwith their environment ( , the controlled system or other components of a communi-cation network) and are therefore calledreactive systems[60,94].

3 Traditional modelsthat describe computer programs as computing some result from given input valuesare inadequate for the description of reactive systems. Instead, the behavior of reactivesystems is usually modelled by transition term Model checking designates a collection of techniques for the automaticanalysis of reactive systems. Subtle errors in the design of safety-critical systems thatoften elude conventional simulation and testing techniques can be (and have been)found in this way. Because it has been proven cost-effective and integrates well withconventional design methods, Model checking is being adopted as a standard procedurefor the quality assurance of reactive inputs to a Model checker are a (usually finite-state) description of the system tobe analysed and a number of properties, often expressed as formulas of temporal logic,that are expected to hold of the system.

4 The Model checker either confirms that theproperties hold or reports that they are violated. In the latter case, it provides a counter-example: a run that violates the property. Such a run can provide valuable feedbackand points to design errors. In practice, this view turns out to be somewhat idealized:quite frequently, available resources only permit to analyse a rather coarse Model ofthe system. A positive verdict from the Model checker is then of limited value becausebugs may well be hidden by the simplifications that had to be applied to the the other hand, counter-examples may be due to modelling artefacts and no longercorrespond to actual system runs.

5 In any case, one should keep in mind that the objectof analysis is always anabstract modelof the system. Standard procedures such ascode reviews are necessary to ensure that the abstract Model adequately reflects thebehavior of the concrete system in order for the properties of interest to be establishedor falsified. Model checkers can be of some help in this validation task because it ispossible to perform sanity checks , for example to ensure that certain runs are indeedpossible or that the Model is free of paper is intended as a Tutorial Overview of some of the fundamental princi-ples of Model checking , based on a necessarily subjective selection of the large body ofmodel checking literature.

6 We begin with a case study in section2where the applicationof Model checking is considered from a user s point of view. Section3reviews transi-tion systems, temporal logics, and automata-theoretic techniques that underly some ap-proaches to Model checking . Section4introduces basic Model checking algorithms forlinear-time and branching-time logics. Finally, section5collects some rather sketchyreferences to more advanced topics. Much more material can be found in other contri-butions to this volume and in the textbooks and survey papers [27,28,69,97,124] onthe subject. The paper contains many references to the relevant literature, in the hopethat this survey can also serve as an annotated Analysis of a Cryptographic Description of the ProtocolLet us first consider, by way of example, the analysis of a public-key authentication pro-tocol suggested by Needham and Schroeder [104] using the Model checker SPIN[65].

7 Two agents A(lice) and B(ob) try to establish a common secret over an insecure channelin such a way that both are convinced of each other s presence and no intruder can gethold of the secret without breaking the underlying encryption algorithm. This is one ofthe fundamental problems in cryptography: for example, a shared secret could be usedto generate a session key for subsequent communication between the protocol is pictorially represented in requires the exchange of threemessages between the participating agents. Notation such as M Cdenotes that mes-sageMis encrypted using agentC s public key. Throughout, we assume the underlyingencryption algorithm to be secure and the private keys of the honest agents to be un-compromised.

8 Therefore, only agentCcan decrypt M Cto initiates the protocol by generating a random numberNAand sending themessage A,NA Bto Bob (numbers such asNAare callednoncesin cryptographicjargon, indicating that they should be used only once by any honest agent). The first1 The original protocol includes communication between the agents and a central key server todistribute the public keys of the agents. We concentrate on the core authentication protocol,assuming all public keys to be known to all agents."!# A"!# Bs1. A,NA B 2. NA,NB A33. NB BFig. public-key of the message informs Bob of the identity of the initiator. The secondcomponent represents one half of the similarly generates a nonceNBand responds with the message NA,NB presence of the nonceNAgenerated in the first step, which only Bob couldhave decrypted, convinces Alice of the authenticity of the message.

9 She thereforeaccepts the pair NA,NB as the common , Alice responds with the message NB B. By the same argument as above,Bob concludes that this message must originate with Alice, and therefore also ac-cepts NA,NB as the common assume all messages to be sent over an insecure medium. Attackers may inter-cept messages, store them, and perhaps replay them later. They may also participate inordinary runs of the protocol, initiate runs or respond to runs initiated by honest agents,who need not be aware of their partners true identity. However, even an attacker canonly decrypt messages that were encrypted with his own public protocol contains a severe flaw, and the reader is invited to find it before con-tinuing.

10 The error was discovered some 17 years after the protocol was first published,using Model checking technology [91]. A PROMELAM odelWe represent the protocol in PROMELA( protocol meta language ), the input languagefor the SPIN Model order to make the analysis feasible, we make a numberof simplifying assumptions: We consider a network of only three agents: A, B, and I(ntruder). The honest agents A and B can only participate in one protocol run each. Agent Acan only act as initiator, and agent B as responder. It follows that A and B need togenerate at most one nonce. The memory of agent I is limited to a single full code is available from the the protocol is very small, our simplifications are quite typical of theanalysis of real-world systems via Model checking : models are usually required tobe finite-state, and the complexity of analysis typically depends exponentially on thesize of those models.