This Small Business Innovation Research Phase I research project supports the research and engineering required to adapt a software verification framework to the C programming language that enables the removal of all potential security flaws from software-based applications before product release. Several research and engineering challenges have prevented industry adoption so far, including: Time Often, verification of a complex system takes days, weeks or months; False Positives Frequently, current techniques report 'flaws' which are, in fact, perfectly valid code; User Interaction Existing verifiers, such as ACL2, require highly advanced expert knowledge not suitable for mainstream programmers. The integration of many techniques have been developed for specific problems, but these techniques are often fixed to a specific programming paradigm or feature set; integrating these techniques into a single verifier remains a challenge.
Several large research groups have been chasing the elusive goal of scalable, precise software verification for nearly a decade. Software verification is has been called the "Holy Grail," because it promises an end to bugs, to security flaws and to patching. However, despite tens of millions spent in the quest, precise, scalable software verification has not been achieved. Current software verification tools are cumbersome and prohibitively slow on standard hardware and too inaccurate to be considered a viable option for commercial use. Inaccuracy, in the context of verification, means that the tool flags too many perfectly legitimate lines of code as potentially flawed: frustrating programmers and wasting productivity. This research will make automatic, secure software verification possible for real, commercial code bases.
