Security is Mathematics(daemonology.net) |
Security is Mathematics(daemonology.net) |
* Mark Dowd
* John McDonald
* Alex Sotirov
* Dino Dai Zovi
* Charlie Miller
* Michal Zalewski
* Aaron Portnoy
* Dave Aitel
* David Litchfield
* Barnaby Jack
This doesn't invalidate the blog post, but I will go on to suggest that quite a lot of people with extensive formal training in mathematics either (a) have/had careers in software security with less spectacular results than e.g. Aaron or Michal or (b) have produced, despite incentive to the contrary, some really crappy code.
Rolf Rolles is a very smart guy, but he's not a security researcher; he works in content protection and reverse engineering. Having said that: sure. That's one. One. :)
You mean the Charlie Miller who has a PhD in mathematics, right?
Also, did you seriously just write a list of top-tier security researchers which didn't include djb?
Rolf Rolles is more of a security researcher --- a lot more --- than Daniel Bernstein. But I'll concede it! He's a third.
We're at 3. Do you think I can't name 10 more notable security researchers, justifying each of them, to back up my point here?
My boss told me a similar story of a computer science professor giving a cross-group talk in which he pitched the concept of formal methods to a group of physicists who, among other things, programmed collectors for particle experiments. (Supposedly this happened at Cornell in the seventies.) The CS professor enthusiastically and animatedly proved the correctness of an algorithm for solving a simple graph-coloring game and then asked whether there were any questions. One of the physicists raised his hand and asked, "How fast does it run?"
"That's the beauty of formal methods! Now that I've proved the algorithm correct, I already know it will produce the right answer. There are far too many possible inputs to verify correctness via testing, so there's actually no point in running it at all."
The problem with writing secure code that works well is making sure that all inputs conform to your well-defined set... i.e. they are a subset of your well-defined set.
Compounding on this is the non-apparent dimensionality of your sets. A good example of this would be concurrency. If a function doesn't have an exclusive lock an an array of data it's going to manipulate, the set could actually have two dimensions (one being time), in which the array could change.
I got a C- in Analysis II. I needed a C to get a Math minor, but decided it wasn't worth it.
It is true that you need to make sure your software conforms to its specifications and that process does involve informal (or formal) proof-like reasoning, but that is only a small part of the challenge. This is the part that mathematicians would be good at, but other technologies are good at the this as well (type checkers prove weak properties, verification tools prove stronger ones). None of this requires a "twisted mind", just attention to detail.
The problem of writing software specifications that correspond to the abstract notion of security is the tougher task. In math, the closest analogy is figuring out what theorems people actually care about. While I don't know for sure, I'm skeptical that a math education emphasizes this skill. Security takes this skill a step further and requires Schneier's "twisted mind" to consider all the real-world ways that things could go wrong (including, among other things, the incentives that might motivate an adversary) and write specifications for secure, but useful, software.
I read this as saying that the mindset required to write proofs is similar to the mindset required to write secure software. The proof mindset is useful for considering “all the real-world ways that things could go wrong.”
I think the paragraphs about Knuth’s famous quote just muddy the water.
Bingo.
I have a degree in math and can see how my attitude changed as I progressed. When taking my first analysis class I was sure it is no coincidence the word begins with anal. It took a while for me to develop habits of skepticism about things that seem obvious at first glance. That's the attitude I think he is describing.
I'm going to steal that line, if you don't mind. :-)
It took a while for me to develop habits of skepticism about things that seem obvious at first glance. That's the attitude I think he is describing.
Yes. The attitude of "I don't care if this looks right; am I absolutely certain that it is right, in all possible universes consistent with my axioms".
But in any case, the gist of the article is correct -- the rigor used in math proofs is the MIN bar for security code.
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.
Which programs and which proofs?
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.
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.
I think we'll have to agree to disagree here. But given our different focuses in security, it's not all that surprising that we have different definitions of "security researcher".
- 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.
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...
(Some people seem to get the idea economics is like accounting but vaguer, like a climatologist is to a weatherman or something. Macro economics is the bit that gets in the media most often, but it's also the most ideology-based rather than fact-based.)
This is why big companies with content everyone craves have such a hard time with DRM -- there's just too much firepower arrayed against them. If you look closer, you find that "DRM Doesn't Work" isn't quite true. It's just not as strong as Phillips or Sony would like it to be.
Here's Ross's "Economics and Security" resource page http://www.cl.cam.ac.uk/~rja14/econsec.html