Is nothing enough? [LWN.net]

Is nothing enough?

Posted Apr 28, 2012 0:57 UTC (Sat) by Company (guest, #57006)
In reply to: Is nothing enough? by kripkenstein
Parent article: Fuzzing for Security (The Chromium Blog)

You know those math proofs you have to do? There's 2 types: "There exists one element that..." or "There exists no element that...". The first one is hard to do usually - you need to find the one element that qualifies, but the second one is a lot harder, because you need to look at every possible element and prove that things hold.

Security is like that: The crackers need to find the one element that breaks things. And the developers need to prove that for all possible inputs, the output is valid to be sure they don't have security issues.
As a side note, that proof would be equal to a formal proof of the correctness of the software. And I remember my university courses about how possible that is even for simple systems (read: Touring machines).

So in short: It's de-facto impossible to make a browser (security-) bug-free. It's just a question of time until people find the next bug and exploit it. Most likely, they are already doing it.

to post comments

Is nothing enough?

Posted Apr 28, 2012 22:07 UTC (Sat) by MisterIO (guest, #36192) [Link] (6 responses)

That's incorrect. It's de-facto impossible to _prove_ that a piece of software doesn't have bugs, but that doesn't mean that you can't actually write bug-free code. Just talking about theory.

Is nothing enough?

Posted Apr 29, 2012 0:05 UTC (Sun) by Company (guest, #57006) [Link]

That's incorrect. It's de-facto impossible to _write_ a piece of software that doesn't have bugs, but that doesn't mean that you can't actually prove code being bug-free. Just talking about theory.

Is nothing enough?

Posted Apr 29, 2012 1:37 UTC (Sun) by mrons (subscriber, #1751) [Link]

I'm reminded of the following quote by Knuth:

"Beware of bugs in the above code; I have only proved it correct, not tried it."

Is nothing enough?

Posted Apr 30, 2012 20:51 UTC (Mon) by quentin.casasnovas (guest, #58238) [Link]

Saying it is
> de-facto impossible to _prove_ that a piece of software doesn't have bugs
does sound a bit strong... Do you have a proof to back-up that somewhat no piece of software can be proven bug-free? I think it is sometimes possible: in synchronous languages for example, using formal analysis.
Think also about pure functions, which could certainly be proven bug-free mathematically. Lambda calculus and functional languages are an extent to that.

Is nothing enough?

Posted May 3, 2012 5:46 UTC (Thu) by Comet (guest, #11646) [Link] (2 responses)

So formal methods do not exist?

Is nothing enough?

Posted May 3, 2012 14:29 UTC (Thu) by nybble41 (subscriber, #55106) [Link] (1 responses)

> So formal methods do not exist?

No, they're just impractical for software of any reasonable complexity. The largest piece of software I've ever heard of which had a formal proof of correctness was a version of the L4 microkernel--essentially not much more than a low-level message-passing interface, with less than 9k lines of C code--and even then the proof is only as good as the requirements defining "correctness".

[1] http://ertos.nicta.com.au/research/l4.verified/

Is nothing enough?

Posted May 4, 2012 5:00 UTC (Fri) by AndreE (guest, #60148) [Link]

Probably of greater interest is this page.

http://ertos.nicta.com.au/research/l4.verified/proof.pml