ITR: Software Design Rules

Stanford University, Stanford CA

Investigators

Abstract

ABSTRACT 0326227 Monica Lam Stanford U Software reliability is one of the most important problems in computer science. A single operating system error can crash a machine. A single security hole can compromise the integrity of an entire system or, as software and its errors is replicated, the integrity of entire networks. This proposal focuses on practical techniques to prevent such software errors. Its approach is based on the insight that software is governed by 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 as loop invariants, pre-conditions and post-conditions that pertain to particular lines of code, design rules are more powerful, succinct, and are applicable to large amounts of code in the program. While design rules are pervasive, in practice they are neither well documented nor automatically enforced, yet programmers need to 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 be explicitly 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 how software is governed by design rules, what these rules are, and how they can be used in practice. The intent 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 of lines of code. Expecting programmers to reliably specify all rules is unrealistic. Depending on them to do so is dangerous since an omitted rule will not be checked. This research will develop techniques to automatically extract design rules from code. It uses the fact that the same rule is obeyed many times in a program, allowing it to be inferred by observing regularities in the program's static and dynamic behavior. The challenge in the approach is inferring subtle patterns from noisy behavior. This research will develop a general theory of design rule extraction. 3. Programming tools for design rules. This research will develop practical tools that automatically extract design 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 for detecting both security and non-deterministic errors (such as race conditions). 4. Fundamental static program analysis. Design-rule conformance testing requires sophisticated program analysis. This research is expected to advance the state of the art in program analyses of contextsensitive pointer aliases and object invariants. 5. Software model checking of design rules. Some rules require deeper analysis than static analysis can provide. This research will support such rules by developing a software model checker that checks actual implementation code (rather than an abstracted specification of it) against programmer-supplied invariants or other implementations. 6. Testing based on design rules. This research intends to improve testing by leveraging expressed and extracted design rules to guide test coverage, test selection and test generation.