| |||||||||||||
A look at the MS-SQL wormA look at the MS-SQL wormPosted Jan 30, 2003 2:09 UTC (Thu) by JoeBuck (subscriber, #2330)Parent article: A look at the MS-SQL worm
I think an argument over whether Karsten's numbers are right might be missing an important point: while he may not be right in his suggestion that in this case 99% of the people applied the patch and we still had major damage from the worm (I, for one, doubt this), I could easily conceive of future cases where this might be true. Consider this scenario: a remote exploit is discovered in Apache. Patches are quickly produced, but only 99% of people running Apache apply the patch by the time that a worm is deployed. The worm is designed to generate so much traffic as to completely saturate a number of crucial backbone links, and it's smartly written (that is, it closes the security hole behind itself, so that the same hole can't be used to clear the infection; it stores itself on disk, so that a reboot doesn't cure it). Blocking the SQL port is one thing; blocking port 80 all over the net basically turns off the web, generating massive economic disruption. 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. This is probably only feasible if applied to very small pieces of code, but perhaps software can be architected so that the volume of code that is ever exposed to untrusted data is kept very small, so that it can be proved to be free of buffer overflows, vulnerability to cross-site scripting and similar attacks, and race conditions. OpenBSD-style code auditing won't do the trick: to have hope of proving safety properties you pretty much have to design the code and the proof together. Such techniques don't have to be incompatible with C (though C does make things harder). Some form of assume-guarantee approach can be used to determine preconditions and postconditions for each function, and given a meticulous effort it might be provable that a given daemon contains no buffer overflows, or that cross-site scripting is impossible, or that it's not possible to get to a shell. I would expect that it will take 100 times as long to write such code, but it could be argued that this most be done to ensure the continued operation of the net (so maybe government funding could be obtained).
(Log in to post comments)
A look at the MS-SQL worm Posted Jan 30, 2003 9:21 UTC (Thu) by skellba (guest, #8043) [Link] formal proof of correctness of programs is pratically impossible: the task is too big to be done. It would be better to not use programming languages like C or C++ which are inherently prone to buffer overflows and memory overwrites.What me really concerns is that there are so many database-servers obviously not behind a firewall: this is definitiv a problem of understanding network security and missing knowledge about Microsoft products.
A look at the MS-SQL worm Posted Jan 30, 2003 10:29 UTC (Thu) by libra (guest, #2515) [Link] -> "missing knowledge about Microsoft products"But who should care about that? It is not a problem of knowing Microsoft or Linux or Solaris or whatever. The problem is understanding what you do, this require knowledge about something more basic : TCP/IP, Filtering, 3-tier architecture etc... I personnaly feel as confident with Microsoft or Linux not because I know one or the other extremly well, but because I can analyse and try to understand what I do. This is a lot more difficult on Windows because everything is hidden in metabases, registry, secret entries and behind frustrating GUIs but for the basics I can still manage what I need. So the problem is not knowledge about Microsoft to my opinion, it is basic knowledge and intelligence. But of course how do you want people to devellop both when they lose their time with bugs and patches to correct them?
A look at the MS-SQL worm Posted Jan 30, 2003 11:11 UTC (Thu) by NAR (subscriber, #1313) [Link] It would be better to not use programming languages like C or C++ which are inherently prone to buffer overflows and memory overwrites.I heard once a guy, who proudly announced his 100 line long secure webserver written in perl, and asked folks to audit it. Of course, it is not that hard to audit 100 lines of code, even if it's written in perl :-) But don't forget, that the C code of the perl interpreter should be audited also, and that is not 100 lines long...
Language versus application security Posted Jan 30, 2003 12:36 UTC (Thu) by copsewood (subscriber, #199) [Link] I think the people who design and implement very high-level programming languages (e.g. Perl, Python, Java, SQL, - 'C' is too low-level) are somewhat more likely to be able to write interpreters secured against buffer overflows etc. than the people likely to be writing network-based applications which use these tools, due to the likely differences in programming knowledge and experience.Hence it is likely that an application designer needs less security knowledge to design a reasonably robust web application in Perl (which does the memory management housekeeping within the language) than in 'C' (which manages memory within the application). Not only that but the ISP hosting virtual domains is likely to want to patch insecurities discovered in the language runtimes much quicker than most of the domain owners will patch insecure web applications.
Language versus application security Posted Jan 30, 2003 18:21 UTC (Thu) by JoeBuck (subscriber, #2330) [Link] Perl doesn't have buffer overflows, but Perl-based web applications have had tons of security holes, mostly caused by not sufficiently checking user-supplied data (../../.. in paths, cross-site scripting, and the like).
Language versus application security Posted Jan 31, 2003 0:54 UTC (Fri) by copsewood (subscriber, #199) [Link] Yep. The approach of deciding what valid data should look like and excluding everything else is similar to the default-deny approach to firewall setups. This can reduce functionality slightly or slightly increases the effort of getting added functionality secure, but its probably much less hassle than trying specifically to exclude what is considered dangerous when you can only ever have limited knowledge of what might be exploitable in future.
A look at the MS-SQL worm Posted Jan 30, 2003 12:11 UTC (Thu) by philips (guest, #937) [Link] > formal proof of correctness of programs is pratically impossible:> the task is too big to be done. It would be better to not use > programming languages like C or C++ which are inherently prone to > buffer overflows and memory overwrites. Take a look at: ----- quote start ----- In other words, you have to open source at some degree your application Another language buys you nothing - implementation & design flaws is
MS-SQL worm - open source not needed for B1 rating Posted Jan 30, 2003 20:27 UTC (Thu) by wittenberg (guest, #4473) [Link] You don't need to open source to get B1 certification. Ten years ago I worked on a product that was to have been certified A1. We had to show our code to NCSC, but only under a non-disclosure agreement. So you need other people to look at the code, but you don't let everyone look at it.
A look at the MS-SQL worm Posted Jan 30, 2003 11:07 UTC (Thu) by NAR (subscriber, #1313) [Link] 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.
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:
|
|||||||||||||