This repo contains code for the Dafny implementation of QUIC protocol layer, which is used in the following paper:
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, and Yi Zhou In Proceedings of the IEEE Symposium on Security and Privacy, May, 2021
The F* implementation of QUIC record layer can be found in the everquic repo.
This work was done as part of Project Everest.
Simply run make on the current directory. This should automatically run everything necessary to build all the files.
Run make verify on the current directory.
All the Dafny files are .dfy files in the src/ directory. They can be grouped as:
- Connection Management: QUICConnection, QUICAPIs, QEngine, QUICEngine, QPacketSpace, QUICDataTypes, QConnection, QUICTLS
- Data Structures: Seqs, PrivateDLL, FreezableArray, DynamicArray
- Frame mgmt: QUICConstants, QUICUtils, QUICFrame
- Loss Recovery and Congestion Control: QLossRecovery, QUICLossAndCongestion
- Stream mgmt: QStream, QUICStream, QStreamManager
- Miscellaneous:: OverFlowCheck, Options, Misc
- FFI: HandleFFIs, QUICFFI, Extern, NativeTypes, QUICCrypto
These are hand-written .h and .cpp files used for FFI. They can be
found in ffi-connections/ and src/handwritten-dot-h-files/
directories.
These handwritten files can be found in the examples/ directory. For
testing see the data/ directory.
For conveniently testing and benchmarking the generated server and
client, see the scripts/ directory.
Can be found in their respective directories.