SBIR-STTR Award

Mathematically Rigorous Methods for Determining Software Quality
Award last edited on: 4/2/2019

Sponsored Program
STTR
Awarding Agency
DOD : Navy
Total Award Amount
$849,509
Award Phase
2
Solicitation Topic Code
N10A-T035
Principal Investigator
Denis Gopan

Company Information

GrammaTech Inc

531 Esty Street
Ithaca, NY 14850
   (607) 273-7340
   info@grammatech.com
   www.grammatech.com

Research Institution

University of Wisconsin

Phase I

Contract Number: N00014-10-M-0251
Start Date: 6/28/2010    Completed: 7/8/2011
Phase I year
2010
Phase I Amount
$100,000
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.

Benefit:
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 GrammaTechs commercial static-analysis tool for C/C++, CodeSonar, which has a substantial established customer base. This streamlined commercialization path will put the technology in the hands of end users very quickly.

Keywords:
software verification, software verification, Machine-code analysis, Computer Security

Phase II

Contract Number: N00014-11-C-0447
Start Date: 9/15/2011    Completed: 3/15/2013
Phase II year
2011
Phase II Amount
$749,509
Modern software typically integrates a number of third-party commercial components. The indiscriminate use of such components poses significant security threats to software systems because the components may harbor unintentional vulnerabilities as well as intentionally malicious behaviors. Moreover, third-party components often come only in binary form preventing 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 them. The goal of this project is to 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 behaviors in the third-party code. Moreover, the tool will integrate with CodeSonarGrammaTechs commercially successful program-analysis tool for finding defects in softwareto increase its precision and to boost its effectiveness in dealing with third-party components and libraries. We expect that the integration will significantly reduce the number of false positives reported by CodeSonar and will allow CodeSonar to identify more bugs and vulnerabilities (and, in particular, subtler bugs and vulnerabilities) in software.

Benefit:
There is a strong need in the market for a tool that can rigorously and soundly analyze machine code, in particular, when neither source code nor debugging information is available. Increasingly, software systems integrate large numbers of commercial third-party components. Those components are typically distributed with no source code, and may be protected from reverse engineering. Thousands of new malware samples are detected daily. Malware is also only available in machine-code form, and is typically protected in order to thwart security analysis. The tool we propose will provide a sorely needed solution to the problem of security analysis of machine code. The tool will be able to find errors and security vulnerabilities in standalone executables. Moreover, the tool will integrate with CodeSonarthe GrammaTech commercially successful bug-finding tooland will boost the precision and rigor of the CodeSonar analysis. We expect that the integration will significantly reduce the number of false positives reported by CodeSonar and will allow CodeSonar to identify more bugs and vulnerabilities (and, in particular, subtler bugs and vulnerabilities) in software. CodeSonar already has an extensive customer base, which will pave the way towards the successful commercialization of the technology we that will develop in this project.

Keywords:
Vulnerability detection, Directed proof generation, Computer Security, COTS Components, Library Summarization, Rigorous program analysis, Model checking, Machine code analysis