SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Combining System Properties: A Cautionary Example and Formal Examination
 by Dr. John Rushby.

Abstract
This report presents a simple example to demonstrate that the composition of a "fault-tolerant" service and a "secure" service does not necessarily provide a secure and fault-tolerant service.

The example is originally due to Peleska, who argues that to achieve the combined service, it is necessary to strengthen one of the individual services to address both concerns. In contrast, I argue that the individual services should be "deconstructed" into smaller and weaker components that can be reassembled in different ways, and I show that the combined service can be achieved by composing the fault-tolerant service with a weaker version of the secure service.

The report also provides an introduction to the use of mechanized formal state exploration methods (specifically, the MurΦ system from Stanford) for the purpose of examining and debugging protocols.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy