Mathematically Rigorous Methods for Determining Software Quality

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.