Automated Channel Fault Analysis with Tofu

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, 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.