Automated Attacker Synthesis for Distributed Protocols
This work addresses the challenge of ensuring robustness in distributed protocols against attacks, though it is incremental as it builds on formal methods for security analysis.
The paper tackles the problem of automatically synthesizing adversarial processes that can cause distributed protocols to malfunction, given a formal threat model, and demonstrates that their prototype KORG can generate well-known attacks for TCP within seconds or minutes.
Distributed protocols should be robust to both benign malfunction (e.g. packet loss or delay) and attacks (e.g. message replay) from internal or external adversaries. In this paper we take a formal approach to the automated synthesis of attackers, i.e. adversarial processes that can cause the protocol to malfunction. Specifically, given a formal threat model capturing the distributed protocol model and network topology, as well as the placement, goals, and interface (inputs and outputs) of potential attackers, we automatically synthesize an attacker. We formalize four attacker synthesis problems - across attackers that always succeed versus those that sometimes fail, and attackers that attack forever versus those that do not - and we propose algorithmic solutions to two of them. We report on a prototype implementation called KORG and its application to TCP as a case-study. Our experiments show that KORG can automatically generate well-known attacks for TCP within seconds or minutes.