25 lines
2.0 KiB
TeX
25 lines
2.0 KiB
TeX
Distributed protocols are the lynchpin of the modern internet,
|
|
underpinning every internet service.
|
|
This has in turn motivated a massive amount of research ensuring the security,
|
|
reliability, and performance of distributed protocols.
|
|
In these works, a wide-ranging assumption is that distributed
|
|
protocols operate over \textit{imperfect} or
|
|
\textit{attacker-controlled} channels, where messages can be arbitrarily
|
|
inserted, dropped, replayed, or reordered.
|
|
Formal methods work formally verifying distributed protocols
|
|
typically defines their own notion of imperfect or malicious channels,
|
|
then constructively proves their protocol is correct with respect to it.
|
|
In this work we take a fundamentally different approach:
|
|
we develop a rigorous methodology for
|
|
automatically discovering \textit{attack traces}
|
|
on distributed protocols with respect to imperfect channels,
|
|
and we introduce \korg, a highly generalizable tool for synthesizing
|
|
attacks on distributed protocols that implements our methodology.
|
|
\korg provides sound, complete analysis, synthesizing attacks on arbitrary
|
|
linear temporal logic (LTL) protocol specifications
|
|
or proving the absence of such through an exhaustive state-space search.
|
|
We demonstrate the applicability of \korg by employing to study TCP, SCTP, and Raft.
|
|
|
|
% ===== OLD ABSTRACT ======
|
|
%Distributed protocols underpin the modern internet, making their correctness and security critical. Formal methods provide rigorous tools for analyzing protocol correctness and cryptographic security, yet existing tools fall short for denial of service (DoS) analysis. We introduce \korg, a tool that synthesizes attacks on distributed protocols by targeting communication channels to violate linear temporal logic (LTL) specifications. \korg provides sound, complete analysis, synthesizing attacks or proving their absence through exhaustive state-space search. With support for pre-defined and custom attacker models, \korg enables targeted DoS analysis and broader LTL-based verification, demonstrated through various case studies.
|