Investigating Correct-by-Construction Attack-Tolerant Systems
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.