CRASH - Clean-slate Resilient Adaptive Secure Hosts
Publications
ShadowDB: A Replicated Database on a Synthesized Consensus Core
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
Eighth Workshop on Hot Topics in System Dependability. 2012.
Interfacing with Proof Assistants for Domain Specific Programming Using EventML
Vincent Rahli
Presented at User Interfaces for Theorem Provers July 2012 (UITP12)
On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer
Robert Constable
LICS 2012 June 2012 Invited. Article and lecture.
Proof Assistants and the Dynamic Nature of Formal Theories
Robert Constable
IJCAR Joint Workshops Invited June 2012. Article and lecture.
Type Theoretic Semantics for First-Order Logic
Robert Constable
The Constructive in Logic and Applications Conference Invited May 2012. Lecture.
Slide presentation on CRASH Methodology, from CRASH PI meeting May 2012
Mark Bickford
Slide presentation on CRASH Methodology from PI meeting, May. 2012
Mark Bickford
Slide presentation on Logic of Events, Jan. 2012
Mark Bickford
EventML Tutorial & Consensus Protocol March 2012
Mark Bickford, Robert L. Constable, Richard Eaton,
David Guaspari, and Vincent Rahli
EventML Manual & Introduction to Classic ML, 2011
by Christoph Kreitz and Vincent Rahli
Investigating Correct-by-Construction
Attack-Tolerant Systems, 2010
by Robert Constable, Mark Bickford, Robbert van Renesse
Attack-tolerant distributed systems change their protocols on-the-fly in response to apparent attacks from the environment; they substitute functionally equivalent versions possibly more resistant to detected threats. Alternative protocols can be packaged together as a single adaptive protocol or variants from a formal protocol library can be sent to threatened groups of processes. We are experimenting with libraries of attack-tolerant protocols that are correct-by-construction and testing them in environments that simulate specified threats, including constructive versions of the famous FLP imaginary adversary against fault-tolerant consensus. We expect that all variants of tolerant protocols are automatically generated and accompanied by machine checked proofs that the generated code satisfies formal properties.
Poster Slides for Correct by Construction Attack Tolerant Systems.
Kickoff Talk Slides from November 2010