Collaborative Research: Type Qualifiers for Software Security

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

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.