| |||||||||||||
A look at the MS-SQL wormA look at the MS-SQL wormPosted Jan 30, 2003 11:07 UTC (Thu) by NAR (subscriber, #1313)In reply to: A look at the MS-SQL worm by JoeBuck 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.
(Log in to post comments)
A look at the MS-SQL worm Posted Jan 30, 2003 15:11 UTC (Thu) by utoddl (subscriber, #1232) [Link] 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)[way off topic, but...] One of the most interesting assignments in my second programming class spelled out what constituted correct input and that the program should handle incorrect input. The instructor was going to run each of our programs against an unspecified input stream, and we would be graded in part on how well we handled bad input. We were still using punch cards back then, and there were plenty of discarded punch cards lying around -- old data sets, discarded (literally!) lines from old programs, etc. The input the instructor chose was... handfulls of old punch cards he pulled from the trash in the key punch room. Snippets of FORTRAN, PL/I, raw data, arbitrary text, etc. made various programs produce, er, interesting results. It was a real eye opener to most of us; we had though "bad input" might mean something not in the right column, or a keyword slightly mispelled. Very few of the programs could handle garbage -- literal garbage -- as input. Sorry for the Old Man tale. You kids go back to your discussion...
A look at the MS-SQL worm Posted Jan 30, 2003 18:33 UTC (Thu) by JoeBuck (subscriber, #2330) [Link] 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.
A look at the MS-SQL worm Posted Feb 1, 2003 7:40 UTC (Sat) by goonie (guest, #4252) [Link] 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. Two possible approaches:
|
|||||||||||||