6 ms·

> Formally verified against what? and what assumption were made? Well, tell me again, what is OpenSSL formally verified against? What assumptions were made in

> 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.
- wizeman 6y ago
  Well, sure, if your start with those premises, then I'm not surprised that you reach the conclusion that the goal is unachievable. First of all, if constructing a formal specification for PKIX is not possible, then that should be telling you that it either needs to be simplified, better specified or scrapped altogether for something better (the latter would require an extremely large transition period, I'm imagining, so the first two are much preferred in this situation). Otherwise, how can you be sure that any implementation in fact implements it correctly? > And there had better be no bugs in the formal descriptions you construct from all these specs! Well, I don't think that is true. You should in fact allow bugs in the formal description, otherwise how will you ever get anything done in such a project? You see, having a formal description with a bug is much better than having no formal description at all. If you have no formal description, you can't really tell if your code has bugs. If you have a buggy formal description, then you are able to catch some bugs in the implementation and the implementation can also catch some bugs in the formal description. Also, some parts of the formal description can catch bugs in other parts of the formal description. So the end result can be strictly better than the status quo. > Plus, it's all a moving target. Sure, but hopefully it's a moving target moving in the direction of simplification rather than getting more complex, otherwise things will just get worse rather than get better, regardless if we keep with the status quo or not. I'm not a TLS expert by any means but I think TLS 1.3 moved in that direction for some parts of the protocol, at least (if I'm not mistaken). Also, I think you are not fully appreciating that formal verification can be done incrementally. You can start by doing the minimum possible, i.e. simply verifying that your code is free of runtime errors, which would eliminate all memory safety-related bugs, including Heartbleed. This would already be better than reimplementing in Rust, because the latter can protect from memory safety bugs but not other runtime bugs (such as division by zero, unexpected panics, etc). BTW, this minimal verification effort would already eliminate the second bug in this security advisory. You can then verify other simple properties, even function by function, no complicated models are even necessary at first. For example, you could verify that your function that verifies a CA certificate, when passed the STRICT flag, is really more strict than when not passed the STRICT flag. This would eliminate the first bug in this security advisory and all other similar bugs in the same function call-chain. BTW, what I just said is really easy to specify, and I'm guessing it's also very easy to prove, since I'm guessing that the strict checks are just additional checks, while the normal checks are shared between the two verification modes. Many other such properties are also easy to prove. The more difficult properties/models, or even full functional verification, can be implemented by more expert developers or even mathematicians. I think the problem is also that OpenSSL devs, like the vast majority of devs, probably have no desire/intention/motivation/ability to do formal verification, otherwise you could even do this in the OpenSSL code base itself (although that is not ideal because verifying a program written in C requires more manual work than verifying it in a simpler language whose code extracts to C). I'm also guessing that your budget estimate is an exaggeration since miTLS and EverCrypt, although admittedly projects whose scope has still not reached your ambitious goals (i.e. full functional verification of all layers in the stack), was probably done with a much smaller budget. And it's not like you can't build on top of that and incrementally verify more properties over time, e.g. more layers of the stack or whatever. You don't need a huge mega-project, just a starting point, and sufficient motivation.

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.

wizeman 6y ago
Well, sure, if your start with those premises, then I'm not surprised that you reach the conclusion that the goal is unachievable. First of all, if constructing a formal specification for PKIX is not possible, then that should be telling you that it either needs to be simplified, better specified or scrapped altogether for something better (the latter would require an extremely large transition period, I'm imagining, so the first two are much preferred in this situation). Otherwise, how can you be sure that any implementation in fact implements it correctly? > And there had better be no bugs in the formal descriptions you construct from all these specs! Well, I don't think that is true. You should in fact allow bugs in the formal description, otherwise how will you ever get anything done in such a project? You see, having a formal description with a bug is much better than having no formal description at all. If you have no formal description, you can't really tell if your code has bugs. If you have a buggy formal description, then you are able to catch some bugs in the implementation and the implementation can also catch some bugs in the formal description. Also, some parts of the formal description can catch bugs in other parts of the formal description. So the end result can be strictly better than the status quo. > Plus, it's all a moving target. Sure, but hopefully it's a moving target moving in the direction of simplification rather than getting more complex, otherwise things will just get worse rather than get better, regardless if we keep with the status quo or not. I'm not a TLS expert by any means but I think TLS 1.3 moved in that direction for some parts of the protocol, at least (if I'm not mistaken). Also, I think you are not fully appreciating that formal verification can be done incrementally. You can start by doing the minimum possible, i.e. simply verifying that your code is free of runtime errors, which would eliminate all memory safety-related bugs, including Heartbleed. This would already be better than reimplementing in Rust, because the latter can protect from memory safety bugs but not other runtime bugs (such as division by zero, unexpected panics, etc). BTW, this minimal verification effort would already eliminate the second bug in this security advisory. You can then verify other simple properties, even function by function, no complicated models are even necessary at first. For example, you could verify that your function that verifies a CA certificate, when passed the STRICT flag, is really more strict than when not passed the STRICT flag. This would eliminate the first bug in this security advisory and all other similar bugs in the same function call-chain. BTW, what I just said is really easy to specify, and I'm guessing it's also very easy to prove, since I'm guessing that the strict checks are just additional checks, while the normal checks are shared between the two verification modes. Many other such properties are also easy to prove. The more difficult properties/models, or even full functional verification, can be implemented by more expert developers or even mathematicians. I think the problem is also that OpenSSL devs, like the vast majority of devs, probably have no desire/intention/motivation/ability to do formal verification, otherwise you could even do this in the OpenSSL code base itself (although that is not ideal because verifying a program written in C requires more manual work than verifying it in a simpler language whose code extracts to C). I'm also guessing that your budget estimate is an exaggeration since miTLS and EverCrypt, although admittedly projects whose scope has still not reached your ambitious goals (i.e. full functional verification of all layers in the stack), was probably done with a much smaller budget. And it's not like you can't build on top of that and incrementally verify more properties over time, e.g. more layers of the stack or whatever. You don't need a huge mega-project, just a starting point, and sufficient motivation.