Microsoft devises bug-free software development system

Microsoft researchers say they have taken the first steps towards building software that can be proven to be free of bugs, a feat that has eluded programmers for decades.

Project IronFleet researchers Chris Hawblitzel, Brian Zill, Jon Howell, Michael Roberts, Bryan Parno, Manos Kapritsos, Jay Lorch and Srinath Setty. Source: Microsoft.

Known as Project IronFleet, the Microsoft research team claim to have worked out a methodology to build correct or bug-free distributed software systems, and to verify they don't harbour subtle imperfections.

Bugs in software systems that span multiple machines occur as developers have to think of all the complex ways in which the devices interact.

While the researchers caution that they are still a long way from building large-scale computer programs, such as operating systems that are guaranteed to be bug-free, smaller software can be mathematically proven to not have imperfections that make it freeze up or fall vulnerable to security flaws.

Blending Typed Assembly Language (TAL) and Hoare logic [pdf] the researchers were able to use recent advances such as cloud servers and improved algorithms to run verification tools much faster than previously possible.

Only ten years ago, running the verification tools on the software system might have taken an entire lifetime; now, the improved algorithms have shortened this period to six hours on a single computer, or just six to eight minutes using cloud-based servers, the researchers said.

Similar verification techniques were used by Microsoft researchers Jean Yang and Chris Hawblitzel to create the Verve small-scale bug-free operating system in 2010. 

The researchers said IronFleet is a departure from the more common approach of testing software rigorously for bugs before it is released, or reacting to any bugs that crop up after the software has been made public. 

Australia's peak science and research organisations NICTA has been at the forefront of developing software can be mathematically proven to be correct since the mid-2000s.

NICTA developed the Secure Embedded L4 (seL4) micro-kernel based operating system for medical, automotive, aerospace and intelligence agency applications, and released the first version for testing in 2009.

SeL4 was released as open source last year, and NICTA has partnered with United States military technology maker General Dynamics, which is considering using the secure operating system in its unmanned aerial vehicles