Slashdot Mirror
Microsoft To Teach Undergrads About Secure Computing
Update: 03/24 18:00 GMT by J : Another report worth reading is Writing Software Right, which requires a free but annoying registration at Technology Review. This regards automated methods of finding software errors (not security specifically). Sun's "Jackpot" is discussed, a lint that also "identifies general instances of good or bad programming."
And Microsoft's efforts in this field are explained as well -- the company "paid more than $60 million in 1999 to acquire Intrinsa, maker of a bug-finding tool called Prefix. The program, which sifts through huge swaths of code searching for patterns that match a defined list of common semantic errors, helped find thousands of mistakes in Windows and other Microsoft products." As a Microsoft QA person says, "Our challenge is to get our software to the point that people expect it to work instead of expecting it to fail."
You can find a description here.
The only difference is that this module was intended to make undergrads see the failure and risk by means of software engineering, and we did this by looking at various procedures for writing secure code, and we looked at lots of examples from history (the challenger incident, for example, etc).
This course seems to be aimed more at specific coding practices - avoiding buffer overruns for example. It doesnt look like they'll be told how to deal with failure once it happens (because it *will* happen). I also fear that since Microsoft will be involved, it'll be specific to Windows & x86 -- not a real life view of computing.
I was wondering how OS-agnostic these courses are going to be, when I came across this quote:
Okin agreed: "We need to get input from others as well. Clearly, there is no point in these undergraduates learning only about Microsoft technology. We need a broad approach."
The reason I wondered was because so much of secure programming involves access control in many ways, direct and indirect. Obviously, Microsoft's access control mechanisms vary wildly from Unix paraadigms. I'm not a hardcore programmer, but I can only assume that priviledge escalation exploits under a Redmond OS would be very different from something similar with linux.
That sentence states unambiguously that the course will cover non-MS architecture.
I, for one, am impressed. Doing the right thing for once, the boys in Redmond.
Blearf. Blearf, I say.
I forget where I heard it, but someone once pointed out that if your going to go to Spain to participate in the running of the bulls, you don't really want to talk with the people that managed to survive it... you want to talk to the guy that got his ass gored off because he can tell you exactly what to avoid doing!
Same thing here! Who better to tell us what security bugs to avoid than Microsoft.
If a pion (n-) collides with a proton in the woods & noone is there to hear it, does lamdba decay into the source pa
The technique you describe is part of a field known as "Formal Methods".
The term "cleanroom" comes from reverse engineering, where you have team A of engineers write a spec for a competitors product and team B (who've never seen the product) write an implementation. This gives you some degree of legal protection, but does not prove anything about correctness.
Of course, the flaw with formal methods is that they only prove the program is functioning as designed - which is definitely a worthwhile goal, but does not say anything about the correctness of the design itself. E.g., think of the problems with the incorrect mirror for the Hubble Space Telescope - the grinding machine worked perfectly, but the final mirror was still ground to the wrong shape.
I believe their real motive in offering such a course would be to teach programmers to code for security the Microsoft way, so that things continue to get worse. Their definition of security of your machine is much like their definition of digital rights of your machine; they are not looking after your digital rights, and they are not looking after your security.
I'm an American. I love this country and the freedoms that we used to have.
I've used formal methods in a few places... much to the indifference of colleagues. I remember one time finding a subtle bug via Z-notation and fixing it, then moving on to another project while several of my former coworkers criticized my code as "unnecessarily complex," etc. A couple years later I happened to overhear a conversation that strongly suggested somebody had "cleaned up" my code, then actually encountered that rare, subtle bug years later and had great difficulty (and pride) in fixing it.
So formal methods are extremely powerful... but I rarely use them now. The problem is that few problems are so well defined that you can use them in a meaningful manner. If you're writing low-level code - something on the level of string libraries or date routines, use them. But as you get closer to real world problems, the formal methods seem more effective at driving home how little you understand about your problem space, not writing solid code.
(As a specific example, I remember getting nailed by the concept of "triangle." We were writing meteorological code, and sometimes "triangles" were planar and sometimes they were triangles on a sphere -- and the problems are *very* different as you move away from small triangles. Some of our code did - many navigation problems can be reduced to triangles with the two endpoints and the North Pole.)
For every complex problem there is an answer that is clear, simple, and wrong. -- H L Mencken
I'd say some of the gems of my book collection are from Microsoft Press. In particular, anything written by Jefferey Richter or Charles Petzold I'm willing to take on faith will be outstanding.
Irrespective of feelings towards Microsoft (and I'm pretty far into the anti-MS camp), their Microsoft Press division has released some darn fine books.
(Note: I only own 4 MS Press books, and all have been outstanding. This does not mean that there aren't hundreds of MS Press books that are crap, but that hasn't been my experience.)
Alan