CRASH Methodology for Correct-by-construction Attack-tolerant Systems
Background
Our method relies on using EventML. EventML 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. More about EventML is at http://www.nuprl.org/software/ and for additional examples see the EventML Tutorial
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
We introduce diversity at multiple steps in the process:
- EventML specification
- Code synthesis
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
Step 2 - Generate the Inductive Logical Form (ILF)from the Scout specification
Using EventML's interface with Nuprl, we generate the ILF. If there are any issues with the proof we revise the specification and reiterate the process with the ILF.
Step 3 - Synthesize Consensus Code
Using EventML's correct-by-construction synthesizer we generate code from the specification.
Step 4 - Diversify & Deploy
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.
Example Deployment: ShadowDB
ShadowDB is a replicated database we created 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.
