Investigating correct-by-construction attack-tolerant systems

Abstract

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.