1. 21

The interesting meat is in:

  1.  

  2. 3

    I was already recommending people turn your WireGuard work into a stand-alone library for making tunnels we can run all sorts of other stuff through. Now you’re including verified ECC implementations? That’s awesome! Keep at it!

    1. 4

      I’m actually working on turning that into the kernel’s second generation crypto API. Stay tuned for more on that.

    2. 3

      It says it verifies for memory safety, functional correctness, and secret independence. Could someone expand on exactly what is meant by that latter two?

      Does “secret independence” mean constant time as a function of the secret and input size?

      1. 4

        Functional correctness means you’ve precisely specified what it’s supposed to do and proven it does it. Secret independence is basically about avoiding timing attacks (i.e. side channels). You might find the slides helpful.

        1. 2

          Those slides are fantastic! Thanks, Nick!

          Do any of these proofs covers things like spectre? They must include some model of the cpu to be able to prove anything, right? Is it just as I said, and they prove that the time is not a function of the secret (for the given cpu model)? E.g. I can imagine a cpu which takes longer to multiply by 5 than any other number, and I don’t see how any normal proof would cover this.

          1. 3

            Answering my own question, from https://eprint.iacr.org/2017/536.pdf :

            Yes they do have a cpu model, but it is very simple. They have a few operations which are assumed to be constant time on the cpu. They even explicitly call out non constant time integer multiplication on some cpus (but they ignore this). They use a cool technique of defining a new type (a secret int) to represent the secrets which doesn’t have a compare operation. Very nice.

      2. 1

        Great, but when oh when will you stop telling me not to use it? IPsec has stolen too much of my life…

        1. 1

          Is this the same HACL X25519 implementation as NSS uses, or are there two distinct implementations on the same formal verification tooling?

          Does it make sense to have a cryptography library (in the style of OpenSSL’s libcrypto) to ease distribution and use of formally verified algorithm implementations?

          1. 2

            Is this the same HACL X25519 implementation as NSS uses, or are there two distinct implementations on the same formal verification tooling?

            NSS and I both used the same project to generate our implementations, but our C code is slightly different, due to kernel constraints. For example, the kernel doesn’t like C99 declarations-after-statements, so a special option must be passed to HACL* to have output that is suitable for C89.

            Does it make sense to have a cryptography library (in the style of OpenSSL’s libcrypto) to ease distribution and use of formally verified algorithm implementations?

            I’m pretty sure this is what HACL* is trying to do, in general. They have a lot of different primitives verified and available. Impressive project.

            1. 2

              They spent who knows what amount of time and money specifying and verifying this stuff down to imperative code. Then, they casually mention this afterward:

              “For convenience, C code for our verified primitives has already been extracted and is available in snapshots/hacl-c. To build the library, you need a modern C compiler.”

              McCoy: “You want me to get trustworthy assembly by running verified C through a modern C compiler? My God, man, I’m not Xavier Leroy!”

              1. 3

                INRIA also makes compcert – http://compcert.inria.fr – which you’ve probably heard about. HACL* appears to have a mode meant for targeting the compcert compiler. So you can do it this way if you’re feeling anxious.

                1. 2

                  Oh yeah. I was mostly kidding. Note that CompCert is proprietary software. They currently allow non-commercial usage of it. Depending on one’s circumstances, the verified C might be available but CompCert might not. It’s why I recommend where possible to add verified assembly using free tools like Simpl/C or x86/Proved. The users can pick what level of risk they want when choosing either the C or whatever assembly was included.