CCured

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 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.

This software is also peer reviewed by journal TOMS.


References in zbMATH (referenced in 23 articles )

Showing results 1 to 20 of 23.
Sorted by year (citations)

1 2 next

  1. Huang, Daniel; Morrisett, Greg: Formalizing the safecode type system (2013)
  2. Godefroid, Patrice; Nori, Aditya V.; Rajamani, Sriram K.; Tetali, Sai Deep: Compositional may-must program analysis: unleashing the power of alternation (2010)
  3. Pedersen, Leif; Reza, Hassan: Using Pit to improve security in low-level programs (2010)
  4. Conway, Christopher L.; Dams, Dennis; Namjoshi, Kedar S.; Barrett, Clark: Pointer analysis, conditional soundness, and proving the absence of errors (2008)
  5. Sathre, Jesse; Zambreno, Joseph: Automated software attack recovery using rollback and huddle (2008)
  6. Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak: The software model checker blast (2007)
  7. Jhala, Ranjit; Majumdar, Rupak; Xu, Ru-Gang: State of the union: Type inference via Craig interpolation (2007)
  8. Matousek, Tomas; Zavoral, Filip: Extracting Zing models from C source code (2007)
  9. Smith, Michael J.A.: Stochastic modelling of communication protocols from source code. (2007)
  10. Sidiroglou, Stelios; Keromytis, Angelos D.: Execution transactions for defending against software failures: use and evaluation (2006)
  11. Sidiroglou, Stelios; Keromytis, Angelos D.: Execution transactions for defending against software failures: use and evaluation (2006)
  12. Della Penna, Giuseppe: A type system for static and dynamic checking of C++ pointers (2005)
  13. Godefroid, Patrice; Klarlund, Nils: Software model checking: Searching for computations in the abstract or the concrete (2005)
  14. Richardson, David G.; Krandick, Werner: Compiler-enforced memory semantics in the SACLIB computer algebra library (2005)
  15. Weimer, Westley; Necula, George C.: Mining temporal specifications for error detection (2005)
  16. Yong, Suan Hsi; Horwitz, Susan: Using static analysis to reduce dynamic analysis overhead (2005)
  17. Frolov, A.M.: A hybrid approach to enhancing the reliability of software (2004)
  18. Musuvathi, Madanlal; Engler, Dawson R.: Some lessons from using static analysis and software model checking for bug finding. (2003)
  19. Oiwa, Yutaka; Sekiguchi, Tatsurou; Sumii, Eijiro; Yonezawa, Akinori: Fail-safe ANSI-C compiler: An approach to making C programs secure (2003)
  20. Shibayama, Etsuya; Yonezawa, Akinori: Secure software infrastructure in the Internet age (2003)

1 2 next