Automated Attacker Synthesis for Distributed Protocols

摘要: Distributed protocols should be robust to both benign malfunction (e.g. packet loss or delay) and attacks message replay) from internal external adversaries. In this paper we take a formal approach the automated synthesis of attackers, i.e. adversarial processes that can cause protocol malfunction. Specifically, given threat model capturing distributed network topology, as well placement, goals, interface (inputs outputs) potential automatically synthesize an attacker. We formalize four attacker problems - across attackers always succeed versus those sometimes fail, attack forever do not propose algorithmic solutions two them. report on prototype implementation called KORG its application TCP case-study. Our experiments show generate well-known for within seconds minutes.