CAREER: Effective Methods for Finding Software Errors

软件可靠性是计算机科学中最重要的问题之一。一个操作系统错误就能使机器崩溃。一个安全漏洞就可以危及整个系统的完整性，或者当软件及其错误被复制时，危及整个网络的完整性。本研究的重点是实用的技术，以有效地发现大量的此类软件错误。最初的结果是有希望的：该方法已经在Linux操作系统以及大型商业系统中发现了数百个安全漏洞和数千个严重的错误。研究的重点是使用静态分析来查找源代码中的错误。它使用两种主要技术：(1)元编译（MC）来检查正确性规则（例如“对lock（）函数的调用必须与对unlock（）的调用配对”）和(2)信念分析来自动推断这些规则。元编译使用程序员编写的、特定于系统的静态检查器来查找软件错误。因为这些扩展可以由系统实现者自己编写，所以它们可以考虑系统的特殊（有时是奇怪的）语义。因为它们是基于编译器的，所以它们也获得了自动静态分析的好处。信念分析：在现实系统中发现程序错误的一个主要障碍是知道系统必须遵守哪些正确性规则。这些规则通常没有文档记录，或者以特别的方式指定。信念分析自动地从源代码本身推断出这种检查信息，而不是从程序员那里，从而避免了对系统规则先验知识的需要。它的工作原理是通过分析源代码来推断程序员相信什么是正确的，并检查这些信念是否矛盾。例如，如果对“lock（）”的调用与对“unlock（）”的调用配对了1000次，而没有配对一次，这很好地表明代码认为这些调用必须配对，并且单个偏差是错误的。这项研究还将涉及教育方面的内容。最重要的特点将是让本科生大量参与研究。根据经验，这样做可以帮助他们创造性地、独立地思考，并推动他们比典型的课程深入得多。

Software reliability is one of the most important problems in computerscience. A single operating system error can crash the machine. A singlesecurity hole can compromise the integrity of the entire system or, assoftware and its errors is replicated, the integrity of entire networks.This research focuses on practical techniques to effectively find largenumbers of such software errors. Initial results are promising: theapproach has found hundreds of security holes and thousands of seriouserrors in the Linux operating system, as well as in large commercialsystems.The research centers on using static analysis to find errors in sourcecode. It uses two main techniques: (1) metacompilation (MC) to checkcorrectness rules (such as ``a call to the lock() function must be pairedwith a call to unlock()'') and (2) belief analysis to infer such rulesautomatically.Metacompilation uses programmer-written, system-specific static checkersto find software bugs. Because these extensions can be written bysystem implementors themselves, they can take into account the ad hoc(sometimes bizarre) semantics of a system. Because they are compilerbased, they also get the benefits of automatic static analysis.Belief analysis: A major obstacle to finding program errors in a realsystem is knowing what correctness rules the system must obey. Theserules are often undocumented or specified in an ad hoc manner.Belief analysis automatically infers such checking information fromthe source code itself, rather than the programmer, thereby avoidingthe need for a priori knowledge of system rules. It works by analyzingsource code to infer what programmers believe to be true and checkingthese beliefs for contradictions. For example, if a call to ``lock()''is paired with a call to ``unlock()'' 1000 times and not paired once,this is a good indication that the code believes these calls must bepaired, and that the single deviation is an error.The research will also involve an educational component. The mostsignificant feature will be heavily involving undergraduates in research.Empirically, doing so helps them think creatively, independently, aswell as pushing them to go much deeper than a typical class.