Ideally you want a formally verified SPARK or CompCert C implementation of TLS, but those are not open sores compilers so they won't fly.
That's a hefty judgment. If we look at major attacks on TLS endpoints I'd summarize them as, in order,:
1. Memory safety
2. Weak / old configurations
3. Invalid state machine transitions
Rustls addresses all 3 of those, or at least it attempts to. (1) is obvious - it's rust. (2) rustls only supports the subset of TLS versions that are considered safe. (3) rustls avoids issues like gotofail and smacktls by encoding state machines as types, turning invalid state transitions into type failures.
Plus, the actual crypto primitives are extremely well tested and built off of other existing libraries.
So yeah, maybe some aspect of the crypto is incorrect, but, while interesting from an academic perspective, the real world ranks those other 3 things as way more important.
Half of these are caused by C problems not present in Rust like: null pointer errors, buffer overflows, integer overflows.
The rest are logic errors (e.g., parsing errors) or crypto vulnerabilities (e.g., side channel attacks). There's nothing about Rust that magically prevents these errors. These vulnerabilities are discovered through testing and more importantly real world usage. Rustls has not been used nearly as much as or as long as openssl, so critical bugs could be in Rustls. You could encode some logic in the type system, but the types are still code that have to be tested. It's not a formal proof. It could still be wrong.
It depends on your threat model and your risk tolerance whether you want to depend on relatively unvetted code.
> These vulnerabilities are discovered through testing and more importantly real world usage.
FWIW I disagree that real world usage is necessarily more important. It is quite important, but at the same time the real world usage isn't going to hit all sorts of weird quirky paths. By contrast, Rustls has 97% line coverage, OpenSSL has ~65%. Of course, coverage isn't everything, but that's notable.
> It's not a formal proof. It could still be wrong.
So long as the type system is sound, I'm not sure this is true. If you embed a state machine into your type system your type system guarantees that the state machine executes as defined. Granted this is not checking against an external model.
I will say that rustls still will benefit from wider adoption and more evaluation but imo it addresses the largest concerns today.
One verified TLS implementation is miTLS, written in F*.
Having a SPARK-verified version would of course be great anyway.