Investigating Correct-by-Construction Attack-Tolerant Systems
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
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
that the generated code satisfies formal properties.
bibTex ref: CBV10 cite link