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.

翻译：分布式协议是现代互联网的基石，支撑着所有互联网服务。这进而催生了大量研究，以确保分布式协议的安全性、可靠性和性能。在这些研究中，一个广泛的假设是：分布式协议运行在有故障或受攻击者控制的通道上，其中消息可以被任意插入、丢弃、重放或重新排序。针对分布式协议的形式化验证工作通常定义其自身的故障或恶意通道概念，然后构造性地证明其协议相对于该概念的正确性。在本文中，我们采取了一种根本不同的方法：我们开发了一种严格的方法论，用于自动对分布式协议进行通道故障分析，并介绍了Tofu——一个实现我们方法论的可泛化工具。Tofu提供可靠且完备的分析，通过在任意线性时态逻辑（LTL）协议规范上合成基于通道故障的攻击轨迹，或通过穷举状态空间搜索证明这类攻击不存在。我们通过将Tofu应用于TCP研究来展示其适用性。