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.