Towards verification of QUIC and its extensions

QUIC is a new transport protocol that aims to be widely used over the Internet. It is built above UDP and associates the benefits of TCP and TLS. The specification of this protocol just finished being standardized with the RFC9000. Compliance to this specification is essential to ensure future web safety and security An attempt to the verification of QUIC was done by McMillan & Zuck by using a methodology called "Network-centric Compositional testing". Ivy, a tool and language developed by Microsoft, was used in this methodology to perform a formal verification of the QUIC protocol. In this master thesis, we propose an extension to this work. First, we update McMillan & Zuck QUIC model to one of the latest draft. This draft is similar to the RFC9000. Then, we added the verification of 41 properties that were not present in the original model. One QUIC extension was also verified. Finally, we tested eight open source implementations to the compliance of all the modelled requirements. We found several errors and highlighted ambiguities that are still present in the RFC9000. The usefulness of our work was demonstrated by fixing a QUIC implementation with the errors we found. We proposed possible extensions to our work and we made publicly available all the resources needed to perform these extensions.