CRASH - Clean-slate Resilient Adaptive Secure Hosts
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
by Vincent Rahli, Mark Bickford, and Abhishek Anand
4th Conference on Interactive Theorem Proving (ITP). Rennes, France. July 2013.
Byzantine Chain Replication
by Robbert van Renesse, Chi Ho, and Nicolas Schiper
16th International Conference On Principles Of DIstributed Systems (OPODIS). Rome, Italy. December 2012
A Diversified and Correct-by-Construction Broadcast Service
by Vincent Rahli, Nicolas Schiper, Robbert Van Renesse, Mark Bickford and Robert L. Constable
Presented at the 2nd International Workshop on Rigorous Protocol Engineering (WRiPE). Austin, TX. October 2012
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
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
LICS 2012 June 2012 Invited. Article and lecture.
Proof Assistants and the Dynamic Nature of Formal Theories
IJCAR Joint Workshops Invited June 2012. Article and lecture.
Type Theoretic Semantics for First-Order Logic
The Constructive in Logic and Applications Conference Invited May 2012. Lecture.
Slide presentation on CRASH Methodology, from CRASH PI meeting May 2012
Slide presentation on CRASH Methodology from PI meeting, May. 2012
Slide presentation on Logic of Events, Jan. 2012
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
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