Posted by Allison Linn
The team of researchers working on IronFleet include, from top left, Chris Hawblitzel, Brian Zill, Jon Howell, Michael Lowell Roberts, Bryan Parno, Manos Kapritsos, Jay Lorch and Srinath Setty.
Microsoft researchers have figured out a way to build software systems spanning many computers that can be proven free of bugs, a significant feat in the decades-long quest to create perfect software.
Microsoft Research Podcast
AI Frontiers: AI for health and the future of research with Peter Lee
Peter Lee, head of Microsoft Research, and Ashley Llorens, AI scientist and engineer, discuss the future of AI research and the potential for GPT-4 as a medical copilot.
“Program verification has been a holy grail for computer science for 40 or 50 years,” said Bryan Parno (opens in new tab), a Microsoft researcher who is one of the co-authors of a forthcoming paper on the project.
The researchers caution that we are still far from a world in which large computer programs, such as complex operating systems, could realistically be built in a way that is guaranteed to be free of bugs.
But, they say, recent advances have made it possible to write smaller-scale software that can be mathematically proven not to have the type of imperfections that make a program freeze up or leave it vulnerable to a security attack.
“These tools are finally reaching the point where developers can start writing code this way,” said Jay Lorch (opens in new tab), a senior researcher who is another of the paper’s co-authors.
The Microsoft research project, called IronFleet (opens in new tab), is one of several projects showcasing advances in building bug-free systems that will be presented at the 25th ACM Symposium on Operating Systems Principles (opens in new tab), which takes place next week.
IronFleet targets systems that span several machines. These types of systems can be prone to bugs because developers have to think of all the complex ways in which the machines have to interact.
For example, a bank may have a distributed system that allows its many servers to coordinate with each other. There’s no room for error because an account holder may have a deposit request come in on one server and a withdrawal request come in on another, and the bank needs to be absolutely sure that both transactions are recorded consistently.
The researchers said that’s also the kind of system in which the security of being bug-free is important enough to justify the larger investment needed to produce this kind of provably correct code. For now, they note, it would be both impractical and cost-prohibitive to produce large-scale software such as a major operating system in this way, since that kind of system may have millions of lines of code and is generally building on past work.
“Initially we’ll be focused on small but critical pieces of software, where security and reliability are so important,” Parno said.
Lorch said the researchers also are focusing on systems that interact only with other computers because they are more predictable.
“Humans are very complicated, so trying to specify how a human interacts with a program is fairly complex,” Lorch said.
Smarter and faster tools
The ability to do this kind of work has improved recently because of better hardware and tools, including faster algorithms that have been developed at Microsoft Research (opens in new tab), said Chris Hawblitzel (opens in new tab), a researcher who also co-authored the IronFleet paper and previously created a small-scale, bug-free operating system (opens in new tab).
A decade ago, Hawblitzel said it might have taken his entire lifetime to run the verification tools needed to determine that their system was correct. Now, thanks to improved algorithms, it might take six hours on a single computer.
With a cloud-based set of servers, the system can be verified in as little as six to eight minutes.
The IronFleet system is a departure from the more common system of testing software rigorously for bugs before it is released, and also reacting to any bugs that crop up after it goes public. It follows another project from the same Microsoft research team, Ironclad (opens in new tab), which aimed to create systems guaranteed to securely handle personal data.
With these projects, the researchers say, there is the potential to up-end the software development (opens in new tab) process completely by creating systems that have been mathematically proven to be perfect to begin with.
“If we’re successful, 10 or 15 years from now people will look back and say, ‘I can’t believe they used to write code that way,'” Parno said. “It’s like doctors doing surgery without anesthetic or sterilizing equipment.”
Other Microsoft research papers being presented at the SOSP conference include:
- Parallelizing user-defined aggregations using symbolic execution (opens in new tab)
Veselin Raychev, ETH Zurich; Madanlal Musuvathi and Todd Mytkowicz, Microsoft Research - High-performance ACID via modular concurrency control (opens in new tab)
Chao Xie, Chunzhi Su, Cody Littley, and Lorenzo Alvisi, University of Texas at Austin; Manos Kapritsos, Microsoft Research; Yang Wang, Ohio State University - Software Defined Batteries (opens in new tab)
Anirudh Badam and Ranveer Chandra, Microsoft Research; Jon A. Dutra, Microsoft; Steve Hodges, Microsoft Research; Pan Hu, University of Massachusetts Amherst; Julia Meinershagen, Microsoft; Bodhi Priyantha and Thomas Moscibroda, Microsoft Research; Evangelia Skiani, Columbia University; Anthony Ferrese, Tesla Motors - No compromises: distributed transactions with consistency, availability and performance (opens in new tab)
Aleksandar Dragojevic, Dushyanth Narayanan, Ed Nightingale, Matthew Renzelmann, Alex Shamis, Anirudh Badam and Miguel Castro, Microsoft Research
Allison Linn is a senior writer at Microsoft Research. Follow Allison on Twitter (opens in new tab).
Programming languages and software engineering