Model Checking Software Binaries
There is an urgent need for better tools and services to detect security vulnerabilities in software. The potential market includes software consumers as well as producers. Producers need to harden products during development and QA—for competitive advantage, and to reduce costs (in dollars and reputation) of repeated security patches during deployment. Consumers need better assurance that the COTS products they use (often in secure and critical information systems) are trustworthy—to reduce costs and risks from vulnerable software.
Under this Homeland Security Advanced Research Projects contract, GrammaTech is developing a software analysis tool that will enable third parties to examine software packages for security weaknesses. The tool will use model-checking techniques to verify security properties of software binaries. The feasibility of software model checking (for a large class of queries, and on large programs) has been demonstrated on source code, but there are many advantages to performing such an analysis on binary code. In particular, the binary code is more complete (because libraries have been linked in, or are otherwise available) and more accurately reflects what the program will do (because compiler-specific artifacts are visible).
GrammaTech will subcontract portions of the effort to its research partners, the University of Wisconsin and Symantec Corporation. This contract was awarded by the DHS Science and Technology (S&T) Directorate.