A look at the MS-SQL worm
Posted Jan 30, 2003 11:07 UTC (Thu) by NAR
In reply to: A look at the MS-SQL worm
Parent article: A look at the MS-SQL worm
I think that the only way out of this mess is to start to think about techniques that can yield formal proofs that certain flaws are not present.
Don't forget, that formal proofs work on only formal programs. As soon as you start to type in a formally proved program, flaws can creep in, and no formal proof can protect from this. You still need testing and code audit. BTW the formal proving methods I studied at the university usually concentrated on what the program should do with the correct input. They didn't deal with incorrect inputs (i.e. it was enough to prove, that the program works on the specified inputs, noone cared, what happens with incorrect input, because it was out of scope), but most flaws are exploited only by incorrect input.
The other thing is that formal proving is an extraordinarily timeconsuming process, even on small, but parallel programs, and it needs strong mathematical tools (i.e. no high school kid will do it). I think that your "100 times" assumption is quite low, but imagine, if you have to wait 200 years for the next stable Linux kernel instead of 2 years.
to post comments)