Collaborative Research: Type Qualifiers for Software Security

协作研究：软件安全的类型限定符

• 批准号: 0430585
• 负责人: David Wagner
• 金额: --
• 依托单位: University of California-Berkeley
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2004
• 资助国家: 美国
• 起止时间: 2004-09-15 至 2009-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0430585&HistoricalAwards=false
• 关键词: Collaborative; Research; Type; Qualifiers; Software

0430585 Wagner, David Collaborative Research: Type Qualifiers for Software Security0430378 Alex Aiken 0430118 Foster, Jeffrey This research aims to develop tools and techniques to find and eliminate security vulnerabilities in software. The approach is based on static analysis, which by analyzing source code can model all possible executions of a program. The distinguishing feature of the project is to show that very large applications are free from classes of security vulnerabilities. Thus, the focus is not just in finding security holes in software, but in verifying their absence. Previous experience has shown that simple, approximate tools do not find all or even nearly all security vulnerabilities; the higher assurance given by verification is needed. The experimental goal is to apply these techniques to the Linux kernel, a security-critical application with millions of lines of code.The main technical approach being investigated is based on user-defined type qualifiers that refine the standard types of the programming language. Previous work has shown that type qualifiers are a natural and useful way to explicitly specify desired security properties that are normally only implicit in a program. In much the same way that a correctly typed program cannot have run-time type errors, having consistent type qualifiers throughout a program implies that the property expressed by those qualifiers must hold in every execution. The significance of this work is that, if successful, it will improve the understanding of how to perform sophisticated static analysis of very large programs. The broader impact will be in discovering and repairing new security vulnerabilities in widely-used software infrastructure and in verifying that some of that infrastructure is free from at least some security flaws.

0430585 Wagner，David Collaborative Research：软件安全的类型限定符0430378 Alex Aiken 0430118 Foster，Jeffrey这项研究旨在开发工具和技术来发现和消除软件中的安全漏洞。该方法基于静态分析，通过分析源代码可以对程序的所有可能执行进行建模。该项目的显著特点是显示超大型应用程序不存在安全漏洞类别。因此，重点不仅是寻找软件中的安全漏洞，而且是验证它们是否存在。以前的经验表明，简单、近似的工具无法发现所有甚至几乎所有的安全漏洞；需要通过验证提供更高的保证。实验目标是将这些技术应用于Linux内核，这是一个拥有数百万行代码的安全关键应用程序。正在研究的主要技术方法是基于用户定义的类型限定符，该限定符细化了编程语言的标准类型。以前的工作已经表明，类型限定符是显式指定所需的安全属性的一种自然而有用的方法，这些属性通常只在程序中隐含。就像类型正确的程序不会有运行时类型错误一样，在整个程序中拥有一致的类型限定符意味着由这些限定符表示的属性在每次执行中都必须保持。这项工作的意义在于，如果成功，它将提高对如何对非常大的程序执行复杂的静态分析的理解。更广泛的影响将是在广泛使用的软件基础设施中发现和修复新的安全漏洞，并核实其中一些基础设施至少没有一些安全缺陷。