Mathematically Rigorous Methods for Determining Software Quality

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 CodeSonarGrammaTech"s 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.