Automated Channel Fault Analysis with Tofu
Jacob Ginesin, Max von Hippel, Cristina Nita-Rotaru

TL;DR
Tofu is a novel tool that automatically analyzes channel faults in distributed protocols, providing attack traces or proving their security through exhaustive state-space search, demonstrated on TCP.
Contribution
We introduce a rigorous, automated methodology and a generalizable tool, Tofu, for analyzing channel faults in distributed protocols with soundness and completeness.
Findings
Tofu can synthesize attack traces for TCP under channel faults.
Tofu proves the absence of channel fault attacks in certain protocol specifications.
The methodology is applicable to arbitrary LTL protocol specifications.
Abstract
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,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
