ITR: Software Design Rules

软件可靠性是计算机科学中最重要的问题之一。一个操作系统错误就可以使机器崩溃。一个安全漏洞可以危及整个系统的完整性，或者当软件及其错误被复制时，危及整个网络的完整性。本建议侧重于防止此类软件错误的实用技术。它的方法基于这样一种认识，即软件受许多设计规则的约束，从一般规则（程序不应超出其缓冲区）到特定于应用程序的规则（如必须在数据库中的提交事务之前调用开始事务），以及低级规则（如输入字符串到strncpy不应重叠）。与循环不变量、前置条件和后置条件等特定代码行的规范不同，设计规则更强大、简洁，并且适用于程序中的大量代码。虽然设计规则无处不在，但在实践中，它们既没有很好的文档记录，也没有自动执行，然而程序员需要理解并遵守它们才能编写正确的程序。知识价值。这项工作的目标是使设计规则成为一级对象。它们应该明确地成为程序设计的一部分，形成系统实现者智力框架的核心部分，并得到有效的技术支持。这项建议为实现这些目标提供了一个全面的办法。预计将作出以下主要贡献：软件开发中设计规则的一般理论。它将提供更深层次的理解软件是如何由设计规则控制的，这些规则是什么，以及如何在实践中使用它们。目的是把这个概念教给所有计算机科学专业的学生。自动设计规则推理。真实的系统有成千上万的设计规则，隐藏在数百万行代码中。期望程序员可靠地指定所有规则是不现实的。依赖它们这样做是危险的，因为忽略的规则将不会被检查。本研究将开发从代码中自动提取设计规则的技术。它利用了同一个规则在一个程序中被多次遵守的事实，允许通过观察程序的静态和动态行为中的规律来推断它。这种方法的挑战在于从嘈杂的行为中推断出微妙的模式。本研究将发展设计规则提取的一般理论。设计规则的编程工具。这项研究将开发实用的工具，自动提取设计规则，检查程序是否违反设计规则，并在程序中执行设计规则。虽然这项工作将支持通用软件，但它也将特别关注用于检测安全性和非确定性错误（如竞争条件）的工具。基本静态程序分析。设计规则一致性测试需要复杂的程序分析。这项研究有望推动上下文敏感指针别名和对象不变量的程序分析的最新进展。设计规则的软件模型检查。有些规则需要比静态分析更深入的分析。这项研究将通过开发一个软件模型检查器来支持这样的规则，该检查器可以根据程序员提供的不变量或其他实现来检查实际的实现代码（而不是抽象的规范）。基于设计规则的测试。本研究旨在通过利用表达和提取的设计规则来指导测试覆盖、测试选择和测试生成，从而改进测试。

ABSTRACT0326227Monica LamStanford USoftware reliability is one of the most important problems in computer science. A single operating systemerror can crash a machine. A single security hole can compromise the integrity of an entire system or, assoftware and its errors is replicated, the integrity of entire networks. This proposal focuses on practicaltechniques to prevent such software errors. Its approach is based on the insight that software is governedby many design rules, from general ones that programs should not overrun their buffers, to application specific rules such as a begin-transaction must be invoked before a commit-transaction in a database,and low-level rules, such as the input strings to strncpy should not overlap. Unlike specifications such asloop invariants, pre-conditions and post-conditions that pertain to particular lines of code, design rules aremore powerful, succinct, and are applicable to large amounts of code in the program. While design rules arepervasive, in practice they are neither well documented nor automatically enforced, yet programmers needto understand and obey them to write correct programs.Intellectual Merit. The goal of this work is to make design rules first-class objects. They should beexplicitly part of program design, form a core part of the intellectual framework of system implementors, and be effectively supported by techniques that have teeth. This proposal provides a comprehensive approach to reach these goals. It is expected to make the following major contributions:1. General theory of design rules in software development. It will provide a deeper understanding of howsoftware is governed by design rules, what these rules are, and how they can be used in practice. Theintent is to teach this concept to all computer science students.2. Automatic design rule inference. Real systems have thousands of design rules, buried in millions oflines of code. Expecting programmers to reliably specify all rules is unrealistic. Depending on them todo so is dangerous since an omitted rule will not be checked. This research will develop techniques toautomatically extract design rules from code. It uses the fact that the same rule is obeyed many timesin a program, allowing it to be inferred by observing regularities in the program's static and dynamicbehavior. The challenge in the approach is inferring subtle patterns from noisy behavior. This researchwill develop a general theory of design rule extraction.3. Programming tools for design rules. This research will develop practical tools that automatically extractdesign rules, check programs for design-rule violations, and also enforce design rules in programs.While the work will support general-purpose software, it will also pay particular attention to tools fordetecting both security and non-deterministic errors (such as race conditions).4. Fundamental static program analysis. Design-rule conformance testing requires sophisticated programanalysis. This research is expected to advance the state of the art in program analyses of contextsensitivepointer aliases and object invariants.5. Software model checking of design rules. Some rules require deeper analysis than static analysis canprovide. This research will support such rules by developing a software model checker that checksactual implementation code (rather than an abstracted specification of it) against programmer-suppliedinvariants or other implementations.6. Testing based on design rules. This research intends to improve testing by leveraging expressed andextracted design rules to guide test coverage, test selection and test generation.