Automated Channel Fault Analysis with Tofu
For researchers and practitioners of distributed protocols, this work provides a generalizable, automated approach to channel fault analysis, addressing a gap in formal verification.
The authors developed a methodology and tool, Tofu, for automated channel fault analysis of distributed protocols, enabling synthesis of attack traces or proof of absence via exhaustive state-space search. They demonstrated Tofu on TCP.
Distributed protocols are the linchpin of the modern internet, underpinning every internet service. This has in turn motivated a massive body of research ensuring the security, reliability, and performance of distributed protocols. In these works, a wide-ranging assumption is that distributed protocols operate over faulty or attacker-controlled channels, where messages can be arbitrarily inserted, dropped, replayed, or reordered. Formal verification work targeting distributed protocols typically defines its own notion of faulty 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 conducting channel fault analysis on distributed protocols, and we introduce Tofu, a generalizable tool that implements our methodology. Tofu provides sound, complete analysis, synthesizing channel fault-based attack traces 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 Tofu by employing it to study TCP.