CRASH Methodology for Correct-by-construction Attack-tolerant Systems
Also see the: CRASH Project Home | About CRASH | Software | People | Publications
Background
Our method uses formal proofs of high-level system requirements then synthesizes to synthesize code from the proofsproven specification. Within our method work on distributed systems we use the following concepts:
- Logic of Events: a simple formal theory of mathematical structure corresponding to message sequence diagrams
- Logic of Events presentation at LADA 2012 by Robert Constable, Mark Bickford, and Vincent Rahli. 2012
- Automated Proof of Authentication Protocols in a Logic of Events by Mark Bickford. 2010
- A Causal Logic of Events in Formalized Computational Type Theory by Mark Bickford, Robert L. Constable. 2005
- Event Classes: abstract description of processes
- Investigating Correct-by-Construction Attack-Tolerant Systems by Robert Constable, Mark Bickford, Robbert Van Renesse. 2010
- Generating Event Logics with Higher-Order Processes as Realizers by Mark Bickford, Robert L. Constable, David Guaspari. 2010
- Component Specification Using Event Classes by Mark Bickford. 2009
The main tool we use is EventML which is a programming and specification language. EventML, built by Vinvent Vincent Rahli, cooperates with the Nuprl interactive theorem prover at every stage of program development to help programmers ensure correctness, document the code, and support modifications and improvements. It generates an Inductive Logical Form that proves the specification and can also automatically synthesize code.
- Resources for EventML
- EventML documentation and downloads available at http://www.nuprl.org/software/
- EventML Tutorial
- Example of 2/3 consensus in EventML
Code diversity is created during the process. We can introduce variants at : the EventML specification , and code synthesis.
For more details about the example below see Mark's presentation at the May 2012 CRASH meeting.
Methodology
To create correct-by-construction code we:
- Write the specification in EventML
- Automatically generate and prove an Inductive Logical Form of the specification
- Synthesize code
- Diversify and deploy code
For more details about the example below see Mark's presentation at the May 2012 CRASH meeting.
Example with Consensus
In this example we will look at Paxos consensus, focusing on specifying the Scout protocol.
Step 1 - We write the Scout specification in EventML
EventML uses classes from the Formal Digital Library to describe events and protocols.
Step 2 - Generate the Inductive Logical Form (ILF)from the Scout specification
Using Here EventML 's interface with Nuprlinterfaces with Nuprl's formal library and theorem prover. Using the distributed prover, we generate the ILFa proof of the protocol which results in a readable Inductive Logical Form. If there are any issues with the proof we revise the specification and reiterate the process with the ILF.
Step 3 - Synthesize Consensus Code
...
Engaging our diversity in classes and state machines we generate multiple verified versions of the code. Then the final step before deployment is to test the code in the EventML simulator. The result is a correct-by-construction synthesized version of Paxos with multiple code variants.
Example Deployment: ShadowDB
ShadowDB is a replicated database we , created by Nicolas Schiper, on top of a synthesized consensus core. The primary defines the order in which transaction updates are applied. When crashes occur, consensus is used to reconfigure the set of replicas and agree on a prefix of executed transactions.
