Ferreira, T;
Brewton, H;
D'Antoni, L;
Silva, A;
(2021)
Prognosis: Closed-box analysis of network protocol implementations.
In:
SIGCOMM '21: Proceedings of the 2021 ACM SIGCOMM 2021 Conference.
(pp. pp. 762-774).
ACM Press: New York, NY, USA.
Preview |
Text
main.pdf - Accepted Version Download (948kB) | Preview |
Abstract
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 analyse 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.
| Type: | Proceedings paper |
|---|---|
| Title: | Prognosis: Closed-box analysis of network protocol implementations |
| Event: | SIGCOMM '21: ACM SIGCOMM 2021 Conference |
| ISBN-13: | 978-1-4503-8383-7 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/3452296.3472938 |
| Publisher version: | https://doi.org/10.1145/3452296.3472938 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Model learning, synthesis, varied abstraction modelling, bug finding, protocol state machines |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10134696 |
Archive Staff Only
 |
View Item |
