Mathematically Rigorous Methods for Determining Software Quality Navy STTR FY2010.A Sol No.: Navy STTR FY2010.A Topic No.: N10A-T035 Topic Title: Mathematically Rigorous Methods for Determining Software Quality Proposal No.: N10A-035-0544 Firm: GrammaTech, Inc 317 N. Aurora Street Ithaca, New York 14850 Contact: Denis Gopan Phone: (608) 827-0657 Web Site: www.grammatech.com Abstract: Software is rarely written entirely from scratch. Typically, third-party commercial off-the-shelf (COTS) components are integrated into larger software systems used both in the commercial sector and in critical infrastructure. Third-party components often come in binary form, e.g., as dynamically linked libraries, Active X controls, or plain executables. That is, the source code for those components is typically unavailable and the debug information is stripped. Additionally, to hamper reverse-engineering attempts, the binaries of those components are often further protected with anti-tamper techniques and obfuscations. The lack of source code for third-party components prevents most existing security-analysis tools from exposing the vulnerabilities and malicious behaviors harbored by those components themselves, as well as by software systems that integrate those components. We propose to design and build a tool that will conduct rigorous analysis of machine code to assess its quality. The tool will automatically identify vulnerabilities in third-party components and will assist security analysts in spotting unexpected and potentially malicious behavior in the third-party code. The proposed tool will integrate with existing GrammaTech source-code-analysis tools to boost their effectiveness in dealing with third-party components and libraries. Benefits: The growing role of software in critical systems makes software reliability and security increasingly important. Yet the typical software application is more complex than ever, making it exceedingly difficult to validate. Over the last few years, automated analysis tools have emerged that have positively impacted software assurance. However, nearly all of these tools examine source code and therefore cannot be used to examine applications or components for which the source code is unavailable. There is a need for new technology that examines binaries directly to assess quality and security. The research proposed herein will result in a program-analysis engine that performs an analysis on binaries to assist in assessing the quality and security of a program. It will verify applications or components (when binary size permits) and serve as a plug-in into a lighter-weight heuristics-based analysis to improve the overall precision of the analysis (when binary size prohibits whole-program verification). The analysis engine will be commercialized by being integrated into GrammaTech's commercial static-analysis tool for C/C++, CodeSonarr, which has a substantial established customer base. This streamlined commercialization path will put the technology in the hands of end users very quickly. Return