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:

Machines and software code must be architected with the amenability of formal analysis in mind.
Formal verification techniques must be scaled up sufficiently, so that they can bring substantial automation to the analysis of software programs running on realistic machine architectures.

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.

Analysis of simple properties is routine and automatic.
The tool suite is easily extendible by the human with program specific insights (e.g., assertions, algorithm-level invariants, etc.) to discharge more subtle and deeper properties.
The tool suite takes into account features of realistic machine architectures (e.g., page tables, translation look-aside buffers, page protections, etc.).
There is clear correspondence between the formal model used for reasoning and the machine architecture and software that is the target of analysis. In particular, machine and language features not modeled in the formalization are explicit.
The tool suite itself is independent of the nuances of a specific machine architecture, but can be instantiated with a broad range of architectural features. Thus, as machine architectures evolve to satisfy both the security and usability demands of modern applications, our tool suite can be easily extended and configured to target such systems.

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

S. Ray, W. A. Hunt, Jr., J. Matthews, and J S. Moore. A Mechanical Analysis of Program Verification Strategies. Journal of Automated Reasoning, volume 40(4), May 2008, pages 245-269. Springer.

W. A. Hunt, Jr., R. B. Krug, S. Ray, and W. D. Young. Mechanized Information Flow Analysis through Inductive Assertions. In A. Cimatti and R. B. Jones, editors, Proceedings of the 8th International Conference on Formal Methods in Computer-aided Design (FMCAD 2008), Portland, OR, November 2008, pages 227-230. IEEE Computer Society.

S. Ray. A Generalized Solution for the While Challenge. Rump Session Presentation. In R. Gamboa, J. Sawada, and J. Cowles, editors, Proceedings of the 7th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2007), Austin, TX, November 2007, pages 83-84.

J. Matthews, J S. Moore, S. Ray, and D. Vroon. Verification Condition Generation via Theorem Proving. In M. Hermann and A. Voronkov, editors, Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), Phnom Penh, Cambodia, November 2006, volume 4246 of LNCS, pages 362-376. Springer.

^[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.