CAREER: Effective Methods for Finding Software Errors

职业：查找软件错误的有效方法

• 批准号: 0238570
• 负责人: Dawson Engler
• 金额: $ 40万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2003
• 资助国家: 美国
• 起止时间: 2003-04-01 至 2010-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0238570&HistoricalAwards=false
• 关键词: CAREER; Effective; Methods; Finding; Software

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.

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