WinHEC 2007, Microsoft’s annual event for hardware manufacturers, was held last month. It’s these event that Microsoft overcomes it’s paranoia, and discloses some of its IP in exchange for third-party support and integration.
Each year, I scrounge the Microsoft website for new information released in the event and this year I focused on the static analysis related content, which Microsoft conveniently compiled into a section of their website, Static Driver Verifier – Finding Bugs at Compile Time. This site focuses on static analysis of drivers using the Static Driver Verifier and Prefast. There are some presentations on each of these tools in the following slides.
Static Analysis and Verification of Drivers [WinHEC 2007; 13.4 MB]
Static Analysis Tools: PREfast for Drivers [WinHEC 2007; 1.2 MB]
Prefast is actually integrated into the Team Suite edition of Visual Studio. The other separate tool, the Static Driver Verifier, includes a graphical user interface shown below, that only a mother could love. I am still trying to figure out what is going on in the trace tree pane.
The truth is: It’s not the looks that matter, but the brains. So, I continued checking out the site for evidence of intelligence.
The site contains copious links on the history and progress of static analysis technology within Microsoft. Most of the history is detailed in one document describing the technology transfer of formal methods inside Microsoft (with SLAM and Static Driver Verifiers). SLAM project originated in Microsoft Research in 2000. Microsoft also created the Programmer Productivity Research Center in 1999 with the acquisition of Intrinsa and its PREfix defect detection tool. The paper notes that twelve percent of the bugs fixed before Windows 2003 Server were found with PREfix technology, so it does seem effective.
According to Bill Gates in his OOPSLA 2002 speech, Intrinsa was purchased for 60 million](http://www.theregister.co.uk/2005/06/29/coverity_analyses_freebsd_for_flaws/).
We’ve created a number of things to do rich static analysis. We actually went out and bought for a little over $30 million a company that was in the business of building those kinds of tools, and we said now we want you to focus on applying these tools to large-scale software systems, the kind of system we have in the source code of Windows or Office, and see how far we can get on this.
What’s the likelihood that I will see that kind of money for better technology? Maybe, the price was also for the staffing of the newly built research centers.
Gates continues his speech, going on about the intractability of static analysis and how so many decades have gone by since he dropped out of school without the problem being solved. He exhibits the typical blind spot in the field—or perhaps is just parroting the words of his researchers, ignoring that the theoretical limits of software are only those limits of humans as well. 640K anyone?
We also went back and say, OK, what is the state-of-the-art in terms of being able to prove programs, prove that a program behaves in a certain way? This is the kind of problem that has been out there for many decades. When I dropped out of Harvard, this was an interesting problem that was being worked on, and actually at the time I thought, well, if I go and start a company it will be too bad, I’ll miss some of the big breakthroughs in proving software programs because I’ll be off writing payroll checks. And it turns out I didn’t miss all that much in terms of rapid progress — (laughter) — which now has become, I’d say, in a sense, a very urgent problem. And although a full general solution to that is in some ways unachievable, for many very interesting properties this ideas of proof has come a long ways in helping us quite substantially just in the last year.
In his WinHec 2002 keynote address, Bill Gates even called software verification the Holy Grail:
“Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas, for example, driver verification we’re building tools that can do actual proof about the software and how it works in order to guarantee the reliability.”
Isn’t that funny; Me, moi, I’m working on the Holy Grail! I didn’t know that. With all the resources, cash, and people, Microsoft basically gives up on the general solution. On the other hand, I get to step up to the plate and grab the lovely green pile of money on the table.
