Use formally-verified code from miTLS

[DemiMarie]

Describe the feature you'd like supported

MsQuic should use as much formally-verified code from miTLS as possible

Proposed solution

This will significantly reduce the risk of a bug or vulnerability.

Additional context

miTLS already has some TLS and QUIC code but it is not easy to use outside of Microsoft.

[nibanks]

We used to use it (go look at release/1.0 branch) but stopped because of the lack of official, production support. The project is currently managed by a Microsoft research team that doesn't have the official budget/capacity to support the library 24-7. @ad-l has anything changed on the miTLS side recently that might allow us to bring back support?

[DemiMarie]

We used to use it (go look at release/1.0 branch) but stopped because of the lack of official, production support. The project is currently managed by a Microsoft research team that doesn't have the official budget/capacity to support the library 24-7. @ad-l has anything changed on the miTLS side recently that might allow us to bring back support?

project-everest/mitls-fstar#252 (comment) claims that this code is currently used in production, FYI

[nibanks]

Pieces of the crypto layer are, but I don't know any places the TLS layer is.

[ad-l]

Hi @DemiMarie, unfortunately miTLS is not actively supported for use with MsQuic at this point so I would not recommend you try to it in a production environment. Other parts of miTLS and Hacl* are in active production use in other settings, but that does not include the QUIC handshake component.

[DemiMarie]

miTLS and Hacl* are in active production use in other settings, but that does not include the QUIC handshake component.

Is there any reference for how to use miTLS’s TLS code in a setup suitable for production?

[nibanks]

@DemiMarie I'm going to close this unless you have any other feedback here. There's nothing we can really do right now.