[NRG] Reminder: NRG meeting: Model Checking Techniques for Protocol Desig... @ Mon Apr 23 2pm - 3pm (NRG Calendar)

Google Calendar calendar-notification at google.com
Sun Apr 22 13:59:49 EDT 2012

This is a reminder for:

Title: NRG meeting: Model Checking Techniques for Protocol Design and  
Please notice that we are meeting later this time because this is also  
Rick's Oral Exam.

Presenter: 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  

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.
When: Mon Apr 23 2pm – 3pm Eastern Time
Where: MCS-148, 111 Cummington Street, Boston, MA 02215
Calendar: NRG Calendar
     * michel.machado at gmail.com - creator

Event details:  

Invitation from Google Calendar: https://www.google.com/calendar/

You are receiving this email at the account nrg-l at cs.bu.edu because you set  
a reminder for this event on the calendar NRG Calendar.

You can change your reminders for specific events in the event details page  
in https://www.google.com/calendar/.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://cs-mailman.bu.edu/pipermail/nrg-l/attachments/20120422/ab90aac2/attachment.html 

More information about the NRG-L mailing list