[kenjackson]

This article is correct, except it omits one important point... writing programs is harder than writing a proof. Especially security code. With sufficiently complex proofs it is often hard to find holes in the proof, but with security code (and code in general) there are ways to attack it, that just isn't doable with standard math proofs. There's no notion of "fuzzing" with proofs.

But in any case, the gist of the article is correct -- the rigor used in math proofs is the MIN bar for security code.

[sparky]

My take is that mathematics provides rigorously defined, leak-proof primitives and operations. Most of the difficulty involved in porting a piece of math to a program is in plugging the leaks in the abstractions provided by efficient machines. For example, infinite-precision real arithmetic (with no overflows, loss of entropy due to FP rounding mode, etc.) is assumed in mathematics, but is devilishly hard to get right (and fast) on fixed-width machines. Obtaining a passphrase from the user in order to hash it is assumed in the algorithm for the hash function, but in reality doing so without compromising the rest of your system can be much harder than coding the hash function correctly.

Things like side channel (e.g., timing) attacks add an orthogonal dimension of complexity to secure complexity that simply doesn't exist (or is rightly elided) in the related math.

Proofs only operate in the domain of the pure and infinite. The glue logic to interface that with the real world is what makes it tricky to write secure code, especially when errors in any part of any program can compromise an entire system (better hardware-enforced isolation between pieces of code is possible today, and indeed used, but isn't pervasive yet because performance is still king, IMO.

[wging]

>writing programs is harder than writing a proof

Which programs and which proofs?

[kenjackson]

Any program function can be cast as a theorem (although vice-verse is difficult). Proving this theorem is easier than writing the corresponding program function.

And by easier, I mean that the proof is easier to pass off as a correct proof than the program is to pass as a correct program. Of course, writing an actually correct proof is just as difficult as writing an actually correct program -- for the most part. Of course sometimes, due to real world constraints in programs (like dealing with fault tolerance or races for perf) correctness in programs can become magnitudes more difficult.

[jdp23]

I agree in the abstract, but ...

- what's the largest program you've written? - what's the largest program you've proved correctness of?

So in reality, meaningful proofs are much much much harder than writing programs.

[kenjackson]

what's the largest program you've proved correctness of?

But that's the point. With security code, while you may not prove the correctness of it, there's a black hat that's trying to find a counterexample to your "proof".

Whereas for 99% of proofs that are published in the literature no one is trying to prove that there are flaws in the proof. As someone who reviewed CS papers I would always try to really read at least one proof in the paper. Not skim, but really scrutinize it. Probably 75% of the time I could find a problem with the proof. Usually one that was easily corrected, but it was still wrong. But it took substantial effort to do this (which is why I only did one per paper and just read the other proofs).

Some recommended reading: http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/l...

[mdwrigh2]

I'd argue there is a certain notion of fuzzing with proofs. Say I have a proof claiming that a certain function is monotonic. Fuzzing, in this case, is throwing a bunch of numbers at the function and checking to see if it's actually monotonic with regards to your inputs.

Obviously not all math proofs are regarding functions and definable numbers, but there's a similar concept of fuzzing for each different proof type -- it just might not be easy to automate, or state in a programming language.

[eru]

There are some domains, like Geometry, where trying enough random numbers is actually good enough for a certain kind of proof.