Portal de Periódicos da CAPES

Automated Attacker Synthesis for Distributed Protocols

2020; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-030-54549-9_9

1611-3349

Max von Hippel, Cole Vick, Stavros Tripakis, Cristina Nita-Rotaru,

Formal Methods in Verification

Distributed protocols should be robust to both benign malfunction (e.g. packet loss or delay) and attacks (e.g. message replay). 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 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 may attack forever versus those that may 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.