[release] will fix several security defects with maximum severity “high”.
I wonder if LibreSSL is vulnerable to these.
They’ve so far been vulnerable to fewer than OpenSSL on any given security announcement, and also frequently have a narrower exposure (i.e., a vulnerability that’s “high” on OpenSSL is legitimately “low” on LibreSSL), but, at least so far, every OpenSSL vulnerability announcement has had an accompanying LibreSSL one. I don’t think this means LibreSSL is a failure; I think it’s a sign it’s working. They’re just not to perfect yet. But I kind of doubt they’re going to get to zero until/unless they also port to ATS or something.
Safer implementations of SSL are within reach.
TrustinSoft, a software verification startup, provides a verification kit for PolarSSL, that is a description of which configurations have been proved completely free of a precisely defined range of C’s undefined behaviours that are used in exploitation.
There is an OCaml implementation of TLS that has seen some amount of testing in the field. There is also a native Haskell implementation, but I don’t know whether/how its security has been tested.
One of the recent-ish OpenSSL vulnerabilities was discovered by preliminary work towards a Coq implementation – a concrete example of the fact that formalizing helps uncovering defects.
Finally, there is a verified implementation of TLS, miTLS, implemented in Fstar – a ML-like language extended with dependent types and designed for software verification.
Oh, absolutely. There was also a formally verified stack in F# or an F# dialect, if I recall correctly. But the point of LibreSSL is to try to provide a sane API-compatible replacement for OpenSSL (as opposed to any of the things we’ve just mentioned, or even as opposed to Google’s BoringSSL). That’s why I mentioned ATS, which at least theoretically can vend C bindings, but also has an extremely rigorous type system. Rust would be another good candidate in that space.
Indeed, you are thinking of the Fstar work, I’ll edit my post to add a reference, thanks.
HIGH Severity. This includes issues that are of a lower risk than critical, perhaps due to affecting less common configurations, or which are less likely to be exploitable.
Also it seems this will be released on the 1st of March