Static Analysis for High Assurance and Security

Presented as part of the 2007 HCSS conference.

Abstract

In this talk we will present a static analysis technology called Abstract Interpretation that enables computing an envelope of all possible executions in a program. Using this technology, it is possible to conduct formal proofs of critical properties of an application on the source code itself, with little or no need for annotation and in a fully automated way. Applications of Abstract Interpretation, including buffer overflow analysis, malware detection, shared variables and semaphores analysis, will be discussed. However, the engineering of this technology is complex and requires a significant effort of specialization for a particular software architecture and property. We will discuss our experience in engineering high-performance static analyzers at NASA and our current approach to the design of sleek, lightweight static analysis tools, using our CodeHawk Technology.