Brian Demsky
Michael D. Ernst
ABSTRACT
Corrupt data structures are an important cause of unacceptable program execution. Data structure repair (which eliminates inconsistencies by updating corrupt data structures to conform to consistency constraints) promises to enable many programs to continue to execute acceptably in the face of otherwise fatal data structure corruption errors. A key issue is obtaining an accurate and comprehensive data structure consistency specification. We present 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. 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. We have implemented this approach and applied it to three sizable benchmark programs: CTAS (an air-traffic control system), BIND (a widely-used Internet name server) and Freeciv (an interactive game). Our results indicate that (1) automatic constraint generation produces constraints that enable programs to execute successfully through data structure consistency errors, (2) compared to manual specification, automatic generation can produce more comprehensive sets of constraints that cover a larger range of data structure consistency properties, and (3) reviewing the properties is relatively straightforward and requires substantially less programmer effort than manual generation, primarily because it reduces the need to examine the program text to understand its operation and extract the relevant consistency constraints. Moreover, when evaluated by a hostile third party "Red Team" contracted to evaluate the effectiveness of the technique, our data structure inference and enforcement tools successfully prevented several otherwise fatal attacks.
- C. Boyapati, S. Khurshid, and D. Marinov. Korat: automated testing based on Java predicates. In Proceedings of the 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis, 2002.]] Google Scholar
Digital Library
- G. Candea and A. Fox. Recursive restartability: Turning the reboot sledgehammer into a scalpel. In HotOS-VIII, pages 110--115, May 2001.]] Google ScholarDigital Library
- S. Ceri, P. Fraternali, S. Paraboschi, and L. Tanca. Automatic generation of production rules for integrity maintenance. ACM Transactions on Database Systems, 19(3), September 1994.]] Google ScholarDigital Library
- S. Ceri and J. Widom. Deriving production rules for constraint maintenance. In Very Large Data Bases, pages 566--577, 1990.]] Google ScholarDigital Library
- J. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridharan. Efficient and precise datarace detection for multithreaded object-oriented programs. In Proceedings of the SIGPLAN '02 Conference on Programming Languages Design and Implementation, 2002.]] Google ScholarDigital Library
- J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proceedings of the 22nd International Conference on Software Engineering, 2000.]] Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238--252, Los Angeles, CA, 1977.]] Google ScholarDigital Library
- Center-TRACON automation system. http://www.ctas.arc.nasa.gov/.]]Google Scholar
- D. Litman and A. Mishra and P. Patel-Schneider. Modeling dynamic collections of interdependent objects using path-based rules. In Proceedings of the 12th Annual Conference on Object-Oriented Programming Systems, Languages and Applications, October 1997.]] Google ScholarDigital Library
- M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In Proceedings of the SIGPLAN '02 Conference on Programming Languages Design and Implementation, 2002.]] Google ScholarDigital Library
- B. Demsky, C. Cadar, D. Roy, and M. Rinard. Efficient specification-assisted error localization. In Proceedings of the Second International Workshop on Dynamic Analysis, May 2004.]]Google ScholarCross Ref
- B. Demsky and M. Rinard. Automatic detection and repair of errors in data structures. In Annual Conference on Object-Oriented Programming Systems, Languages and Applications, October 2003.]] Google ScholarDigital Library
- B. Demsky and M. Rinard. Data structure repair using goal-directed reasoning. In Proceedings of the 27th International Conference on Software Engineering, 2005.]] Google ScholarDigital Library
- N. Dor, M. Rodeh, and M. Sagiv. CSSV: Towards a realistic tool for statically detecting all buffer overflows in C. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI), 2003.]] Google ScholarDigital Library
- M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering, 27(2):99--123, Feb. 2001. A previous version appeared in ICSE '99, Proceedings of the 21st International Conference on Software Engineering, pages 213--224, Los Angeles, CA, USA, May 19-21, 1999.]] Google ScholarDigital Library
- M. D. Ernst, A. Czeisler, W. G. Griswold, and D. Notkin. Quickly detecting relevant program invariants. In ICSE 2000, Proceedings of the 22nd International Conference on Software Engineering, pages 449--458, Limerick, Ireland, June 7-9, 2000.]] Google ScholarDigital Library
- J. Gray and A. Reuter. Transaction Processing: Concepts and Techniques. Morgan Kaufmann, 1993.]] Google ScholarDigital Library
- T. Griffin, H. Trickey, and C. Tuckey. Generating update constraints from PRL5.0 specifications. Preliminary report presented at AT&T Database Day, Sept. 1992.]]Google Scholar
- P. J. Guo. Fjalar: A dynamic analysis framework for C and C++ programs. http://pag.csail.mit.edu/fjalar/.]]Google Scholar
- P. J. Guo, J. H. Perkins, S. McCamant, and M. D. Ernst. Dynamic inference of abstract types. In ISSTA 2006, Proceedings of the 2006 International Symposium on Software Testing and Analysis, Portland, ME, USA, July 18-20, 2006.]] Google ScholarDigital Library
- N. Gupta, L. Jagadeesan, E. Koutsofios, and D. Weiss. Auditdraw: Generating audits the FAST way. In Proceedings of the 19th International Conference on Software Engineering, 1997.]]Google ScholarCross Ref
- S. Hallem, B. Chelf, Y. Xie, and D. Engler. A system and language for building system-specific, static analyses. In Proceedings of the SIGPLAN '02 Conference on Programming Languages Design and Implementation, 2002.]] Google ScholarDigital Library
- G. Haugk, F. Lax, R. Royer, and J. Williams. The 5ESS(TM) switching system: Maintenance capabilities. AT&T Technical Journal, 64(6 part 2):1385--1416, July-August 1985.]]Google Scholar
- R. Hoover. Incremental computation as a programming abstraction. In Proceedings of the SIGPLAN '92 Conference on Programming Languages Design and Implementation, 1992.]] Google ScholarDigital Library
- M. K. Johnson. Whitepaper: Red Hat's new journaling file system: ext3. http://www.redhat.com/support/wpapers/redhat/ext3/index.html, 2001.]]Google Scholar
- V. Kuncak, H. H. Nguyen, and M. Rinard. An algorithm for deciding BAPA: Boolean Algebra with Presburger Arithmetic. In 20th International Conference on Automated Deduction, CADE-20, Tallinn, Estonia, July 2005.]] Google ScholarDigital Library
- D. A. Ladd and J. C. Ramming. Two application languages in software production. In Proceedings of the 1994 USENIX Symposium on Very High Level Language, October 1994.]] Google ScholarDigital Library
- G. Lopez. The Design and Implementation of Kaleidoscope, A Constraint Imperative Programming Language. PhD thesis, University of Washington, April 1997.]] Google ScholarDigital Library
- A. Mishra, J. Ros, A. Singhal, G. Weiss, D. Litman, P. Patel-Schneider, D. Dvorak, and J. Crawford. R++: Using rules in object-oriented designs. In Proceedings of the 11th Annual Conference on Object-Oriented Programming Systems, Languages and Applications, July 1996.]]Google Scholar
- S. Mourad and D. Andrews. On the reliability of the IBM MVS/XA operating system. Transactions on Software Engineering, September 1987.]] Google ScholarDigital Library
- D. A. Patterson, A. Brown, P. Broadwell, G. Candea, M. Chen, J. Cutler, P. Enriquez, A. Fox, E. Kiciman, M. Merzbacher, D. Oppenheimer, N. Sastry, W. Tetzlaff, J. Traupman, and N. Treuhaft. Recovery-oriented computing (ROC): Motivation, definition, techniques, and case studies. Technical Report UCB//CSD-02-1175, UC Berkeley Computer Science, March 15, 2002.]] Google ScholarDigital Library
- M. Rinard, C. Cadar, D. Dumitran, D.M. Roy, T. Leu, and J. William S. Beebee. Enhancing server availability and security through failure-oblivious computing. In Proceedings of the 6th Symposium on Operating Systems Design and Implementation, 2004.]] Google ScholarDigital Library
- M. Rosenblum and J. Ousterhout. The design and implementation of a log-structured file system. In Symposium on Operating Systems Principles, Oct. 1991.]] Google ScholarDigital Library
- S. D. Urban and L. M. Delcambre. Constraint analysis: A design process for specifying operations on objects. IEEE Transactions on Knowledge and Data Engineering, 2(4), December 1990.]] Google ScholarDigital Library
- D. Wagner, J. S. Foster, E. A. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Proceedings of the Year 2000 Network and Distributed System Security Symposium, 2000.]]Google Scholar
- Y. M. Wang, Y. Huang, K. P. Vo, P. Y. Chung, and C. Kintala. Checkpointing and its applications. In Proceedings of the 25th Fault-Tolerant Computing Symposium, 2005.]] Google ScholarDigital Library
- T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard. Field constraint analysis. In Proc. Int. Conf. Verification, Model Checking, and Abstract Interpratation, 2006.]] Google ScholarDigital Library
Index Terms
- Inference and enforcement of data structure consistency specifications
Recommendations
Data structure repair using goal-directed reasoning
ICSE '05: Proceedings of the 27th international conference on Software engineeringData structure repair is a promising technique for enabling programs to execute successfully in the presence of otherwise fatal data structure corruption errors. Previous research in this field relied on the developer to write a specification to ...
Automatic detection and repair of errors in data structures
Special Issue: Proceedings of the OOPSLA '03 conferenceWe present a system that accepts a specification of key data structure consistency constraints, then dynamically detects and repairs violations of these constraints, enabling the program to continue to execute productively even in the face of otherwise ...
Contract-based data structure repair using alloy
ECOOP'10: Proceedings of the 24th European conference on Object-oriented programmingContracts and specifications have long been used in object-oriented design, programming and testing to enhance reliability before software deployment. However, the use of specifications in deployed software is commonly limited to runtime checking where ...
Comments