CAREER: Effective Methods for Finding Software Errors

软件可靠性是计算机科学中最重要的问题之一。 一个操作系统错误就可能使机器崩溃。 一个安全漏洞可能危及整个系统的完整性，或者当软件及其错误被复制时，整个网络的完整性。 初步结果令人鼓舞：该方法已经在Linux操作系统以及大型商业系统中发现了数百个安全漏洞和数千个严重错误。它使用两种主要技术：（1）检查正确性规则的元编译（MC）（例如"对lock（）函数的调用必须与对unlock（）函数的调用配对“）和（2）自动推断这些规则的置信分析。 因为这些扩展可以由系统实现者自己编写，所以它们可以考虑系统的特殊（有时是奇怪的）语义。 因为它们是基于编译器的，所以它们还可以获得自动静态分析的好处。信念分析：在真实系统中发现程序错误的一个主要障碍是知道系统必须遵守什么样的正确性规则。这些规则通常是没有文档记录的或者是以特别的方式指定的。信念分析自动地从源代码本身而不是程序员那里推断出这样的检查信息，从而避免了对系统规则的先验知识的需要。 它通过分析源代码来推断程序员认为什么是正确的，并检查这些信念是否矛盾。 例如，如果对"lock（lock）“的调用与对" unlock（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.