George C. Necula
ABSTRACT
In this paper we propose a scheme that combines type inference and run-time checking to make existing C programs type safe. We describe the CCured type system, which extends that of C by separating pointer types according to their usage. This type system allows both pointers whose usage can be verified statically to be type safe, and pointers whose safety must be checked at run time. We prove a type soundness result and then we present a surprisingly simple type inference algorithm that is able to infer the appropriate pointer kinds for existing C programs.Our experience with the CCured system shows that the inference is very effective for many C programs, as it is able to infer that most or all of the pointers are statically verifiable to be type safe. The remaining pointers are instrumented with efficient run-time checks to ensure that they are used safely. The resulting performance loss due to run-time checks is 0-150%, which is several times better than comparable approaches that use only dynamic checking. Using CCured we have discovered programming bugs in established C programs such as several SPECINT95 benchmarks.
- 1.M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems, 13(2):237-268, April 1991. Google Scholar
Digital Library
- 2.T. M. Austin, S. E. Breach, and G. S. Sohi. Efficient detection of all pointer and array access errors. SIGPLAN Notices, 29(6):290-301, June 1994. Proceedings of the ACM SIGPLAN '94 Conference on Programming Language Design and Implementation. Google ScholarDigital Library
- 3.H.-J. Boehm and M. Weiser. Garbage collection in an uncooperative environment. Software Practice and Experience, 27:807-820, Sept. 1997. Google ScholarDigital Library
- 4.V. Breazu-Tannen, C. A. Gunter, and A. Scedrov. Computing with coercions. In LISP and Functional Programming, pages 44 60, 1990. Google ScholarDigital Library
- 5.L. Cardelli, J. Donahue, L. Glassman, M. Jordan, B. Kalsow, and G. Nelson. Modula3 report, 1989.Google Scholar
- 6.M. C. Carlisle. Olden: Parullelizing Programs with Dynamic Data Structures on Distributed-Memory Machines. PhD thesis, Princeton University Department of Computer Science, June 1996. Google ScholarDigital Library
- 7.R. Cartwright and M. Pagan. Soft typing. In Proceedings of the '91 Conference on Programming Language Design and Implementation, pages 278-292, 1991. Google ScholarDigital Library
- 8.S. Chandra and T. Reps. Physical type checking for C. In Proceedings of the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, volume 24.5 of Softwarv Engeneering Notes (SEN), pages 66 75. ACM Press, Sept. 6 1999. Google ScholarDigital Library
- 9.D. Evans. Static detection of dynamic memory errors. ACM SIGPLAN Notices, 31(5):44 53, 1996. Google ScholarDigital Library
- 10.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.Google Scholar
- 11.F. Henglein. Global tagging optimization by type inference. In Proceedings of the 1992 ACM Conference on LISP and Functional Programming, pages 205-215, 1992. Google ScholarDigital Library
- 12.S. Jagannathan and A. Wright. Effective flow analysis for avoiding run-time checks. In Proceedings of the Second International Static Analysis Symposium, volume 983, pages 207-224. Springer-Verlag, 1995. Google ScholarDigital Library
- 13.R. W. M. Jones and P. III. J. Kelly. Backwards-compatible bounds checking for arrays and pointers in C programs. AADEBUG, 1997.Google Scholar
- 14.S. Kaufer, R. Lopez, and S. Pratap. Saber-C: an interpreterbased programming environment for the C language. In Proceedings of the Summer Usenix Confervnce, pages 161-171, 1988.Google Scholar
- 15.A. Kind and H. Friedrich. A practical approach to type inference for EuLisp. Lisp and Symbolic Computation, 6(1/2):159-176, 1993. Google ScholarDigital Library
- 16.B. Lampson. A description of the Cedar language. Technical Report CSL-83-15, Xerox Palo Alto Research Center, 1983.Google Scholar
- 17.B. Liskov, R. R. Atkinson, T. Bloom, E. B. Moss, R. Schaffert, and A. Snyder. CLU Reference Manual. Springer- Verlag, Berlin, 1981. Google ScholarDigital Library
- 18.A. Loginov, S. Yong, S. IIIorwitz, and T. Reps. Debugging via run-time type checking. In Proceedings of FACE2001: Fun - damental Appwaches to Software Engineering, Apr. 2001. Google ScholarDigital Library
- 19.H. Patil and C. N. Fischer. Efficient run-time monitoring using shadow processing. In Automated and Algorithmic Debugging, pages 119-132, 1995.Google Scholar
- 20.H. Patil and C. N. Fischer. Low-cost, concurrent checking of pointer and array accesses in C programs. S@ware Practice and Experience, 27(1):87-110, Jan. 1997. Google ScholarDigital Library
- 21.G. Ramalingam, J. Field, and F. Tip. Aggregate structure identification and its application to program analysis. In Symposium on Principles of Programming Languages, pages 119-132, Jan. 1999. Google ScholarDigital Library
- 22.D. Remy and a. Vouillon. Objective ML: A simple objectoriented extension of ML. In Symposium on Principles of Programming Languages, pages 40-53, 1997. Google ScholarDigital Library
- 23.M. Shields, T. Sheard, and S. L. P. Jones. Dynamic typing as staged type inference. In Symposium on Principles of Programming Languages, pages 289-302, 1998. Google ScholarDigital Library
- 24.M. Sift, S. Chandra, T. Ball, K. Kunchithapadam, and T. Reps. Coping with type casts in C. In 1999 ACM Foundations on Software Engineering Conference (LNCS 1687), volume 1687 of Lecture Notes in Computer Science, pages 180-198. Springer-Verlag / ACM Press, September 1999. Google ScholarDigital Library
- 25.G. Smith and D. Volpano. A sound polymorphic type system for a dialect of C. Science of Computer Programming, 32(1 3):49-72, 1998. Google ScholarDigital Library
- 26.SPEC 95. Standard Performance Evaluation Corportation Benchmarks. http ://www. spee. org/osg/cpu95/UINT95, July 1995.Google Scholar
- 27.J. L. Steften. Adding run-time checking to the Portable C Compiler. Software Practice and Experience, 22(4):305- 316, Apr. 1992. Google ScholarDigital Library
- 28.S. Thatte. Quasi-static typing. In Conference record of the 17th ACM Symposium on Principles of Programming Languages (POPL), pages 367-381, 1990. Google ScholarDigital Library
- 29.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.Google Scholar
- 30.A. Wright and R. Cartwright. A practical soft type system for Scheme. A UM Transactions on Programming Languages and Systems, 1997. Google ScholarDigital Library
- CCured: type-safe retrofitting of legacy code
Recommendations
CCured: type-safe retrofitting of legacy software
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 ...
CCured: type-safe retrofitting of legacy code
In this paper we propose a scheme that combines type inference and run-time checking to make existing C programs type safe. We describe the CCured type system, which extends that of C by separating pointer types according to their usage. This type ...
CCured: type-safe retrofitting of legacy code
Supplemental issueIn this paper we propose a scheme that combines type inference and run-time checking to make existing C programs type safe. We describe the CCured type system, which extends that of C by separating pointer types according to their usage. This type ...
Comments