SBIR Phase I: Application of Advanced Environment Analysis for Secure, Scalable Software Development

该小型企业创新研究第一阶段研究项目支持将软件验证框架调整为C编程语言所需的研究和工程，以便在产品发布之前消除基于软件的应用程序的所有潜在安全缺陷。到目前为止，一些研究和工程挑战阻碍了行业的采用，包括：时间上，复杂系统的验证往往需要几天、几周或几个月的时间；误报频繁，当前技术报告的“缺陷”实际上是完全有效的代码；用户交互；现有的验证器，如ACL2，需要非常高级的专业知识，而不适合主流程序员。已经针对特定问题开发了许多技术的集成，但这些技术通常固定到特定的编程范例或功能集；将这些技术集成到单个验证器中仍然是一个挑战。近十年来，几个大型研究小组一直在追求可伸缩、精确的软件验证这一难以实现的目标。软件验证被称为“圣杯”，因为它承诺结束错误、安全缺陷和补丁。然而，尽管在这方面花费了数千万美元，但精确的、可扩展的软件验证尚未实现。目前的软件验证工具在标准硬件上笨重且速度慢得令人望而却步，而且太不准确，不能被认为是商业使用的可行选择。在验证的上下文中，不准确意味着该工具将太多完全合法的代码行标记为潜在的缺陷：让程序员感到沮丧，浪费生产力。这项研究将使对真实的商业代码库进行自动、安全的软件验证成为可能。

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.