论文标题
预后：网络协议实施的闭盒分析
Prognosis: Closed-Box Analysis of Network Protocol Implementations
论文作者
论文摘要
我们提出了预后，该框架为网络协议实现的模型提供了自动的闭盒学习和分析。预后可以学习从简单确定性自动机到包含数据操作（例如寄存器更新）的模型的模型，并可用于解锁各种分析技术 - 模型检查时间属性，计算同一协议的两个实现模型之间的差异，或通过基于模型测试生成改进测试。预后是模块化的，易于适应不同方案（例如TCP和QUIC）及其实现。我们使用预后来学习（部分）三个Quic实现的模型 - Quiche（Cloudflare），Google Quic和Facebook MVFST-并使用这些模型来分析各种实现之间的差异。我们的分析提供了对不同设计选择的见解，并发现了潜在的错误。具体而言，我们发现了多个QUIC实施中的关键错误，这些错误已被开发人员承认。
We present Prognosis, a framework offering automated closed-box learning and analysis of models of network protocol implementations. Prognosis can learn models that vary in abstraction level from simple deterministic automata to models containing data operations, such as register updates, and can be used to unlock a variety of analysis techniques -- model checking temporal properties, computing differences between models of two implementations of the same protocol, or improving testing via model-based test generation. Prognosis is modular and easily adaptable to different protocols (e.g., TCP and QUIC) and their implementations. We use Prognosis to learn models of (parts of) three QUIC implementations -- Quiche (Cloudflare), Google QUIC, and Facebook mvfst -- and use these models to analyze the differences between the various implementations. Our analysis provides insights into different design choices and uncovers potential bugs. Concretely, we have found critical bugs in multiple QUIC implementations, which have been acknowledged by the developers.
