Tofu：自动化通道故障分析工具

分布式协议是现代互联网的基石，支撑着每一个互联网服务。这导致动力大量研究确保分布式协议的安全、可靠性和性能。在这些工作中，广泛假设是分布式协议运行在故障或受攻击者控制的通道上，消息可被任意插入、删除、重放或重新排序。针对分布式协议的形式化验证工作通常定义自身对故障或恶意通道的概念，然后构造性地证明其协议相对于该概念是正确的。在本工作中，我们采取根本不同的方法：我们发展了一种自动对分布式协议进行通道故障分析的严格方法，并引入 Tofu，这是一个通用可实现我们方法的工具。Tofu 提供严谨、完备的分析，通过穷举状态空间搜索合成通道故障基础的攻击轨迹，或证明其不存在。我们通过应用于 TCP 研究来展示 Tofu 的适用性。