Subject: Specification-based testing of QUIC implementations

From: Kenneth McMillan <[email-masked]>
Date: Wed, 28 Nov 2018 22:54:25 +0000

Hello, QUIC working group,

I am a researcher at Microsoft. Along with Lenore Zuck at the University of Illinois at Chicago, I have been working on a formal specification of the QUIC protocol. The formal specification is written in a language called Ivy, in a way that allows modular testing of implementations. That is, from the specification we can produce an automated tester
that takes one role in the protocol. The tester uses a technique called symbolic execution to randomly generate protocol traffic that complies with the specification. For example, if the tester is taking the client role, it generates packets that are legal for the client to send, and these are transmitted to the server being tested. The responses sent by the server are then checked for compliance with the specification.

This approach has certain advantages when compared to interoperabilty testing. First, the specification-based tester can generate stimulus that can't be produced by any current implementation and perhaps would only be produced by attackers. Because it is randomized, it tends to generate the unusual cases that specifiers and implementers may not have considered. Second, it checks for actual specification compliance and not just for correct interoperation. Ensuring compliance to the specification can be helpful for future protocol developers who have deal with compatibility with legacy implementations. Third, the formal specification can be seen as documentation, since it gives an unambiguous interpretation of statements made in natural language in the specification documents.

Thus far, we have work with Christian Huitema on picoquic and with Lars Eggert on quant. Testing the servers has exposed a variety of issues that run from memory faults and assertion failures to more interesting protocol compliance issues. A couple of these have stimulated discussion on github, including  issue #2033, related to an off-path migration attack, and issue #2052, related to the pseudo-code in the recovery document.

The formal specification is currently under development. Enough of QUIC is currently specified to allow testing of basic interactions of the client and server, but quite a few protocol features are still not specified. It would be very helpful for us to hear from the working group about which protocol features are most in need of testing, or which might be clarified by formalizing their specification. Also, as you may imagine, there are some cases where we found the draft specification document a little difficult to interpret. Please let us know if this is the right forum to raise issues about ambiguity in the spec, or whether that would be better done on github.

If you're interested to look at the formal specification or run the testers, you can find the code here:

https://github.com/Microsoft/ivy/blob/quic15_merge_temp/doc/examples/quic/README.md

Also, if you have an implementation of QUIC and would be interested in testing it, we'll be happy to work with you.

-- Ken McMIllan

Sent from Outlook<http://aka.ms/weboutlook>

---

From: Lucas Pardue <[email-masked]>
Date: Wed, 28 Nov 2018 23:42:10 +0000

Hi Ken and Lenore,

This sounds really interesting. Thanks for working on the topic and sharing
it.

I intend to take a deeper look. My initial question before then is, is this
scoped at the transport layer, or is it applicable to application layer
i.e. HTTP/3.

Kind regards
Lucas

On Wed, 28 Nov 2018, 22:54 Kenneth McMillan <kenmcmil=
[email-masked] wrote:

> I am a researcher at Microsoft. Along with Lenore Zuck at the University
> of Illinois at Chicago, I have been working on a formal specification of
> the QUIC protocol. The formal specification is written in a language called
> Ivy, in a way that allows modular testing of implementations. That is, from
> the specification we can produce an automated tester
> that takes one role in the protocol. The tester uses a technique called
> symbolic execution to randomly generate protocol traffic that complies with
> the specification. For example, if the tester is taking the client role, it
> generates packets that are legal for the client to send, and these are
> transmitted to the server being tested. The responses sent by the server
> are then checked for compliance with the specification.
>
> This approach has certain advantages when compared to interoperabilty
> testing. First, the specification-based tester can generate stimulus that
> can't be produced by any current implementation and perhaps would only be
> produced by attackers. Because it is randomized, it tends to generate the
> unusual cases that specifiers and implementers may not have considered.
> Second, it checks for actual specification compliance and not just for
> correct interoperation. Ensuring compliance to the specification can be
> helpful for future protocol developers who have deal with compatibility
> with legacy implementations. Third, the formal specification can be seen as
> documentation, since it gives an unambiguous interpretation of statements
> made in natural language in the specification documents.
>
> Thus far, we have work with Christian Huitema on picoquic and with Lars
> Eggert on quant. Testing the servers has exposed a variety of issues that
> run from memory faults and assertion failures to more interesting protocol
> compliance issues. A couple of these have stimulated discussion on github,
> including  issue #2033, related to an off-path migration attack, and
> issue #2052, related to the pseudo-code in the recovery document.
>
> The formal specification is currently under development. Enough of QUIC is
> currently specified to allow testing of basic interactions of the client
> and server, but quite a few protocol features are still not specified. It
> would be very helpful for us to hear from the working group about which
> protocol features are most in need of testing, or which might be clarified
> by formalizing their specification.. Also, as you may imagine, there are
> some cases where we found the draft specification document a little
> difficult to interpret. Please let us know if this is the right forum to
> raise issues about ambiguity in the spec, or whether that would be better
> done on github.
>
> Also, if you have an implementation of QUIC and would be interested in
> testing it, we'll be happy to work with you.
>
> -- Ken McMIllan
>
>
>
>
>
> Sent from Outlook <http://aka.ms/weboutlook>
>

---

From: Kenneth McMillan <[email-masked]>
Date: Wed, 28 Nov 2018 23:46:52 +0000

Hi Lucas,

Right now we're only specifying the transport layer. The application layer is just modeled as a collection of abstract streams. However, if there are interesting interactions between QUIC and HTTP/3 that need to be tested, we could move in that direction.

--Ken

________________________________
From: Lucas Pardue <[email-masked]>
Sent: Wednesday, November 28, 2018 3:42:10 PM
To: Kenneth McMillan
Cc: QUIC WG; Lenore Zuck
Subject: Re: Specification-based testing of QUIC implementations

Hi Ken and Lenore,

This sounds really interesting. Thanks for working on the topic and sharing it.

I intend to take a deeper look. My initial question before then is, is this scoped at the transport layer, or is it applicable to application layer i.e. HTTP/3.

Kind regards
Lucas

On Wed, 28 Nov 2018, 22:54 Kenneth McMillan <kenmcmil=[email-masked]<mailto:[email-masked]> wrote:

The formal specification is currently under development. Enough of QUIC is currently specified to allow testing of basic interactions of the client and server, but quite a few protocol features are still not specified. It would be very helpful for us to hear from the working group about which protocol features are most in need of testing, or which might be clarified by formalizing their specification... Also, as you may imagine, there are some cases where we found the draft specification document a little difficult to interpret. Please let us know if this is the right forum to raise issues about ambiguity in the spec, or whether that would be better done on github.

https://github.com/Microsoft/ivy/blob/quic15_merge_temp/doc/examples/quic/README..md<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FMicrosoft%2Fivy%2Fblob%2Fquic15_merge_temp%2Fdoc%2Fexamples%2Fquic%2FREADME.md&data=02%7C01%7Ckenmcmil%40exchange.microsoft.com%7Cc19b82c509ee4d3857bc08d6558b2757%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636790453481274030&sdata=dwZmBl%2FFW4EnvsiiBAhkyG1eID%2BkEXMQ3Nw%2Bkt%2BStN4%3D&reserved=0>

-- Ken McMIllan

---

From: Lars Eggert <[email-masked]>
Date: Thu, 29 Nov 2018 10:18:06 +0200

Hi,

you might also be interested in this related paper that is going to be presented next week at EPIQ:

Felix Rath, Daniel Schemmel, and Klaus Wehrle. 2018. Interoperability-Guided Testing of QUIC Implementations using Symbolic Execution. In Proceedings of the Workshop on the Evolution, Performance, and Interoperability of QUIC (EPIQ'18). ACM, New York, NY, USA, 15-21. DOI: https://doi.org/10.1145/3284850.3284853

Unfortunately, the PDF will only become available at the link above once the event has started, which is next Tuesday :-/ But you can probably ask the authors for a copy.

Lars

---

From: Jan Rüth <[email-masked]>
Date: Fri, 30 Nov 2018 08:48:04 +0000

Hi,

the paper in reference is from a colleague of mine.

He just uploaded it to arxiv to have it already available for the wg:

https://arxiv.org/abs/1811.12099

Jan

On 29. Nov 2018, at 09:18, Lars Eggert <[email-masked]<mailto:[email-masked]>> wrote:

Hi,

Lars

---

From: Kenneth McMillan <[email-masked]>
Date: Fri, 30 Nov 2018 20:23:34 +0000

Thanks for the link to the paper.

Actually, if you're familiar with tools like Klee, I can explain some of the differences with the approach we are taking and some of the relative advantages and disadvantages. Klee and similar tools do "white-box" testing. That is, they examine an execution path of the implementation code and apply symbolic execution to discover other inputs that will drive the code along other paths, thus improving test coverage. In the paper, they apply this idea to QUIC by writing some test scenarios in C, linking these with the client and server code, and then using Klee to generate inputs for the test scenarios. This is actually a pretty neat trick, because they have to get both the client and the server to run as a single thread to apply KLEE.

By contrast, what Lenore and I are doing is "black-box" testing. That is, we don't look inside the implementations or symbolically execute their code. Rather, we start with a formal specification of the protocol. We apply symbolic execution techniques to this specification to randomly generate legal protocol traffic at the level of UDP datagrams, in response to actions of the implementation being tested (either a client or a server). The randomly generated datagrams take into account the protocol state, so the specification-based test effectively takes one role in the protocol and has a "conversation" with the implementation under test.

The "black-box" specification-based approach has several advantages:

1) There are no manual tests scenarios involved, so we are not limited to scenarios that an engineer imagines.

2) We are not limited to protocol behaviors that can be generated by existing implementations.

3) We can detect protocol compliance violations and not just interop issues or crashes.

4) The implementation can be in any language and can be tested without modification or mocking API's.

Generally speaking, it's much easier to generate interesting behavior on the wire by driving the wire directly than by driving it through the API of some client or server library.

On the other hand, the chief advantage of the "white-box" approach is that takes into account the actual code being tested and tries to generate tests that produce good coverage for that particular code. Also, there's no need to write a formal specification of the protocol. You just have to write a few test scenarios.

So the two approaches are complementary. In principle, you could also do specification-based "white-box" testing by symbolically executing the specification and implementation simultaneously. There are lots of technical problems there, however, and this might not scale to a protocol of the complexity of QUIC.

--Ken

________________________________
From: Jan Rüth <[email-masked]>
Sent: Friday, November 30, 2018 12:48:04 AM
To: Lars Eggert
Cc: Kenneth McMillan; Lenore Zuck; QUIC WG; Lucas Pardue
Subject: Re: Specification-based testing of QUIC implementations

Hi,

https://arxiv..org/abs/1811.12099<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Farxiv.org%2Fabs%2F1811.12099&data=02%7C01%7Ckenmcmil%40exchange.microsoft.com%7Cfb915933c4e044453dbc08d656a096a3%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636791645071181884&sdata=WsuYQv97%2BhUnao14%2F0fhJ4%2B8EdfjbsTEa8jMC%2BgodXo%3D&reserved=0>

Jan

Hi,

Felix Rath, Daniel Schemmel, and Klaus Wehrle. 2018. Interoperability-Guided Testing of QUIC Implementations using Symbolic Execution. In Proceedings of the Workshop on the Evolution, Performance, and Interoperability of QUIC (EPIQ'18). ACM, New York, NY, USA, 15-21. DOI: https://doi.org/10.1145/3284850.3284853<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdoi.org%2F10.1145%2F3284850.3284853&data=02%7C01%7Ckenmcmil%40exchange.microsoft.com%7Cfb915933c4e044453dbc08d656a096a3%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636791645071191831&sdata=27hL%2FzTMWVyKsEc3o6%2BOhDQDVxzpWEWw2lKh%2BdE1%2Bsw%3D&reserved=0>

Lars