5 lines
2.2 KiB
TeX
5 lines
2.2 KiB
TeX
Distributed protocols are the foundation for the modern internet, and therefore ensuring their correctness and security is paramount. To this end, formal methods, the use of mathematically rigorous techniques for reasoning about software, has been increasingly employed to analyze and study distributed protocols. Historically, formal methods has been employed for reasoning about concurrency and distributed algorithms \cite{Lamport_1994, Holzmann_1997, Clarke_Wang}, and in recent years formal methods have been employed at scale to reason about the security of cryptographic protocols and primitives \cite{Basin_Cremers_Dreier_Sasse_2022, Blanchet_Smyth_Cheval_Sylvestre, Kobeissi_Nicolas_Tiwari, Blanchet_Jacomme, Basin_Linker_Sasse}.
|
|
This myriad of formal methods tooling applicable to secure protocols has enabled reasoning about security-relevant properties involving secrecy, authentication, indistinguishability in addition to concurrency, safety, and liveness. However, no previous formal methods tooling offered an effective solution for rigorously studying an attacker that controls communication channels. That is, how do you reason about an attacker that can arbitrarily drop, reorder, replay, or insert messages onto a communication channel?
|
|
|
|
To fill this gap, we introduce \korg, a tool for synthesizing attacks on distributed protocols that implements the theoretical framework proposed in Hippel et al. \cite{Hippel2022}. In particular, \korg targets the communication channels between the protocol endpoints, and synthesizes attacks to violate arbitrary linear temporal logic (LTL) specifications. \korg either synthesizes attack, or proves the absence of such via an exhaustive state-space search. \korg is sound and complete, meaning if there exists an attack \korg will find it, and \korg will never have false positives. \korg supports pre-defined attacker models, including attackers that can replay, reorder, or drop messages on channels, as well as custom user-defined attacker models. Although \korg best lends itself for reasoning about denial of service attacks, it can target any specification expressable in LTL. We present a variety of case studies illustrating the employability and usefulness of \korg.
|