Verified cryptography for Firefox 57
blog.mozilla.org
Verified cryptography for Firefox 57
1–10 of 15 posts
Re: Verified cryptography for Firefox 57
#2Beware of bugs in the above code; I have only proved it correct, not tried it.
Donald KnuthRe: Verified cryptography for Firefox 57
#3As CS was originally born largely from people with math backgrounds, formal proofs were all the rage for software early on. As time passed and software became more complex, that requirement effectively dropped off to some academia and defense/high-risk (aka nuclear controls) projects.
Now amazon is trying to formally verify a lot of AWS with TLA+ and other techniques. Here Mozilla is trying to verify it’s crypto.
Given the increasing rise of cyber security problems and their consequences, will formal verifications once again become more standard in software engineering? At minimum, we’ll need to see more user-friendly variants of TLA+ and other techniques for average developers to be able to use. Probably it should be taught in normal CS education. Even better would be for some kind of AI to help take existing code or specs and put it into something that can be formally proved.
Re: Verified cryptography for Firefox 57
#4> As an additional bonus, besides being formally verified, the HACL Curve25519 implementation is also almost 20% faster on 64 bit platforms than the existing NSS implementation
Bravo! Looking forward to that.
Re: Verified cryptography for Firefox 57
#5As CS was originally born largely from people with math backgrounds, formal proofs were all the rage for software early on. As time passed and software became more complex, that requirement effectively dropped off to some academia and defense/high-risk (aka nuclear controls) projects. Now amazon is trying to formally verify a lot of AWS with TLA+ and other techniques. Here Mozilla is trying to verify it’s crypto. Giv…
> Here Mozilla is trying to verify it’s crypto.
If you look at the paper describing this work " rel="nofollow">https://arxiv.org/abs/1703.00053>, you'll see that this is an academic effort and 7 of 12 authors are actually at Microsoft Research. But kudos to Mozilla for bringing all this advanced stuff to their products.
Re: Verified cryptography for Firefox 57
#6Most interesting to me is that it's implemented in a language I'd never heard of, F* (https://www.fstar-lang.org/), which is an ML that compiles to OCaml, F#, or a subset of the language can compile to C. It's intended for just this sort of work ("verified effectful programming" is seemingly one of their taglines for the thing).
That's pretty neat. I like seeing exotic languages used in mainstream projects. It's just fun, ya know? Firefox is also shipping with some Rust code these days.
Re: Verified cryptography for Firefox 57
#7Most interesting to me is that it's implemented in a language I'd never heard of, F* ( https://www.fstar-lang.org/ ), which is an ML that compiles to OCaml, F#, or a subset of the language can compile to C. It's intended for just this sort of work ("verified effectful programming" is seemingly one of their taglines for the thing). That's pretty neat. I like seeing exotic languages used in mainstream projects. It's ju…
F* is a great project and under very active development. Basically at every POPL you find papers with genuine improvements and simplifications to the core of F*. I don't know of any other language that's improving this rapidly.
Re: Verified cryptography for Firefox 57
#8Beware of bugs in the above code; I have only proved it correct, not tried it. Donald Knuth
While this is a fun aphorism, it's getting less and less applicable these days since many proof systems (and programming languages that double as such) allow for code extraction to e.g. ML or C code. Naturally, the usual caveats apply: You'll want proof that the code extractor is correct. (But then, you'd want proof that the proof system itself is correct, regardless.)
Nevertheless, the aphorism is part of the reason that I'm (also) sceptical of using proof systems that don't allow for code extraction. Assuming you're actually trying to prove things about programs and just just proving things for e.g. math.
Re: Verified cryptography for Firefox 57
#9As CS was originally born largely from people with math backgrounds, formal proofs were all the rage for software early on. As time passed and software became more complex, that requirement effectively dropped off to some academia and defense/high-risk (aka nuclear controls) projects. Now amazon is trying to formally verify a lot of AWS with TLA+ and other techniques. Here Mozilla is trying to verify it’s crypto. Giv…
> Here Mozilla is trying to verify it’s crypto. If you look at the paper describing this work " rel="nofollow">https://arxiv.org/abs/1703.00053> , you'll see that this is an academic effort and 7 of 12 authors are actually at Microsoft Research. But kudos to Mozilla for bringing all this advanced stuff to their products.
Bad link. Should be: https://arxiv.org/abs/1703.00053
Re: Verified cryptography for Firefox 57
#10Beware of bugs in the above code; I have only proved it correct, not tried it. Donald Knuth
While this is a fun aphorism, it's getting less and less applicable these days since many proof systems (and programming languages that double as such) allow for code extraction to e.g. ML or C code. Naturally, the usual caveats apply: You'll want proof that the code extractor is correct. (But then, you'd want proof that the proof system itself is correct, regardless.) Nevertheless, the aphorism is part of the reason…
You don't need to prove that the proof system is correct. It suffices to extract a proof of the properties you care about for the particular program you care about, and then check that that particular proof is correct. This can generally be done with a very simple proof-checker whose own correctness can fairly easily be checked by hand.