Hacker News Reader

Comment by gefh | Hacker News Reader

It turns out software was only reliable in the dimensions we we carefully looking at. I'm not sure 'proof' would have helped any - we might well have proved that, say, Flash could successfully display any valid animation you could throw at it without even thinking about whether it was also pwning your machine.

View on HN

Proofs in software are more complicated than that. For something like flash, you could have proofs that it handles corrupt, either intentionally or unintentionally, data without blowing up.

Then again, I'm one to believe that we need to focus more on capabilities systems, and other ways to ensure applications can only do what they want to do. Look at something like the rowhammer attack. Being able to break out of a sandbox through completely valid code is something we should be looking at mitigating as well.

Rowhammer is a great example of something that a perfectly reasonable looking proof would have missed!

Most of the security vulnerabilities involve C undefined behaviour. Any proven-correct program necessarily won't invoke undefined behaviour.

(We could also have used memory-safe languages)

Correct, but "undefined behaviour" sometimes mean "defined by machine"

I mean, pretty much the same way as int or size_t has a machine type size dependency

Not true in theory or in practice. "Undefined behaviour" has a specific meaning in terms of the C standard, distinct from "implementation-defined behaviour" like the size of int or size_t. And in practice, writing beyond the bounds of an array almost always leads to arbitrary code execution (remote in the case of a networked program), double free almost always leads to arbitrary code execution, signed integer overflow on newer compilers sometimes leads to arbitrary code execution, ...

Many, but I'm not sure most. However they nearly all involve someone (be it the language designer, compiler writer or application writer) not thinking about all the malicious possibilities of the code in question. Because that's not the problem they're trying to solve right now, and they're only human. And I only use security vulnerabilities as an example - the next thing we're all not thinking about might be power consumption, or creating AI paradoxes, or whatever. But we're definitely not thinking about it, and no-ones going to be proving it.

Also there are probably zero non-toy programs out there that don't have any undefined behavior in them :)

> And I only use security vulnerabilities as an example - the next thing we're all not thinking about might be power consumption, or creating AI paradoxes, or whatever. But we're definitely not thinking about it, and no-ones going to be proving it.

I don't think you have to be thinking about it. Every time some new class of vulnerabilities has arisen, e.g. SQL injection, it just hasn't affected well-formed programs written with good tools, and certainly not verified programs. Correct programs just don't have these problems, as a side effect of being correct.

The problem with "proofs" is that software is often an iterative process because the environment and problems are constantly changing. If you have a fixed known problem you can do proofs to your hearts content, but in a changing environment you make the most of it with limited resources.

You don't have to proof everything. Eg just halting is good enough for a lot of things. (And this is not the general halting problem. Writing programs that provably halt is almost trivial.)

Reply on news.ycombinator.com