3 ms·

> 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

> 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
You are confusing verification as in "certificate" with verification as in "theorem proving", and you are still assuming a formal description of what to verify (which I'll remind you: doesn't exist). And then you go on to talk about myths and uneducated and uninterested devs. Your approach is like tilting at windmills, and will achieve exactly as much.
- wizeman 6y ago
  If I understood you correctly, then I am not confusing those two things. Maybe you haven't noticed but I actually wrote a theorem about a hypothetical verify_certificate() function in my previous comment. Maybe you also haven't noticed, but I didn't need a formal description of how certificate validation needs to be done to write that theorem. And I assure you, if the implementation of verify_certificate() is anything except absolute garbage, it would be very easy to prove the theorem to be correct. I actually have some experience doing this, you know? I'm not just parroting something I read, I've proved code to be 100% correct multiple times using formal verification (i.e. theorem proving) tools. That is, according to certain basic and reasonable assumptions, of course, like e.g. the hardware is not faulty or buggy while running the code, and that the compiler itself is not buggy, which would be a lot more rare than a bug in my code -- and even then, note that compilers and CPUs can be (and have been) formally verified. Maybe you don't agree with my approach but I think it's the most realistic one for a project such as this and I am absolutely confident it would be practical, would completely eliminate most (i.e. more than 50%, at least) existing bugs with minimal verification effort (which almost anyone would be capable of doing with minimal training), and would steadily become more and more bug-free with additional, incremental verification (i.e. theorem proving) and refactoring effort.
  - westurner 6y ago
    https://project-everest.github.io/ https://project-everest.github.io/ : > Focusing on the HTTPS ecosystem, including components such as the TLS protocol and its underlying cryptographic algorithms, Project Everest began in 2016 aiming to build and deploy formally verified implementations of several of these components in the F* proof assistant. > […] Code from HACL*, ValeCrypt and EverCrypt is deployed in several production systems, including Mozilla Firefox, Azure Confidential Consortium Framework, the Wireguard VPN, the upcoming Zinc crypto library for the Linux kernel, the MirageOS unikernel, the ElectionGuard electronic voting SDK, and in the Tezos and Concordium blockchains. S2n is Amazon's formally verified TLS library. https://en.wikipedia.org/wiki/S2n https://en.wikipedia.org/wiki/S2n IDK about a formally proven PKIX. https://www.google.com/search?q=formally+verified+pkix https://www.google.com/search?q=formally+verified+pkix lists a few things. A formally verified stack for Certificate Transparency would be a good way to secure key distribution (and revocation); where we currently depend upon a TLS library (typically OpenSSL), GPG + HKP (HTTP Key Protocol). Fuzzing on an actual hardware - with stochastic things that persist bits between points in spacetime - is a different thing.
    - cryptonector 6y ago
      Funny, the first hit for that search you linked is... my comment above. The "few things" other than that are for alternatives to PKIX, which is fine and good, but PKIX will be with us for a long time yet. As for Everest, it jives with what I wrote above, that verified implementations of TLS are feasible (Everest also implements QUIC and similar), but -surprise!- not listed is PKIX. I know, it sounds crazy, really crazy, but PKIX is much bigger than TLS. It's big. It's just big. The crypto, you can verify. The session and presentation layers, you can verify. Heck, maybe you can verify your app. PKIX implementations of course can be verified in principle, but in fact it would require a serious amount of resources -- it would be really expensive. I hope someone does it, to be sure. I suppose the first step would be to come up with a small profile of PKIX that's just enough for the WebPKI. Though don't be fooled, that's not really enough because people do use "mTLS" and they do use PKINIT, and they do use IPsec (mostly just for remote access) with user certificates, and DoD has special needs and they're not the only ones. But a small profile would be a start -- a formal specification for that is within the realm of the achievable in reasonably short order, though still, it's not small.

cryptonector 6y ago

You are confusing verification as in "certificate" with verification as in "theorem proving", and you are still assuming a formal description of what to verify (which I'll remind you: doesn't exist). And then you go on to talk about myths and uneducated and uninterested devs. Your approach is like tilting at windmills, and will achieve exactly as much.

wizeman 6y ago
If I understood you correctly, then I am not confusing those two things. Maybe you haven't noticed but I actually wrote a theorem about a hypothetical verify_certificate() function in my previous comment. Maybe you also haven't noticed, but I didn't need a formal description of how certificate validation needs to be done to write that theorem. And I assure you, if the implementation of verify_certificate() is anything except absolute garbage, it would be very easy to prove the theorem to be correct. I actually have some experience doing this, you know? I'm not just parroting something I read, I've proved code to be 100% correct multiple times using formal verification (i.e. theorem proving) tools. That is, according to certain basic and reasonable assumptions, of course, like e.g. the hardware is not faulty or buggy while running the code, and that the compiler itself is not buggy, which would be a lot more rare than a bug in my code -- and even then, note that compilers and CPUs can be (and have been) formally verified. Maybe you don't agree with my approach but I think it's the most realistic one for a project such as this and I am absolutely confident it would be practical, would completely eliminate most (i.e. more than 50%, at least) existing bugs with minimal verification effort (which almost anyone would be capable of doing with minimal training), and would steadily become more and more bug-free with additional, incremental verification (i.e. theorem proving) and refactoring effort.
- westurner 6y ago
  https://project-everest.github.io/ https://project-everest.github.io/ : > Focusing on the HTTPS ecosystem, including components such as the TLS protocol and its underlying cryptographic algorithms, Project Everest began in 2016 aiming to build and deploy formally verified implementations of several of these components in the F* proof assistant. > […] Code from HACL*, ValeCrypt and EverCrypt is deployed in several production systems, including Mozilla Firefox, Azure Confidential Consortium Framework, the Wireguard VPN, the upcoming Zinc crypto library for the Linux kernel, the MirageOS unikernel, the ElectionGuard electronic voting SDK, and in the Tezos and Concordium blockchains. S2n is Amazon's formally verified TLS library. https://en.wikipedia.org/wiki/S2n https://en.wikipedia.org/wiki/S2n IDK about a formally proven PKIX. https://www.google.com/search?q=formally+verified+pkix https://www.google.com/search?q=formally+verified+pkix lists a few things. A formally verified stack for Certificate Transparency would be a good way to secure key distribution (and revocation); where we currently depend upon a TLS library (typically OpenSSL), GPG + HKP (HTTP Key Protocol). Fuzzing on an actual hardware - with stochastic things that persist bits between points in spacetime - is a different thing.
  - cryptonector 6y ago
    Funny, the first hit for that search you linked is... my comment above. The "few things" other than that are for alternatives to PKIX, which is fine and good, but PKIX will be with us for a long time yet. As for Everest, it jives with what I wrote above, that verified implementations of TLS are feasible (Everest also implements QUIC and similar), but -surprise!- not listed is PKIX. I know, it sounds crazy, really crazy, but PKIX is much bigger than TLS. It's big. It's just big. The crypto, you can verify. The session and presentation layers, you can verify. Heck, maybe you can verify your app. PKIX implementations of course can be verified in principle, but in fact it would require a serious amount of resources -- it would be really expensive. I hope someone does it, to be sure. I suppose the first step would be to come up with a small profile of PKIX that's just enough for the WebPKI. Though don't be fooled, that's not really enough because people do use "mTLS" and they do use PKINIT, and they do use IPsec (mostly just for remote access) with user certificates, and DoD has special needs and they're not the only ones. But a small profile would be a start -- a formal specification for that is within the realm of the achievable in reasonably short order, though still, it's not small.