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

SBIR 第一阶段：应用高级环境分析进行安全、可扩展的软件开发

• 批准号: 0638060
• 负责人: Matthew Might
• 金额: --
• 依托单位: Diagis Systems, Inc.
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-01-01 至 2007-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0638060&HistoricalAwards=false
• 关键词: SBIR; Phase; Application; Advanced; Environment

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.

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