Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Verified cryptography for Firefox 57

blog.mozilla.org

Post reply on HN
Print view View original

11–15 of 15 posts

Re: Verified cryptography for Firefox 57

#11

Post by lomnakkus »

roca wrote: post #10
lomnakkus wrote: post #8

Earlier quoted context omitted.

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.

True, but that adds an extra burden for programmers... and if proof systems are ever going to gain widespread acceptance (that'll be the day!), the ergonomics of using them need to be improved. (That is, having an extra manual step is not acceptable.)

Re: Verified cryptography for Firefox 57

#13

Post by dsacco »

SwellJoe wrote: post #6

Most 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 somewhat well known in circles of information security, but it's not widely used in general. It's frequently used for formal verification of cryptographic protocols. If you look at the papers on the website you'll see a variety of applications for provable security in crypto.

I wouldn't call it a general purpose language (in the sense that you can productively use it for just about anything), but to be fair I've only read papers about/using the language; I've not used it personally. It's a great leap forward for provable security in general, though.

Re: Verified cryptography for Firefox 57

#14

Post by lower »

tfcata wrote: post #12

Sadly, formal verification works only for small amount of code, a few thousands lines of code when I looked at it a while back. It doesn't stop us from imagining a fully verified firefox though.

> a few thousands lines of code when I looked at it a while back.

That's not true anymore. Have a look at CompCert, CakeML or CertiKOS, for example. Verification still takes a big effort, but it's getting better a lot.

Re: Verified cryptography for Firefox 57

#15

Post by pron »

azinman2 wrote: post #3

As 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…

> At minimum, we’ll need to see more user-friendly variants of TLA+ and other techniques for average developers to be able to use.

TLA+ is quite user-friendly, certainly more than most other formal methods. It takes about two weeks to become fully productive, without any guidance other than the freely available tutorials. It's easier to learn than most programming languages.

> Probably it should be taught in normal CS education.

I agree.

Post reply on HN