Related research papers:

• M. Bishop and M. Dilger, Checking for Race Conditions in File Accesses, Computing Systems 9(2) pp. 131-152 (Spring 1996). David Wagner reports that this is a common type of security flaw that is well-suited to static analysis.
• W. R. Bush, J. D. Pincus and D. J. Sielaff. A static analyzer for finding dynamic programming errors. In Software Practice and Experience, 2000; 30 : 775-802. This is the most recent paper on the PREfix tool. Abstract: There are important classes of programming errors that are hard to diagnose, both manually and automatically, because they involve a program's dynamic behavior. This article describes a compile-time analyzer that detects these dynamic errors in large, real-world programs. The analyzer traces execution paths through the source code, modeling memory and reporting inconsistencies. In addition to avoiding false paths through the program, this approach provides valuable contextual information to the programmer who needs to understand and repair the defects. Automatically-created models, abstracting the behavior of individual functions, allow inter-procedural defects to be detected efficiently. A product built on these techniques has been used effectively on several large commerical programs.
• Thomas Colcombet, Pascal Fradet, Enforcing Trace Properties by Program Transformation, In Conference record of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2000. They propose an automatic method to enforce trace properties on programs. The programmer specifies the property separately from the program; a program transformer takes the program and the property and automatically produces another ``equivalent'' program satisfying the property. This separation of concerns makes the program easier to develop and maintain. The approach is both static and dynamic. It integrates static analyses in order to avoid useless transformations. On the other hand, it never rejects programs but adds dynamic checks when necessary. The most obvious application domain is the enforcement of security policies. Also available in US letter size.
• D. A. Cyrluk, M. K. Sirvas, Theorem Proving: Not an Esoteric Diversion, but the Unifying Framework for Industrial Verification, in IEEE ICCD '95. Abstract: The effectiveness of hardware verification techniques has increased markedly in the past decade. As hardware verification techniques become increasingly powerful the idea of transitioning verification technology to industry can be taken seriously. Nevertheless, powerful decision procedures that can completely automate the verification of certain types of hardware, whether they are BDD based model-checkers [10] or automatic microprocessor verification tools [4], cannot be adequate on their own for industrial hardware verification. However, a high-level, general-purpose theorem prover with specific capabilities can provide an overall framework in which these tools can be embedded and in which they can then be effectively used for industrial hardware verification.
• D. Detlefs, K. R. M. Leino, G. Nelson, and J. Saxe, Extended Static Checking, Compaq SRC Research Report 159, December 1998. The report describes the ESC/Module-3 project. Among other things, it uses abstract variables in public interfaces and representation invariants in private implementations. It contains two examples of such specifications and a "hard specification problem" that leads to their generalization of previously know solutions to data abstraction.
• Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem, Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions, This paper will appear in OSDI 2000. It discusses a set of small extensions that found roughly 500 bugs in Linux, OpenBSD, and the Xok exokernel. The extensions were usually less than 100 lines. It also used extensions to find hundreds of optimization opportunities in heavily-tuned cache coherence software (e.g., places where message buffers could be freed sooner for greater parallelism). Andy Chou has also commented on the performance of the system:

  Usually we observe a 10%-100% overhead compared with running g++ without MC enabled. The speed depends on the SM and the size of the input in terms of # of AST nodes. If "per-variable state" is used then it also depends on the number of variables in the input. The metal paper talks a little more about variables that affect running time.

  We haven't observed swapping yet so we don't care too much about the memory usage. I expect that it should be approximately linear in the input size, but don't quote me on it.

• P. Fradet, D. Le Métayer. Shape types, In Proc. of Principles of Programming Languages, ACM Press, Paris, France, Jan. 1997. Abstract: Type systems currently available for imperative languages are too weak to detect a significant class of programming errors. For example, they cannot express the property that a list is doubly-linked or circular. We propose a solution to this problem based on a notion of shape types defined as context-free graph grammars. We define graphs in set-theoretic terms, and graph modifications as multiset rewrite rules. These rules can be checked statically to ensure that they preserve the structure of the graph specified by the grammar. We provide a syntax for a smooth integration of shape types in C. The programmer can still express pointer manipulations with the expected constant time execution and benefits from the additional guarantee that the property specified by the shape type is an invariant of the program. Also available in US Letter size.
• Daniel Jackson, Aspect: An Economical Bug-Detector, IEEE 1991: CH2982-7. Abstract: A technique for catching code-level bugs is presented. Programmers write simple assertions about the information required to compute a result; an efficient mechanical checker can then find bugs in the annotated code. Careless slips that escape type-checking and standard compiler anomaly tests can be detected, without the cost of formal verification or the uncertainty of testing.
• T. Jensen, D. Le Métayer, T. Thorn, Verification of control flow based security policies , IRISA, technical report, number 1210, 1998. Abstract: A fundamental problem in software-based security is whether local security checks inserted into the code are sufficient to implement a given global security policy. We introduce a formalism based on a two-level linear-time temporal logic for specifying global security policies pertaining to the control-flow of the program, and illustrate its expressive power with a number of existing policies. We define a minimalistic, security-dedicated program model that only contains procedure call and dynamic security checks and propose an automatic method for verifying that an implementation using local security constructs satisfies a global security policy. For a given formula in the temporal logic we prove that there exists a bound on the size of the states that have to be considered in order to assure the validity of the formula: this reduces the problem to finite-state model checking. Finally, we instantiate the framework to the security architecture proposed for Java (JDK 1.2).
• Klarlund, N. and Schwartzbach, M. Graph Types, POPL '93, pp. 196-205. Abstract: Recursive data structures are abstractions of simple records and pointers. They impose a shape invariant, which is verified at compile-time and exploited to automatically generate code for building, copying, comparing, and traversing values without loss of efficiency. However, such values are always tree shaped, which is a major obstacle to practical use. We propose a notion of graph types, which allow common shapes, such as doubly-linked lists or threaded trees, to be expressed concisely and efficiently. We define regular languages of routing expressions to specify relative addresses of extra pointers in a canonical spanning tree. An efficient algorithm for computing such addresses is developed. We employ a second-order monadic logic to decide well-formedness of graph type specifications. This logic can also be used for automated reasoning about pointer structures.
• K. R. M. Leino and R. Stata, Checking Object Invariants, Compaq SRC Technical Note 1997-007, January 1997. In the Java branch of the ESC project, object invariants are used instead of abstract variables. Some of the issues the project faced are described here.
• D. Le Métayer. Program analysis for software engineering: new applications, new requirements, new tools, ACM Sigplan Notices, number 1, pp. 86-88, January 1997. In order to play a bigger role in software engineering tools, static analysis techniques must take into account the specific needs of this application area, in particular in terms of interaction with the user and scalability. This new perspective requires a reexamination of the field of static program analysis both internally and in connection with related areas like theorem proving and debugging.
• Alexey Loginov, Suan Hsi Yong, Susan Horwitz, and Thomas Reps, Debugging via Run-Time Type Checking. This paper describes the design and implementation of a tool for C programs that provides run-time checks based on type information. The tool instruments a program to monitor the type stored in each memory location. Whenever a value is written into a location, the location's run-time type tag is updated to match the type of the value. Also, the location's static type is compared with the value's type; if there is a mismatch, a warning message is issued. Whenever the value in a location is used, its run-time type tag is checked, and if the type is inappropriate in the context in which the value is being used, an error message is issued.
• Anders Mřller and Michael I. Schwartzbach, The Pointer Assertion Logic Engine. Pointer Assertion Logic is a notation for expressing assertions about the heap structure of imperative languages. It allows programmers to specify pre- and post-conditions of procedures, loop invariants, and other assertions in Weak Monadic Second-order Logic of Graph Types - a logic that allows many common data structures to be expressed. The logic is decidable, meaning that the assertions can be verified automatically. The main target applications are safety critical data type algorithms.
• R. Stata and M. Abadi, A Type System for Java Bytecode Routines, Compaq SRC Research Report 158, June 1998. This paper describes typing rules that describe the Java bytecode verifier. The verifier runs on untrusted JVML code before the JVM interprets it.

Return to the main OSQ page.

Last modified: Sun May 18 13:38:11 PDT 2003