Robust Reasoning Framework for Machine Code Verification

Background, Motivation, and Goals

With pervasive use of software artifacts in every aspect of human life, the cost of malfunctioning software today is staggering. According to a report of the US Department of Commerce's National Institute of Standards and Technology, the cost to the US economy is as high as 60 Billion dollars per year. In addition to crashes and failures in shipped software artifacts requiring significant investments to develop complicated patches in deployed systems, bugs make systems susceptible to malware, viruses, and other attacks. On the other hand, it is impossible today fully to understand or predict the behavior of large software systems, and this problem is getting worse as system complexity continues to grow.

Formal methods have shown significant promise to dramatically improve software reliability. The idea of formal methods is to model software executions in a formal, mathematical logic and use mathematical reasoning to ensure and check that the executions satisfy the desired properties and specifications. The process is well-known to catch rare, corner-case software bugs that are difficult to identify through simulation and testing, but can have catastrophic consequences in real execution, especially in the presence of adversaries actively looking for opportunities to exploit such vulnerabilities. In spite of such promise, however, the adoption of formal methods in software engineering practice has been limited. The key reason for this is that the state-of-the-art formal methods solutions available today are still too expensive for day-to-day use in large-scale software assurance. In particular, deductive or theorem proving solutions, based on human-guided, semi-automatic mechanical reasoning often involve prohibitive manual effort, while fully automatic approaches based on decision procedures (e.g., model checking) can quickly run out of available time and memory.

Ameliorating the scalability problem for future systems requires synergistic and collaborative progress in computer architecture, software design, and formal methods:

The goal of this project is to develop scalability of formal analysis tools and techniques for verification of software running on realistic machine architectures. The anticipated outcome is a comprehensive analysis tool-suite for machine-code verification, with the following characteristic features.

Funding, Personnel, and Organizations

The research has been funded in part by the Defense Advanced Research Projects Agency and the National Science Foundation under Grant CNS-0429591, and by the Defense Advanced Research Projects Agency under Grant N66001-10-2-4087.[1]

Here are the people who have been involved in this research so far in various capacities.

We're looking for more help, so if you're interested in the work feel free to talk to us.

Publications

[1] Any opinions, findings and conclusions or recomendations expressed in this material are those of the authors and do not necessarily reflect the views of the Defense Advanced Research Projects Agency or the National Science Foundation.