4 ms·

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 constructin

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.

cryptonector 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. I didn't say unachievable. I said costly. > 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). https://xkcd.com/927/ https://xkcd.com/927/ The specs for the new thing would basically have to be written in Coq or similar. Even if you try real hard to keep it small and not make the... many mistakes made in PKIX's history... it would still be huge. And it would be even less accessible than PKIX already is. > 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. That's just an argument for better testing. That's not implementation verification. > This would eliminate the first bug in this security advisory and all other similar bugs in the same function call-chain. Only if you thought to write that test to begin with. Writing a test for everything is... not really possible. SQLite3, one of the most tested codebases in the world, has a private testsuite that gets 100% branch coverage, and even that is not the same as testing every possible combination of branches. > 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. It's not. The reason the strictness flag was added was that OpenSSL was historically less strict than the spec demanded. It turns out that when you're dealing with more than 30 years of history, you get kinks in the works. It wouldn't be different for whatever thing replaces PKIX. > 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 [...] You must be very popular at parties. > I'm also guessing that your budget estimate is an exaggeration since miTLS and EverCrypt, [...] Looking at miTLS, it only claims to be an implementation of TLS, not PKIX. Not surprising. EverCrypt is a cryptography library, not a PKIX library.
- wizeman 6y ago
  > That's just an argument for better testing. That's not implementation verification. No, I'm not talking about testing, I'm talking about really basic formal verification: forall (x: Certificate), verify_certificate(x, flags = 0) == invalid ==> verify_certificate(x, flags = STRICT) == invalid This is trivial to specify and almost as trivial to prove to be correct for all inputs. Testing can't do that, no matter how good your testing. > Only if you thought to write that test to begin with. Writing a test for everything is... not really possible. I agree, but I'm not talking about testing. I'm talking about formal verification. > It's not. The reason the strictness flag was added was that OpenSSL was historically less strict than the spec demanded. It turns out that when you're dealing with more than 30 years of history, you get kinks in the works. It wouldn't be different for whatever thing replaces PKIX. That's totally fine and wouldn't affect the verification of that function at all. This is a very simple property to verify and it would avoid this bug and all similar bugs in that function (even if that function calls other functions, no matter how large or complex they are). Other functions also have such easy to verify properties, this is not hard at all to come up with (although sure, some more difficult properties might be harder to verify). > You must be very popular at parties. I didn't want to be dismissive of OpenSSL devs or other devs in general, I just find it frustrating that there are so many myths surrounding this topic, and a lot less education, interest and investment than I think there should be, nowadays.

cryptonector 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. I didn't say unachievable. I said costly. > 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). https://xkcd.com/927/ https://xkcd.com/927/ The specs for the new thing would basically have to be written in Coq or similar. Even if you try real hard to keep it small and not make the... many mistakes made in PKIX's history... it would still be huge. And it would be even less accessible than PKIX already is. > 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. That's just an argument for better testing. That's not implementation verification. > This would eliminate the first bug in this security advisory and all other similar bugs in the same function call-chain. Only if you thought to write that test to begin with. Writing a test for everything is... not really possible. SQLite3, one of the most tested codebases in the world, has a private testsuite that gets 100% branch coverage, and even that is not the same as testing every possible combination of branches. > 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. It's not. The reason the strictness flag was added was that OpenSSL was historically less strict than the spec demanded. It turns out that when you're dealing with more than 30 years of history, you get kinks in the works. It wouldn't be different for whatever thing replaces PKIX. > 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 [...] You must be very popular at parties. > I'm also guessing that your budget estimate is an exaggeration since miTLS and EverCrypt, [...] Looking at miTLS, it only claims to be an implementation of TLS, not PKIX. Not surprising. EverCrypt is a cryptography library, not a PKIX library.

wizeman 6y ago
> That's just an argument for better testing. That's not implementation verification. No, I'm not talking about testing, I'm talking about really basic formal verification: forall (x: Certificate), verify_certificate(x, flags = 0) == invalid ==> verify_certificate(x, flags = STRICT) == invalid This is trivial to specify and almost as trivial to prove to be correct for all inputs. Testing can't do that, no matter how good your testing. > Only if you thought to write that test to begin with. Writing a test for everything is... not really possible. I agree, but I'm not talking about testing. I'm talking about formal verification. > It's not. The reason the strictness flag was added was that OpenSSL was historically less strict than the spec demanded. It turns out that when you're dealing with more than 30 years of history, you get kinks in the works. It wouldn't be different for whatever thing replaces PKIX. That's totally fine and wouldn't affect the verification of that function at all. This is a very simple property to verify and it would avoid this bug and all similar bugs in that function (even if that function calls other functions, no matter how large or complex they are). Other functions also have such easy to verify properties, this is not hard at all to come up with (although sure, some more difficult properties might be harder to verify). > You must be very popular at parties. I didn't want to be dismissive of OpenSSL devs or other devs in general, I just find it frustrating that there are so many myths surrounding this topic, and a lot less education, interest and investment than I think there should be, nowadays.