[Busec] PhD Oral Area Exam by Rick Skowyra (Today @ 2:00pm, MCS-148)
best at bu.edu
Mon Apr 23 08:47:31 EDT 2012
Computer Science Department / College of Arts and Sciences
PhD Oral Area Exam of Rick Skowyra
Monday April 23, 2:00pm - 3:30pm
Model Checking Techniques for Protocol Design and Analysis
In recent years, outsourcing of data and computation to cloud environments has prompted the development of many new networking, data management, and distributed systems protocols. Due to the potentially high financial value of information in the cloud, as well as legal and regulatory implications for its leakage or loss, these protocols must often guarantee enforcement of strong availability, integrity, confidentiality, and privacy properties. To this end, verification techniques for checking system implementations against their specifications are increasingly used to catch violations of such properties before a protocol is deployed.
While theorem provers like Coq and Isabelle have been used in the past to perform this verification, the substantial amount of time and effort required to employ these tools has limited their adoption. Instead, model checking has often been used to expose protocol flaws. A model checker compares an incomplete model of the system under evaluation against a set of properties inherited from its specification. Counter-examples to these properties (bugs) are then searched for by exploring the state-space of all possible execution paths defined by the model. This approach is sound, but not complete: a counter-example found by model checking is guaranteed to be a real bug, but the lack of any counter-examples in the checked model does not prove the implementation is bug-free. Model checking has been used to find bugs in a large number of deployed protocols, ranging from cryptographic authentication schemes to transport and application layer protocols.
In this talk, I will discuss three model checkers that collectively span the design space. I will focus on the formal logics they support, the kind of problems which are most amenable to being modeled in their syntax, and the mechanisms by which the model checker formalizes a model and searches for counter examples. I will also present a survey of protocols in which model checkers have found severe flaws, attacks, or unexpected behavior.
Azer Bestavros, Ran Canetti, and Assaf Kfoury
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Busec