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
- 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.
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
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.
Here are the people who have been involved in this research so far in
We're looking for more help, so if you're interested in the work feel
free to talk to us.
- 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
- 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