Prognosis：网络协议实现的闭盒分析
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
