Advertisement

Journal of Automated Reasoning

, Volume 42, Issue 2–4, pp 125–187 | Cite as

Formal Verification of C Systems Code

Structured Types, Separation Logic and Theorem Proving
  • Harvey Tuch
Article

Abstract

Systems code is almost universally written in the C programming language or a variant. C has a very low level of type and memory abstraction and formal reasoning about C systems code requires a memory model that is able to capture the semantics of C pointers and types. At the same time, proof-based verification demands abstraction, in particular from the aliasing and frame problems. In this paper we present a study in the mechanisation of two proof abstractions for pointer program verification in the Isabelle/HOL theorem prover, based on a low-level memory model for C. The language’s type system presents challenges for the multiple independent typed heaps (Burstall-Bornat) and separation logic proof techniques. In addition to issues arising from explicit value size/alignment, padding, type-unsafe casts and pointer address arithmetic, structured types such as C’s arrays and structs are problematic due to the non-monotonic nature of pointer and lvalue validity in the presence of the unary &-operator. For example, type-safe updates through pointers to fields of a struct break the independence of updates across typed heaps or ∧*-conjuncts. We provide models and rules that are able to cope with these language features and types, eschewing common over-simplifications and utilising expressive shallow embeddings in higher-order logic. Two case studies are provided that demonstrate the applicability of the mechanised models to real-world systems code; a working of the standard in-place list reversal example and an overview of the verification of the L4 microkernel’s memory allocator.

Keywords

Separation logic Interactive theorem proving 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Programming languages—C. Technical report 9899:TC2, ISO/IEC JTC1/SC22/WG14 (2005)Google Scholar
  2. 2.
    Appel, A.W., Blazy, S.: Separation logic for small-step Cminor. In: Schneider, K., Brandt, J. (eds.) Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007). Lecture Notes in Computer Science, vol. 4732, pp. 5–21. Springer, New York (2007)Google Scholar
  3. 3.
    Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) Proceedings of the 8th International SPIN Workshop on Model Checking Software. Lecture Notes in Computer Science, vol. 2057, pp. 103–122. Springer, New York (2001)Google Scholar
  4. 4.
    Berdine, J., Calcagno, C., O’Hearn, P.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) Proceedings of the 24th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2004). Lecture Notes in Computer Science, vol. 3328, pp. 97–109. Springer, New York (2004)Google Scholar
  5. 5.
    Bijlsma, A.: Calculating with pointers. Sci. Comput. Program 12(3), 191–205 (1989)MATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Blume, M.: No-longer-foreign: teaching an ML compiler to speak C “natively”. Electron. Notes Theoret. Comput. Sci. 59(1), 36–52 (2001)CrossRefGoogle Scholar
  7. 7.
    Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R.C., Oliveira, J.N. (eds.) Proceedings of the 5th International Conference on Mathematics of Program Construction (MPC 2000). Lecture Notes in Computer Science, vol. 1837, pp. 102–126. Springer, New York (2000)Google Scholar
  8. 8.
    Burstall, R.: Some techniques for proving correctness of programs which alter data structures. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 23–50. Edinburgh University Press, Edinburgh (1972)Google Scholar
  9. 9.
    Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Beyond reachability: shape abstraction in the presence of pointer arithmetic. In: Yi, K. (ed.) Proceedings of the 13th International Symposium on Static Analysis (SAS 2006). Lecture Notes in Computer Science, vol. 4134, pp. 182–203. Springer, New York (2006)Google Scholar
  10. 10.
    Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2001). Lecture Notes in Computer Science, vol. 2245, pp. 108–119. Springer, New York (2001)Google Scholar
  11. 11.
    Cartwright, R., Oppen, D.C.: The logic of aliasing. Technical report STAN-CS-79-740, Stanford University, Stanford (1979)Google Scholar
  12. 12.
    Cock, D.: Bitfields and tagged unions in C: verification through automatic generation. In: Beckert, B., Klein, G. (eds.) Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, vol. 372 of CEUR Workshop Proceedings (2008). CEUR-WS.org
  13. 13.
    Filliâtre, J.-C., Marché, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) Proceedings of the 6th International Conference on Formal Methods and Software Engineering (ICFEM 2004). Lecture Notes in Computer Science, vol. 3308, pp. 15–29. Springer, New York (2004)Google Scholar
  14. 14.
    Hallem, S., Chelf, B., Xie, Y., Engler, D.R.: A system and language for building system-specific, static analyses. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation. SIGPLAN Notices, vol. 37, pp. 69–82. ACM, New York (2002)CrossRefGoogle Scholar
  15. 15.
    Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T.F. (eds.) Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005). Lecture Notes in Computer Science, vol. 3603, pp. 114–129. Springer, New York (2005)Google Scholar
  16. 16.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) Proceedings of the 10th International SPIN Workshop on Model Checking Software (SPIN 2003). Lecture Notes in Computer Science, vol. 2648, pp. 235–239. Springer, New York (2003)Google Scholar
  17. 17.
    Hohmuth, M., Tews, H., Stephens, S.G.: Applying source-code verification to a microkernel—the VFiasco project. Technical report TUD-FI02-03-März, TU Dresden (2002)Google Scholar
  18. 18.
    Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2001). SIGPLAN Notices, vol. 36, pp. 14–26. ACM, New York (2001)CrossRefGoogle Scholar
  19. 19.
    Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice-Hall, Englewood Cliffs, New Jersey (1988)Google Scholar
  20. 20.
    Klein, G.: Verified java bytecode verification. Ph.D. thesis, Institut für Informatik, Technische Universität München (2003)Google Scholar
  21. 21.
    Kroening, D.: Application specific higher order logic theorem proving. In: Autexier, S., Mantel, H. (eds.) Proceedings of the 2nd Verification Workshop (VERIFY 2002), pp. 5–15, Technical Report no. 2002/07. DIKU (2002)Google Scholar
  22. 22.
    L4Ka Team. L4 eXperimental kernel reference manual version X.2. University of Karlsruhe. http://l4ka.org/projects/version4/l4-x2.pdf (2001). Oct 2001
  23. 23.
    Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason. 41(1), 1–31 (2008)MATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Liedtke, J.: On μ-kernel construction. In: Proceedings of the Fifteenth ACM Symposium on Operating System Principles (SOSP 95). Operating System Review, vol. 29, pp. 267–284. ACM, New York (1995)Google Scholar
  25. 25.
    Marti, N., Affeldt, R., Yonezawa, A.: Verification of the heap manager of an operating system using separation logic. In: Third workshop on Semantics, Program Analysis, and Computing Environments For Memory Management (SPACE 2006), pp. 61–72. Charleston, South Carolina (2006)Google Scholar
  26. 26.
    Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Inf. Comput. 199(1–2), 200–227 (2005)MATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation. SIGPLAN Notices, vol. 37, pp. 221–231. ACM, New York (2001)CrossRefGoogle Scholar
  28. 28.
    Morris, J.M.: A general axiom of assignment. In: Broy, M., Schmidt, G. (eds.) Theoretical Foundations of Programming Methodology (Proceedings of the 1981 Maktoberdorf Summer School), pp. 25–51 (1982)Google Scholar
  29. 29.
    Moy, Y.: Union and cast in deductive verification. In: C/C++ Verification Workshop, pp. 1–16. Technical report ICIS-R07015. Radboud University Nijmegen (2007)Google Scholar
  30. 30.
    Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (eds.) Proceedings of the 11th International Conference on Compiler Construction (CC 2002). Lecture Notes in Computer Science, vol. 2304, pp. 213–228. Springer, New York (2002)Google Scholar
  31. 31.
    Nipkow, T.: Term rewriting and beyond—theorem proving in Isabelle. Form. Asp. Comput. 1(4), 320–338 (1989)CrossRefGoogle Scholar
  32. 32.
    Norrish, M.: C formalised in HOL. Ph.D. thesis, Computer Laboratory, University of Cambridge (1998)Google Scholar
  33. 33.
    O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) Proceedings of the 15th International Workshop on Computer Science Logic (CSL 2001). Lecture Notes in Computer Science, vol. 2142, pages 1–19. Springer, New York (2001)Google Scholar
  34. 34.
    Oheimb: D.v.: Information flow control revisited: noninfluence = noninterference + nonleakage. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) Proceedings of the 9th European Symposium on Research in Computer Security (ESORICS 2004). Lecture Notes in Computer Science, vol. 3193, pages 225–243. Springer, New York (2004)Google Scholar
  35. 35.
    Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reason. 5(3), 363–397 (1989)MATHCrossRefMathSciNetGoogle Scholar
  36. 36.
    Preoteasa, V.: Mechanical verification of recursive procedures manipulating pointers using separation logic. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) Proceedings of the 14th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 508–523. Springer, New York (2006)Google Scholar
  37. 37.
    Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structures. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millenial Perspectives in Computer Science, pp. 303–321. Palgrave, Houndsmill, Hampshire (2000)Google Scholar
  38. 38.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55–74. IEEE Computer Society (2002)Google Scholar
  39. 39.
    Ritchie, D.M.: The development of the C language. In: Proceedings of the ACM History of Programming Languages Conference (HOPL-II). SIGPLAN Notices, vol. 28, pp. 201–208. ACM, New York (1993)CrossRefGoogle Scholar
  40. 40.
    Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1999), pp. 105–118. ACM, New York (1999)CrossRefGoogle Scholar
  41. 41.
    Schirmer, N.: Verification of sequential imperative programs in Isabelle/HOL. Ph.D. thesis, Technische Universität München (2006)Google Scholar
  42. 42.
    Schlich, B., Kowalewski, S.: Model checking C source code for embedded systems. In: Margaria, T., Steffen, B., Hinchey, M.G. (eds.) Proceedings of the IEEE/NASA Workshop Leveraging Applications of Formal Methods, Verification, and Validation (IEEE/NASA ISoLA 2005), pp. 65–77. NASA, Maryland, USA (2005). NASA/CP-2005-212788Google Scholar
  43. 43.
    Shapiro, J.: Programming language challenges in systems codes: why systems programmers still use C, and what to do about it. In: Probst, C.W. (ed.) Proceedings of the 3rd Workshop on Programming Languages and Operating Systems: Linguistic Support for Modern Operating Systems (PLOS 2006), pp. 9. ACM, New York (2006)CrossRefGoogle Scholar
  44. 44.
    System Architecture Group. The L4Ka::Pistachio microkernel. White paper, University of Karlsruhe, May 2003. http://l4ka.org/projects/pistachio/pistachio-whitepaper.pdf
  45. 45.
    Tews, H.: Verifying Duff’s device: a simple compositional denotational semantics for goto and computed jumps (2004). http://www.cs.ru.nl/~tews/Goto/goto.pdf
  46. 46.
    Tuch, H.: Formal memory models for verifying C systems code. Ph.D. thesis, University of NSW (2008)Google Scholar
  47. 47.
    Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), pp. 97–108. ACM, New York (2007)CrossRefGoogle Scholar
  48. 48.
    Weber, T.: Towards mechanized program verification with separation logic. In: Marcinkowski, J., Tarlecki, A. (eds.) Proceedings of the 18th International Workshop on Computer Science Logic (CSL 2004). Lecture Notes in Computer Science, vol. 3210, pp. 250–264. Springer, New York (2004)Google Scholar
  49. 49.
    Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 97). Lecture Notes in Computer Science, vol. 1275, pp. 307–322. Springer, New York (1997)Google Scholar
  50. 50.
    Yang, H., O’Hearn, P.W.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002). Lecture Notes in Computer Science, vol. 2303, pp. 402–416. Springer, New York (2002)Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2009

Authors and Affiliations

  1. 1.Sydney Research Lab.National ICT AustraliaEveleighAustralia

Personalised recommendations