
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.
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 7 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
