A look at the MS-SQL worm

A look at the MS-SQL worm

Posted Jan 30, 2003 18:33 UTC (Thu) by JoeBuck (subscriber, #2330)
In reply to: A look at the MS-SQL worm by NAR
Parent article: A look at the MS-SQL worm

I come from the electronic design automation world; when I speak of formal proof, I'm talking about the real thing, and it most certainly is possible to do, though it requires considerable expertise and it will require more research to make it scale.

Of course I know that high school students won't do this; it will take Ph.D's. And available proofs will refer to particular library routines, at most; it might be possible to prove that a given JPEG-decoding routine contains no buffer overflows or memory access errors, given a correct compiler for the language it is written in (even if that language is C).

Of course, compilers can have bugs. But we'll still be better off than we are today. And in the meantime, semi-formal techniques like the Stanford Checker are turning up hundreds of bugs in existing code. The point is that, for security testing, debuggers are no good, as you can only run a debugger with an input that you have thought of. An attacker will construct an input you never thought of to try to break your code.

The software world is way behind the hardware world on this one: after the Pentium bug cost Intel half a billion dollars, they've thrown tons of money into formal verification. Register-transfer-level to gate equivalence checking by formal techniques is well established, for example, and it is standard practice to mathematically prove that cache coherency protocols or floating point units are designed correctly.

---

(Log in to post comments)