Joe Yao writes:
> In short, Marcus was first saying that you can't prove that software is
> flawless; then he was saying that you can't prove it safe. Wherein
> lies the contradiction?
I was saying something even stupider and less interesting
than that. :) I said you can't prove something is flawless,
and then bolstered it with
> "As far as I have seen, there is *no* software that can be proven
> to be "safe"..."
...which is more along the line of an experimental observation.
That observation was based on my experience with formal
proofs of software "correctness." In general, I've found those
attempts to be pretty silly because they make all kind of
assumptions in order to succeed, and they prove only very
simple programs that are completely self-contained. So,
what you wind up with is a formal "proof" that a program
which does no I/O or hardly anything else, running on
flawless hardware (no microcode errors, or ram errors or
disk errors, etc) will operate flawlessly.
The problem is that we can't practically make
ourselves comfortable with code, yet we are making
it more and more important to many aspects of our
lives. We've seen that mis-designed software (designed
without security) is much harder to fix and retrofit
security into, but yet there is no way of stemming the
huge tide of code that is built without security. The
industry/market pressures are making it increasingly
hard to secure systems at the same time as it's making
it increasingly important that our systems be secure.
In other words, things suck and the suction is increasing.
mjr.
-----
Marcus J. Ranum, CEO, Network Flight Recorder, Inc.
<A HREF=http://www.clark.net/pub/mjr>Personal</A>
<A HREF=http://www.nfr.net>Work</A>
<A HREF=http://www.clark.net/pub/mjr/websec>New Book!!</A>
|
|
