Collaborative Research: Type Qualifiers for Software Security

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

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.