Compositional Testing of Internet Protocols
Compositional Testing of Internet Protocols
复制标题
DOI：
10.1109/secdev.2019.00031
复制
发表时间：
2019-09
期刊：
影响因子：
--
通讯作者：
K. McMillan;L. Zuck
中科院分区：
文献类型：
--
作者：
K. McMillan;L. Zuck
我们引入了一种以网络为中心的组合测试 (NCT) 方法来开发互联网协议的正式线路规范并测试协议实现是否符合通用标准。我们使用正式规范来生成用于协议实现的自动化测试器，基于使用 SMT 求解器求解的随机约束。这使得可以使用实现中固有的知识来解决非正式标准文档中的歧义，同时测试实现是否符合正在开发的正式规范。因为测试是组合性的，所以它允许我们检测规范太弱或太强的情况，并相应地完善规范。我们将该方法应用于 QUIC，这是一种新的互联网安全传输协议，目前正在 IETF 标准化过程中，旨在替代 TLS/TCP 堆栈并为 HTTP/3 奠定基础。在指定 QUIC 的过程中，我们发现了许多实现中的错误以及标准本身的问题。其中包括偏离路径拒绝服务攻击和类似于 OpenSSL 中“heartbleed”漏洞的信息泄露。本文描述了该方法的形式基础，并总结了其在 QUIC 中的具体应用。
We introduce a methodology of Network-centric Compositional Testing (NCT) to develop formal wire specifications of Internet protocols and to test protocol implementations for compliance to a common standard. We use formal specifications to generate automated testers for implementations of the protocol, based on randomized constraint solving using an SMT solver. This makes it possible to resolve ambiguities in informal standards documents using knowledge inherent in the implementations, while at the same time testing the implementations for compliance to the developing formal specification. Because the testing is compositional, it allows us to detect cases when the specification is either too weak or too strong, and to refine the specification accordingly. We apply the methodology to QUIC, a new Internet secure transport protocol currently in the process of IETF standardization and intended as a replacement for the TLS/TCP stack and a foundation for HTTP/3. In the process of specifying QUIC, we discovered numerous errors in implementations, as well as issues in the standard itself. These include an off-path denial of service attack and an information leak similar to the "heartbleed" vulnerability in OpenSSL. The paper describes the formal foundations of the methodology, and summarizes its specific application to QUIC.