CCured in the real world

ABSTRACT

CCured is a program transformation system that adds memory safety guarantees to C programs by verifying statically that memory errors cannot occur and by inserting run-time checks where static verification is insufficient.This paper addresses major usability issues in a previous version of CCured, in which many type casts required the use of pointers whose representation was expensive and incompatible with precompiled libraries. We have extended the CCured type inference algorithm to recognize and verify statically a large number of type casts; this goal is achieved by using physical subtyping and pointers with run-time type information to allow parametric and subtype polymorphism. In addition, we present a new instrumentation scheme that splits CCured's metadata into a separate data structure whose shape mirrors that of the original user data. This scheme allows instrumented programs to invoke external functions directly on the program's data without the use of a wrapper function.With these extensions we were able to use CCured on real-world security-critical network daemons and to produce instrumented versions without memory-safety vulnerabilities.

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: Martin Christopher Carlisle, Olden: parallelizing programs with dynamic data structures on distributed-memory machines, Princeton University, Princeton, NJ, 1996
• 4: 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
• 5: CERT Coordination Center. Cert advisory ca-2003-12: Buffer overflow in sendmail. http://www.cert.org/advisories/CA-2003-12.html, 2003.
• 6: 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
• 7: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 8: R. Hastings and B. Joyce. Purify: Fast detection of memory leaks and access errors. In Proceedings of the Usenix Winter 1992 Technical Conference, pages 125--138, Berkeley, CA, USA, Jan. 1991. Usenix Association.
• 9: 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
• 10: 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
• 11: R. W. M. Jones and P. H. J. Kelly. Backwards-compatible bounds checking for arrays and pointers in C programs. AADEBUG, 1997.
• 12: S. Kaufer, R. Lopez, and S. Pratap. Saber-C: an interpreter-based programming environment for the C language. In Proceedings of the Summer Usenix Conference, pages 161--171, 1988.
• 13: 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]
• 14: 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
• 15: 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
• 16: H. Patil and C. N. Fischer. Efficient run-time monitoring using shadow processing. In Automated and Algorithmic Debugging, pages 119--132, 1995.
• 17: 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]
• 18: 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]
• 19: SecuriTeam.com. PHP3 / PHP4 format string vulnerability.
• 20: J. Seward. Valgrind, an open-source memory debugger for x86-GNU/Linux. Technical report, http://developer.kde.org/~sewardj/, 2003.
• 21: 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]
• 22: 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
• 23: 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]
• 24: SPEC 95. Standard Performance Evaluation Corportation Benchmarks. http://www.spec.org/osg/cpu95/CINT95, July 1995.
• 25: 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]
• 26: D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step toward automated detection of buffer overrun vulnerabilities. In Network Distributed Systems Security Symposium, pages 1--15, Feb. 2000.
• 27: W. Weimer. The CCured type system and type inference. Technical Report UCB-CS, University of California, Berkeley. http://www.cs.berkeley.edu/~weimer/ TheCCuredTypeSystem.ps, 2002.
• 28: 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

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

General Terms:
Experimentation, Languages, Reliability, Security

Keywords:
C, compatibility with library code, memory safety, run-time type information, type safety