Collaborative Research: Type Qualifiers for Software Security

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

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

0430118 PI Foster, Jeffrey Collaborative Research: Type Qualifiers for Software Security0430585 Wagner, David 0430378 Alex AikenThis 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.

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