[Busec] PhD Oral Area Exam by Rick Skowyra (April 23 @ 2:00pm, MCS-148)

Bestavros, Azer best at bu.edu
Tue Apr 17 11:55:34 EDT 2012


Computer Science Department / College of Arts and Sciences

PhD Oral Area Exam of Rick Skowyra

Monday April 23, 2:00pm - 3:30pm
Location: MCS-148


Model Checking Techniques for Protocol Design and Analysis

Rick Skowyra
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.

Examination Committee:
Azer Bestavros, Ran Canetti, and Assaf Kfoury.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://cs-mailman.bu.edu/pipermail/busec/attachments/20120417/b9e9991f/attachment-0001.html 

More information about the Busec mailing list