65 lines
7.1 KiB
TeX
65 lines
7.1 KiB
TeX
%!TEX root = ../main.tex
|
|
Distributed protocols are the lynchpin of the modern internet,
|
|
representing the fundamental communication and coordination backbone
|
|
of all modern services over the internet.
|
|
The vast importance of distributed protocols has motivated ample
|
|
research in ensuring their security, reliability, and
|
|
performance. One popular approach in prior literature
|
|
has been the employment of
|
|
\textit{formal methods}, the use of mathematically rigorous techniques,
|
|
to analyze and verify distributed protocols.
|
|
Formal methods has been applied to verify Raft \cite{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson, Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016, Ongaro_Ousterhout},
|
|
Paxos \cite{Delzanno_Tatarek_Traverso_2014, ironfleet, Rahli_Vukotic_Völp_Esteves-Verissimo_2018}, PBFT \cite{Sergey_Wilcox_Tatlock_2018, ironfleet}, and countless other distributed protocols \cite{Smith_1997, Narayana_Chen_Zhao_Chen_Fu_Zhou_2006, Arun_Arashloo_Saeed_Alizadeh_Balakrishnan_2021, Beurdouche}.
|
|
A common assumption among all the prior formal methods work is assuming
|
|
distributed protocols operate over \textit{imperfect} or
|
|
\textit{attacker-controlled} communication channels, where
|
|
messages can be arbitrarily dropped, replayed, or reordered, then proving
|
|
the targeted protocol maintains properties of interest with respect to them.
|
|
|
|
In this work, we take a fundamentally different approach to studying distributed protocols under imperfect channels. While previous work generally assumes one specific channel configuration and primarily seeks to manually construct proofs with respect to it, we study protocols under various channel configurations and seek to automatically discover interesting attack traces, counterexamples, and guarantees.
|
|
|
|
We introduce a general methodology for automatically discovering dropping, replay, reordering attacks traces on distributed protocols, and we introduce \korg, a highly generalizable tool for synthesizing attacks on distributed protocols that implements our methodology and the drop, replay, and reordering attacker models. \korg targets the communication channels between the protocol endpoints, and synthesizes attacks to violate general linear temporal logic (LTL) specifications. \korg is designed to either synthesize an attack, or prove 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 is also designed to be easy to use once the protocol model is constructed: all a user must do is select the victim channels, select the desired attacker models, and invoke \korg.
|
|
|
|
In this work we take an approach rooted in \textit{formal methods} and \textit{automated reasoning} to construct \korg. In particular, we employ \textit{model checking}, a sub-discipline of formal methods, to decidably and automatically find attacks in protocols or prove the absence of such.
|
|
|
|
We summarize our contributions:
|
|
|
|
\begin{itemize}
|
|
\item We present generalizable gadgets representing attackers capable of dropping, replaying, and reordering messages on communication channels of distributed protocols.
|
|
\item We present \korg, a tool for synthesizing attacks against distributed communication protocols. \korg supports four general attacker models: an attacker that can drop, replay, reorder, or insert messages on a channel.
|
|
\item We provide an overview of \korg and demonstrate its usage by walking through applying it to the ABP protocol
|
|
\item We present three case studies for three well-known protocols, TCP, Raft, and SCTP, illustrating the usefulness of \korg.
|
|
\end{itemize}
|
|
|
|
We release our code and our models as open source at \url{https://zenodo.org/records/14968780}.
|
|
%\url{https://anonymous.4open.science/r/attacksynth-artifact-1B5D}.
|
|
|
|
%Formal methods work typically assumes the communication channe
|
|
|
|
%One common assumption among all the prior work is assuming or explicitly defining some notion of an \textit{imperfect} or \textit{malicious} communication channel, then proving the target protocol maintains certain properties with respect to them.
|
|
|
|
|
|
|
|
% ======= OLD INTRODUCTION ========
|
|
\begin{comment}
|
|
|
|
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, Kobeissi_Nicolas_Tiwari, Blanchet_Jacomme, Basin_Linker_Sasse}.
|
|
%, Blanchet_Smyth_Cheval_Sylvestre
|
|
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 and extends the theoretical framework proposed in \cite{Hippel2022_anonym}. 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.
|
|
|
|
In this work we take an approach rooted in \textit{formal methods} and \textit{automated reasoning} to construct \korg. In particular, we employ \textit{model checking}, a sub-discipline of formal methods, to decidably and automatically find attacks in protocols or prove the absence of such.
|
|
|
|
We summarize our contributions:
|
|
\begin{itemize}
|
|
\item We present \korg, a tool for synthesizing attacks against distributed communication protocols. \korg supports four general attacker models: an attacker that can drop, replay, reorder, or insert messages on a channel.
|
|
\item We provide an overview of \korg and demonstrate its usage by walking through applying it to the ABP protocol
|
|
\item We present two case studies for two well-known protocols, TCP and Raft, illustrating the usefulness of \korg.
|
|
\end{itemize}
|
|
|
|
We release our code and our models as open source at \url{https://anonymous.4open.science/r/attacksynth-artifact-1B5D}.
|
|
|
|
\end{comment}
|
|
|