7 ms·

Not if the implementation is formally verified, like miTLS [0] and EverCrypt [1]. Parts of the latter were integrated into Firefox, which even provided a perfor

Not if the implementation is formally verified, like miTLS [0] and EverCrypt [1]. Parts of the latter were integrated into Firefox, which even provided a performance boost (10x in one case) [2]. I think what is needed is something like EverCrypt but for TLS. Or in other words, something like miTLS but which extracts to C and/or Assembly, to avoid garbage collection and for easy interoperation with different programming languages (preferably including an OpenSSL-compatible API for backwards compatibility). [0]: https://mitls.org/ https://mitls.org/ [1]: https://hacl-star.github.io/HaclValeEverCrypt.html https://hacl-star.github.io/HaclValeEverCrypt.html [2]: https://blog.mozilla.org/security/2020/07/06/performance-improvements-via-formally-verified-cryptography-in-firefox/ https://blog.mozilla.org/security/2020/07/06/performance-imp...

j16sdiz 6y ago
Formally verified against what? and what assumption were made? miTLS is formally verified against the TLS spec on handshaking, assuming the lower-level crypto routine are good. It is not even free from timing attack. EverCrypt have stronger proof, but it is only safe as in not crashing and correct as in match the spec in all valid input. It is not proved to be free from DoS or invalid input attack. OpenSSL do more then TLS. Lots of interesting thing are in the cert format parsing and management.
- wizeman 6y ago
  > Formally verified against what? and what assumption were made? Well, tell me again, what is OpenSSL formally verified against? What assumptions were made in OpenSSL? Formal verification does not eliminate very large classes of bugs only when absolutely everything is formally verified, including timing attacks. Instead, it consistently produces more reliable software, many times even when only certain basic properties are proved (such as, memory safety, lack of integer overflows or division by zero, etc). Formal verification can be a continuum, like testing, but proven to work for all inputs (that possibly meet certain conditions, under certain assumptions). The assumptions and properties that are proven can always be strengthened later, as seen in multiple real-world projects (such as seL4 and others). The result is code that is almost always a lot more bug-free than code that is not formally verified. And as I said, more properties can be proven over time, especially as new classes of attacks are discovered (e.g. timing attacks, speculation attacks in CPUs, etc).
  - nitrogen 6y ago
    It's also not like you'd just give up on fuzzers because you have formally verified code. All the same tools should still be available, plus one more.
  - cryptonector 6y ago
    To formally verify an implementation you need a... formal description of what is to be implemented and verified. Constructing a formal specification from RFC8446 is possible. Constructing a formal specification for PKIX... is not. PKIX is specified by a large number of RFCs and ITU-T/ISO specs, some of which are more formal than others. E.g., constructing a formal specification for ASN.1 should be possible (though a lot of work), while constructing a formal specification for certificate validation is really hard, especially if you must support complex PKIs like DoD's. Checking CRLs and OCSP, among other things, requires support for HTTP, and even LDAP, so now you have... a bunch more RFCs to construct formal descriptions of. And there had better be no bugs in the formal descriptions you construct from all these specs! Recall, they're mostly not formal specs at all -- they're written in English, with smatterings of ASN.1 (which is formal, though the specs for it, though they're very very good, mostly aren't formal). The CVE in question is in the PKIX part of OpenSSL, not the TLS implementation. What you're asking for is not 5 man-years worth of work, but tens of man-decades. The number of people with deep knowledge of all this stuff is minute as it is -- maybe just a handful, tens at most. The number of people with deep knowledge of a lot of this stuff is larger, but still minute. So you're asking to spend decades' worth of a tiny band of people's time on this project, when there are other valuable things for them to do. The number of people who can do dev work in this space is much larger, of course -- in the thousands. But very few of them have the right expertise to work on a formal, verified implementation of PKIX. Plus, it's all a moving target. Sure, we could... train a lot of people just for such a project, but it takes time to do that, and it still takes time from that tiny band of people who know this stuff really well. I'm afraid you're asking for unobtanium. EDIT: Plus, there's probably tens of millions of current dollars' (if not more) worth of development embodied in OpenSSL as it stands. It's probably at least that much to replace it with a verified implementation, and probably much more because the value of programmers expert enough to do it is much more than the $200K/year suggested above (even if you train new ones, it would take years of training, and then they would be just as valuable). I think a proper , formally verified replacement of OpenSSL would probably run into the hundreds of millions, especially if it's one huge project since those tend to fail.

j16sdiz 6y ago

Formally verified against what? and what assumption were made? miTLS is formally verified against the TLS spec on handshaking, assuming the lower-level crypto routine are good. It is not even free from timing attack. EverCrypt have stronger proof, but it is only safe as in not crashing and correct as in match the spec in all valid input. It is not proved to be free from DoS or invalid input attack. OpenSSL do more then TLS. Lots of interesting thing are in the cert format parsing and management.

wizeman 6y ago
> Formally verified against what? and what assumption were made? Well, tell me again, what is OpenSSL formally verified against? What assumptions were made in OpenSSL? Formal verification does not eliminate very large classes of bugs only when absolutely everything is formally verified, including timing attacks. Instead, it consistently produces more reliable software, many times even when only certain basic properties are proved (such as, memory safety, lack of integer overflows or division by zero, etc). Formal verification can be a continuum, like testing, but proven to work for all inputs (that possibly meet certain conditions, under certain assumptions). The assumptions and properties that are proven can always be strengthened later, as seen in multiple real-world projects (such as seL4 and others). The result is code that is almost always a lot more bug-free than code that is not formally verified. And as I said, more properties can be proven over time, especially as new classes of attacks are discovered (e.g. timing attacks, speculation attacks in CPUs, etc).
- nitrogen 6y ago
  It's also not like you'd just give up on fuzzers because you have formally verified code. All the same tools should still be available, plus one more.
- cryptonector 6y ago
  To formally verify an implementation you need a... formal description of what is to be implemented and verified. Constructing a formal specification from RFC8446 is possible. Constructing a formal specification for PKIX... is not. PKIX is specified by a large number of RFCs and ITU-T/ISO specs, some of which are more formal than others. E.g., constructing a formal specification for ASN.1 should be possible (though a lot of work), while constructing a formal specification for certificate validation is really hard, especially if you must support complex PKIs like DoD's. Checking CRLs and OCSP, among other things, requires support for HTTP, and even LDAP, so now you have... a bunch more RFCs to construct formal descriptions of. And there had better be no bugs in the formal descriptions you construct from all these specs! Recall, they're mostly not formal specs at all -- they're written in English, with smatterings of ASN.1 (which is formal, though the specs for it, though they're very very good, mostly aren't formal). The CVE in question is in the PKIX part of OpenSSL, not the TLS implementation. What you're asking for is not 5 man-years worth of work, but tens of man-decades. The number of people with deep knowledge of all this stuff is minute as it is -- maybe just a handful, tens at most. The number of people with deep knowledge of a lot of this stuff is larger, but still minute. So you're asking to spend decades' worth of a tiny band of people's time on this project, when there are other valuable things for them to do. The number of people who can do dev work in this space is much larger, of course -- in the thousands. But very few of them have the right expertise to work on a formal, verified implementation of PKIX. Plus, it's all a moving target. Sure, we could... train a lot of people just for such a project, but it takes time to do that, and it still takes time from that tiny band of people who know this stuff really well. I'm afraid you're asking for unobtanium. EDIT: Plus, there's probably tens of millions of current dollars' (if not more) worth of development embodied in OpenSSL as it stands. It's probably at least that much to replace it with a verified implementation, and probably much more because the value of programmers expert enough to do it is much more than the $200K/year suggested above (even if you train new ones, it would take years of training, and then they would be just as valuable). I think a proper , formally verified replacement of OpenSSL would probably run into the hundreds of millions, especially if it's one huge project since those tend to fail.