CRASH Methodology

...

for Correct-by-construction Attack-tolerant Systems

To create correct-by-construction code we:

1. Write the secification in EventML
2. Automatically generate and prove an Inductive Logical Form of the specification
3. Synthesize code
4. Diversify and deploy code

We introduce diversity at multiple steps in the process:

• EventML specification
• Code synthesis

...