CCured: type-safe retrofitting of legacy software

ABSTRACT

This article describes CCured, a program transformation system that adds type safety guarantees to existing C programs. CCured attempts to verify statically that memory errors cannot occur, and it inserts run-time checks where static verification is insufficient.CCured extends C's type system by separating pointer types according to their usage, and it uses a surprisingly simple type inference algorithm that is able to infer the appropriate pointer kinds for existing C programs. CCured uses physical subtyping to recognize and verify a large number of type casts at compile time. Additional type casts are verified using run-time type information. CCured uses two instrumentation schemes, one that is optimized for performance and one in which metadata is stored in a separate data structure whose shape mirrors that of the original user data. This latter scheme allows instrumented programs to invoke external functions directly on the program's data without the use of a wrapper function.We have used CCured on real-world security-critical network daemons to produce instrumented versions without memory-safety vulnerabilities, and we have found several bugs in these programs. The instrumented code is efficient enough to be used in day-to-day operations.

REFERENCES

• 1: Martín Abadi , Luca Cardelli , Benjamin Pierce , Gordon Plotkin, Dynamic typing in a statically typed language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.2, p.237-268, April 1991 [doi>10.1145/103135.103138]
• 2: Todd M. Austin , Scott E. Breach , Gurindar S. Sohi, Efficient detection of all pointer and array access errors, ACM SIGPLAN Notices, v.29 n.6, p.290-301, June 1994
• 3: Hans-Juergen Boehm , Mark Weiser, Garbage collection in an uncooperative environment, Software—Practice & Experience, v.18 n.9, p.807-820, September 1988 [doi>10.1002/spe.4380180902]
• 4: Cardelli, L., Donahue, J., Glassman, L., Jordan, M., Kalsow, B., and Nelson, G. 1989. Modula-3 report (rev.). SRC Research rep. 52. Digital Equipment Corporation Systems Research Center, Palo alto, CA.
• 5: Martin Christopher Carlisle, Olden: parallelizing programs with dynamic data structures on distributed-memory machines, Princeton University, Princeton, NJ, 1996
• 6: Robert Cartwright , Mike Fagan, Soft typing, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.278-292, June 24-28, 1991, Toronto, Ontario, Canada
• 7: CERT Coordination Center. 2003. CERT Advisory CA-2003-12: Buffer overflow in sendmail. Web site: http://www.cert.org/advisories/CA-2003-12.html.
• 8: Satish Chandra , Thomas Reps, Physical type checking for C, Proceedings of the 1999 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.66-75, September 06-06, 1999, Toulouse, France
• 9: Jeremy Condit , Matthew Harren , Scott McPeak , George C. Necula , Westley Weimer, CCured in the real world, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 10: Karl Crary , Stephanie Weirich , Greg Morrisett, Intensional polymorphism in type-erasure semantics, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.301-312, September 26-29, 1998, Baltimore, Maryland, United States
• 11: Manuvir Das, Unification-based pointer analysis with directional assignments, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.35-46, June 18-21, 2000, Vancouver, British Columbia, Canada
• 12: Dominic Duggan, Dynamic typing for distributed programming in polymorphic languages, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.1, p.11-45, Jan. 1999 [doi>10.1145/314602.314604]
• 13: David Evans, Static detection of dynamic memory errors, ACM SIGPLAN Notices, v.31 n.5, p.44-53, May 1996
• 14: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 15: Hastings, R. and Joyce, B. 1991. Purify: Fast detection of memory leaks and access errors. In Proceedings of the Usenix Winter 1992 Technical Conference. Usenix Association, Berkeley, CA, 125--138.
• 16: Fritz Henglein, Global tagging optimization by type inference, Proceedings of the 1992 ACM conference on LISP and functional programming, p.205-215, June 22-24, 1992, San Francisco, California, United States
• 17: Fritz Henglein , Jesper Jørgensen, Formally optimal boxing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-226, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177874]
• 18: Hirzel, M. 2000. Effectiveness of garbage collection and explicit deallocation. M.S. thesis. University of Colorado at Boulder, Boulder, CO.
• 19: ISO/IEC. 1999. ISO/IEC 9899:1999(E) Programming Languages---C. ISO/IEC, Geneva, Switzerland. Web site: www.iso.ch.
• 20: Suresh Jagannathan , Andrew K. Wright, Effective Flow Analysis for Avoiding Run-Time Checks, Proceedings of the Second International Symposium on Static Analysis, p.207-224, September 25-27, 1995
• 21: Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 22: Jones, R. W. M. and Kelly, P. H. J. 1997. Backwards-compatible bounds checking for arrays and pointers in C programs. In Proceedings of the Third International Workshop on Automatic Debugging (May). 13--26.
• 23: Kaufer, S., Lopez, R., and Pratap, S. 1988. Saber-C: An interpreter-based programming environment for the C language. In Proceedings of the Summer Usenix Conference. 161--171.
• 24: Andreas Kind , Horst Friedrich, A practical approach to type inference for EuLisp, Lisp and Symbolic Computation, v.6 n.1-2, p.159-176, Aug. 1993 [doi>10.1007/BF01025919]
• 25: Lampson, B. 1983. A description of the Cedar language. Tech. rep. CSL-83-15. Xerox Palo Alto Research Center, Palo Alto, CA.
• 26: B Liskov , E Moss , A Snyder , R Atkinson , J C. Schaffert , T Bloom , R Scheifler, CLU reference manual, Springer-Verlag New York, Inc., New York, NY, 1984
• 27: Alexey Loginov , Suan Hsi Yong , Susan Horwitz , Thomas W. Reps, Debugging via Run-Time Type Checking, Proceedings of the 4th International Conference on Fundamental Approaches to Software Engineering, p.217-232, April 02-06, 2001
• 28: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 29: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 30: Patil, H. and Fischer, C. N. 1995. Efficient run-time monitoring using shadow processing. In Proceedings of the Conference on Automated and Algorithmic Debugging. 119--132.
• 31: Harish Patil , Charles Fischer, Low-cost, concurrent checking of pointer and array accesses in C programs, Software—Practice & Experience, v.27 n.1, p.87-110, Jan. 1997 [doi>10.1002/(SICI)1097-024X(199701)27:1<87::AID-SPE78>3.0.CO;2-P]
• 32: G. Ramalingam , John Field , Frank Tip, Aggregate structure identification and its application to program analysis, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-132, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292553]
• 33: Didier Rémy , Jérôme Vouillon, Objective ML: a simple object-oriented extension of ML, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.40-53, January 15-17, 1997, Paris, France [doi>10.1145/263699.263707]
• 34: SecuriTeam.com. 2000. PHP3/PHP4 format string vulnerability. Web site: http://www.securiteam.com/securitynews/6O00T0K03O.html.
• 35: Seward, J. 2003. Valgrind, an open-source memory debugger for x86-GNU/Linux. Tech. rep. Available online at http://developer.kde.org/sewardj/.
• 36: Mark Shields , Tim Sheard , Simon Peyton Jones, Dynamic typing as staged type inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.289-302, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268970]
• 37: Michael Siff , Satish Chandra , Thomas Ball , Krishna Kunchithapadam , Thomas Reps, Coping with type casts in C, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.180-198, September 06-10, 1999, Toulouse, France
• 38: Geoffrey Smith , Dennis Volpano, A sound polymorphic type system for a dialect of C, Science of Computer Programming, v.32 n.1-3, p.49-72, Sept. 1998 [doi>10.1016/S0167-6423(97)00030-0]
• 39: SPEC. 1995. Standard Performance Evaluation Corporation Benchmarks. Web site: http://www.spec.org/osg/cpu95/CINT95.
• 40: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 41: Joseph L. Steffen, Adding run-time checking to the portable C compiler, Software—Practice & Experience, v.22 n.4, p.305-316, April 1992 [doi>10.1002/spe.4380220403]
• 42: Satish Thatte, Quasi-static typing, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.367-381, December 1989, San Francisco, California, United States [doi>10.1145/96709.96747]
• 43: Wagner, D., Foster, J., Brewer, E., and Aiken, A. 2000. A first step toward automated detection of buffer overrun vulnerabilities. In Proceedings of the Network Distributed Systems Security Symposium. 1--15.
• 44: Andrew K. Wright , Robert Cartwright, A practical soft type system for scheme, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.1, p.87-152, Jan. 1997 [doi>10.1145/239912.239917]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
      D.2.7 Distribution, Maintenance, and Enhancement
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Keywords:
Memory safety, libraries, pointer qualifier, subtyping