3 ms·
Have you considered implementing any parts of this in F* (so they can be verified) and extracting back to C, as is being done for TLS? https://project-everest.
by profquail 6y ago
Have you considered implementing any parts of this in F* (so they can be verified) and extracting back to C, as is being done for TLS?
https://project-everest.github.io/ https://project-everest.github.io/
- nibanks 6y agoWe do work with the Everest team. We have unofficial support on top of miTLS (which they produce). We haven't looked into actually using F* for any of the QUIC code though.
- catalin_hritcu 6y agoSome work on verifying QUIC packet encryption using F* is happening at Microsoft Research: https://github.com/project-everest/everquic-crypto https://github.com/project-everest/everquic-crypto
- protz 6y agoJust to build on Catalin's answer. We are actively working on an implementation of QUIC's transport layer (i.e. packet encryption and decryption), along with a proof of cryptographic security. This is what Catalin linked to (https://github.com/project-everest/everquic-crypto https://github.com/project-everest/everquic-crypto). EverQuic-Crypto builds upon two previous projects: EverParse, a library of verified low-level parsers and serializers which we apply to the QUIC network formats, and EverCrypt, a cryptographic provider with agility and multiplexing, which we use for all the cryptography, e.g. packet number encryption, AEAD, etc. This is not yet a full QUIC implementation, but we have plans for extending this codebase to cover more of the QUIC protocol.