CCured

作者: George C. Necula , Scott McPeak , Westley Weimer

DOI: 10.1145/2442776.2442786

关键词: Pointer (computer programming)Programming languageSoundnessOperational semanticsData structureComputer scienceType inferenceLegacy codeDangling pointerMemory safetySoftwareComputer Graphics and Computer-Aided Design

摘要: In this paper we propose a scheme that combines type inference and run-time checking to make existing C programs safe. We describe the CCured system, which extends of by separating pointer types according their usage. This system allows both pointers whose usage can be verified statically safe, safety must checked at run time. prove soundness result then present surprisingly simple algorithm is able infer appropriate kinds for programs.Our experience with shows very effective many programs, as it most or all are verifiable The remaining instrumented efficient checks ensure they used safely. resulting performance loss due 0-150%, several times better than comparable approaches use only dynamic checking. Using have discovered programming bugs in established such SPECINT95 benchmarks.

参考文章(27)
Suresh Jagannathan, Andrew Wright, Effective Flow Analysis for Avoiding Run-Time Checks static analysis symposium. pp. 207- 224 ,(1995) , 10.1007/3-540-60360-3_41
Paul H. J. Kelly, Richard W. M. Jones, Backwards-Compatible Bounds Checking for Arrays and Pointers in C Programs Proceedings of the 3rd International Workshop on Automatic Debugging; 1997 (AADEBUG-97). pp. 13- 26 ,(1997)
Eric A. Brewer, Alexander Aiken, David A. Wagner, Jeffrey S. Foster, A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities. network and distributed system security symposium. ,(2000)
Alexey Loginov, Suan Hsi Yong, Susan Horwitz, Thomas Reps, Debugging via Run-Time Type Checking fundamental approaches to software engineering. pp. 217- 232 ,(2001) , 10.1007/3-540-45314-8_16
Mark Shields, Tim Sheard, Simon Peyton Jones, Dynamic typing as staged type inference symposium on principles of programming languages. pp. 289- 302 ,(1998) , 10.1145/268946.268970
Todd M. Austin, Scott E. Breach, Gurindar S. Sohi, Efficient detection of all pointer and array access errors programming language design and implementation. ,vol. 29, pp. 290- 301 ,(1994) , 10.1145/178243.178446
Satish Thatte, Quasi-static typing Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90. pp. 367- 381 ,(1990) , 10.1145/96709.96747
Martín Abadi, Luca Cardelli, Benjamin Pierce, Gordon Plotkin, Dynamic typing in a statically typed language ACM Transactions on Programming Languages and Systems. ,vol. 13, pp. 237- 268 ,(1991) , 10.1145/103135.103138