Comment by zepolud | Hacker News Reader

Comment by zepolud | Hacker News Reader

To take it one step further, it might be a good idea to specify the whole thing in Coq, prove correctness and derive the C code from there. Coq is a theorem prover based on the Martin-Löf type theory like the ATS mentioned in the article. Xavier Leroy (the man behind OCaml) managed to write a whole verified C compiler in Coq[1] so while it's slower than writing C directly it should still be feasible for projects of such critical importance.

On a related note, mathematicians are also finding it increasingly difficult to trust unverified proofs. Papers by Vladimir Voevodsky, a Fields medalist and one of the most prominent in the field, were also discovered to contain errors more than ten years after publication, having been cited hundreds of times and nobody noticing the errors in the proofs. This was one of the principal motivations for him to initiate the project for homotopy type theory, which also has roots in Martin-Löf type theory and is also being developed formally in Coq.

[1]http://compcert.inria.fr/diagram.png

I've said it before and I'll say it again.

Formalizing the TLS specification and proving that an implementation is consistent with it only shows that the implementation is logically correct. However, it does NOT show that the implementation is secure. Your implementation can be vulnerable to side-channel attacks (particularly timing attacks) while still being logically correct.

Proofs of correctness are a (big) step in the right direction, but they're not a silver bullet for building a secure implementation.

You can use mathematics to prove other things as well. You could e.g. use a special bool type for all secure data that you can't branch on, so that no secrets could be exposed by examining the runtime path of execution. Or build a model of your CPU's caching and prefetching behaviour and prove that you're code doesn't expose any secrets by that channel.

How complex must that model be?

At least as complex as a real CPU, so we're back on square one.

Right--this will work on some types of side-channel attacks. For example, I could prove that my decryption function runs in a constant amount of time no matter the input.

However, you can't proactively defend against side-channel attacks. By definition, a side-channel attack exists because the designer didn't know that the cryptosystem leaks information when (s)he designed and proved the correctness of the implementation.

Proving that the cryptosystem doesn't leak information is damn nigh impossible, and often outside the scope of software engineering. My favorite example is acoustic analysis (https://www.cs.tau.ac.il/~tromer/acoustic/). Before this was shown to be possible, how were cryptosystem designers supposed to know to defend against it?

The best we can do is come up with and formalize a threat model, and then prove that the cryptosystem is secure against the adversaries in the threat model. The problem is that threat models don't help you with adversaries in the future, who have means of getting information from your cryptosystem that you didn't think of.

I take your point, but I don't think _anything_ can defend against unknown attacks. However, we could defend against all known attacks using formal methods, which is a lot better than we're doing at the moment. Further, when a new attack becomes known, I would wager that having something that is verifiable today will be easier to verify or fix in the future, as compared to a code-base that is not provable.

Just because we can't achieve theoretical perfection, we should not rule out using methods that would solve many of the actual problems we encounter today.

Of course, if you can find a way to defend against unknown future problems, I'm all in favor of using your method!

Unknown-unknowns as it were.

A formal methods solver for an engineering description language was the thinking behind Zed (Z notation) https://en.wikipedia.org/wiki/Z_notation

But the ideas of trusted OS and instruction might be necessary to compartment secrets to reduce their potential exposure to the least possible opportunity. It's basically impossible to completely eliminate plaintext and secrets in clear unless maths allow it, but we should still try.

Heartbleed was not a side-channel attack. It was not a subtlety of the TLS specification. It was the single most well-known, common C-based security flaw. Better languages may not solve everything but they are absolutely the solution to this class of errors.

Well-said!

Similar could be said for Goto Fail and the GnuTLS bug. I wonder how something like Coq could handle the Debian random number bug, though. Still, 3 out of 4 ain't bad.

Do any functional or logic programming languages or libraries have a concept of entropy, and entropy generating/reducing operations?

TLS has so many features that it factorially increases the attack surface to the size of the Milky Way.

A much simpler nonrepudiated authenticated encryption scheme implemented in a safer language would be an ideal way forward. It also would help to have a reference implementation and reference test suite to lock down behavior.

It occurs to me that if I was a (black hat) hacker looking for vulnerabilities, I could reimplement critical software in a safe language, leveraging the type checker to search for bugs. Is anyone aware of people doing this already?

Your reimplementation would either be very different from the original, and hence not suffer the same bugs, or the compiler wouldn't get further than a couple of function calls before giving you a cryptic error message since it doesn't understand the control flow.

Static analysis tools are useful for finding bugs in existing code, but safe programming languages won't magically point out all of the errors in some arbitrary code written in another language. They're safe precisely because they do not allow you to write code in the way that an unsafe language would.

As an analogy, if you were looking for use-after-free errors in some C code, it wouldn't do you any good to check a Python version.

Actually, your reimplementation can be identical to the original, in a language like ATS, as demonstrated by the article in question. This is one of the things I find very compelling about ATS.

You are on your way to reinventing grammar/model/spec based fuzzing. It works pretty well. Eg. it was used to find the Heartbleed bug (Codenomicon's tools at least, don't know how Google fuzzed it).

You can do specification as type in ATS2 too. My biased view is that I find ATS2 to be far more practical than using coq.

Reply on news.ycombinator.com