Research Abstracts - 2006

Automatic Inference and Enforcement of Data Structure Consistency Specifications

Brian Demsky, Michael D. Ernst, Philip J. Guo, Stephen McCamant, Jeff H. Perkins & Martin Rinard

Introduction

Corrupt data structures are a frequent cause of crashes and other unacceptable program behaviors. Data structure repair eliminates inconsistencies by updating corrupt data structures to conform to consistency constraints. Repair enables many programs to continue to execute acceptably in the face of otherwise fatal data structure corruption errors, but a key issue in the application of data structure repair is obtaining an accurate and comprehensive data structure consistency specification.

We have developed a new technique for obtaining data structure consistency specifications for data structure repair. Instead of requiring the developer to manually generate such specifications, our approach automatically generates candidate data structure consistency properties using the Daikon invariant detection tool [1]. The developer then reviews these properties, potentially rejecting or generalizing overly specific properties to obtain a specification suitable for automatic enforcement via data structure repair [2].

Approach

Our approach consists of the following phases:

• Dynamic Analysis: The developer runs the program on a range of test inputs for which the program is known to produce correct results. The Daikon dynamic analysis tool processes the test runs to produce a candidate set of data structure consistency specifications.
• Review: The generated data structure consistency specifications are satisfied in all of the sample executions, but may be overly specific to the test inputs. The developer may therefore review the generated specifications to discard or generalize any overly specific properties.
• Translation: Our tools translate the generated properties from the Daikon specification language into the repair system's data structure consistency specification language. Whereas Daikon reports properties over the concrete variables and object fields of the program, the data structure repair system works with an abstract model of the state (the abstract model simplifies the repair algorithm). Our tools seamlessly bridge this abstraction gap.
• Monitoring and Repair: Our tools augment the program with automatically generated code that implements our data structure repair algorithm. As the program runs, this code monitors its data structures for consistency property violations, repairing any violations as necessary to keep the program executing acceptably (Figure 1).

Figure 1. The repair process operates by constructing an abstract model of the program's state; repairs are first generated in the abstract, and then translated into a concrete data-structure modifications. The concrete structure is then re-abstracted, and the process repeats until a consistent structure is obtained. A static analysis guarantees that the repair process always terminates.

Experience

We have applied our technique to three sizable benchmark programs.

CTAS is a set of air-traffic control tools developed at the NASA Ames Research Center; versions of it are in daily operational use at centers around the country. We used our system to protect the flight plan data structure in CTAS, and inserted faults to mimic the effect of errors in flight plan processing of a kind found in previous CTAS versions. Without repair, CTAS fails with an addressing exception; with repair, the origin or destination airport of an affected flight is incorrect, but the rest of the system continues to operate normally.

BIND is the most widely used server for the DNS protocol which translates between names and addresses for computers on the Internet. We used our system to protect the data structures involved in two previously known denial-of-service security vulnerabilities in BIND, each of which could prevent a server from handling legitimate requests. For one vulnerability, relating to the caching of negative replies, our technique ameliorates the effect of an attack by limiting the time maliciously chosen data remains in a cache, allowing a server to return to correct operation more quickly. For a second vulnerability, relating to the validation of replies with cryptographic signatures, an attack would cause a server without repair to crash with an assertion violation. With repair, the malformed reply is rejected, and the server continues normal processing.

Freeciv is a multi-player distributed strategy game. To evaluate our technique's effectiveness in protecting the Freeciv server, we provided an outside three-person "Red Team" with complete information about Freeciv and our repair system, and they developed data structure corruptions in an attempt to crash the server. The repair system detected 80% if the data-structure corruptions introduced by the Red Team, and in 75% of those cases was able to perform a repair that allowed the server to keep running.

Research Support

This research is supported by DARPA and a National Defense Science and Engineering Graduate Fellowship.

References:

[1] Jeff H. Perkins and Michael D. Ernst. Efficient incremental algorithms for dynamic detection of likely invariants. In The Proceedings of the ACM SIGSOFT 12th Symposium on the Foundations of Software Engineering (FSE 2004), pp. 23–32, Newport Beach, California, USA, November 2004.

[2] Brian Demsky and Martin C. Rinard. Data structure repair using goal-directed reasoning. In The Proceedings of the 2005 International Conference on Software Engineering (ICSE), pp. 176–185, St. Louis, Missouri, USA, May 2005.