Harvey Tuch
Michael Norrish
ABSTRACT
We present a formal model of memory that both captures the low-level features of C's pointers and memory, and that forms the basis for an expressive implementation of separation logic. At the low level, we do not commit common oversimplifications, but correctly deal with C's model of programming language values and the heap. At the level of separation logic, we are still able to reason abstractly and efficiently. We implement this framework in the theorem prover Isabelle/HOL and demonstrate it on two case studies. We show that the divide between detailed and abstract does not impose undue verification overhead, and that simple programs remain easy to verify. We also show that the framework is applicable to real, security- and safety-critical code by formally verifying the memory allocator of the L4 microkernel.
- Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In 13th International Symposium on Static Analysis (SAS 2006), volume 4134 of Lecture Notes in Computer Science, pages 182--203. Springer, 2006. Google Scholar
Digital Library
- T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN'01, Workshop on Model Checking of Software, volume 2057 of Lecture Notes in Computer Science, pages 103--122, 2001. Google ScholarDigital Library
- J. Berdine, C. Calcagno, and P. O'Hearn. A decidable fragment of separation logic. In FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16--18, 2004, 2004. Google ScholarDigital Library
- W. R. Bevier. Kit: A study in operating system verification. IEEE Transactions on Software Engineering, 15(11):1382--1396, 1989. Google ScholarDigital Library
- D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. Checking memory safety with Blast. In Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE), volume 3442 ofLecture Notes in Computer Science, pages 2--18. Springer, 2005. Google ScholarDigital Library
- J. Bloch. Nearly all binary searches and mergesorts are broken. newblock http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html, June 2006.Google Scholar
- M. Blume. No-longer-foreign: Teaching an ML compiler to speak C "natively". Electronic Notes in Theoretical Computer Science, 59(1), 2001.Google Scholar
- R. Bornat. Proving pointer programs in Hoare Logic. In R. Backhouse and J. Oliveira, editors,Mathematics of Program Construction (MPC 2000), volume 1837 of LNCS, pages 102--126. Springer, 2000. Google ScholarDigital Library
- R. Burstall. Some techniques for proving correctness of programs which alter data structures. In B. Meltzer and D. Michie, editors, Machine Intelligence 7, pages 23--50. Edinburgh University Press, 1972.Google Scholar
- B. Cook, D. Kroening, and N. Sharygina. Cogent: Accurate theorem proving for program verification. In K. Etessami and S. K. Rajamani, editors, Proceedings of CAV 2005, volume 3576 ofLecture Notes in Computer Science, pages 296--300. Springer Verlag, 2005. Google ScholarDigital Library
- M. Daum, S. Maus, N. Schirmer, and M. N. Seghir. Integration of a software model checker into Isabelle. In G. Sutcliffe and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005, volume 3835 ofLecture Notes in Artificial Intelligence, pages 381--395, Montego Bay, Jamaica, October 2005. Springer. Google ScholarDigital Library
- J.-C. Filliâtre and C. Marché. Multi-prover verification of C programs. InFormal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, USA, volume 3308 ofLNCS, pages 15--29. Springer, 2004.Google Scholar
- M. Gargano, M. Hillebrand, D. Leinenbach, and W. Paul. On the correctness of operating system kernels. In Proc. 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'05), pages 1--16, Oxford, UK, 2005. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with Blast. In SPIN'03, Workshop on Model Checking Software, 2003. Google ScholarDigital Library
- M. Hohmuth, H. Tews, and S. G. Stephens. Applying source-code verification to a microkernel --- the VFiasco project. Technical Report TUD-FI02-03-M"arz, TU Dresden, 2002.Google Scholar
- S. S. Ishtiaq and P. W. O'Hearn. BI as an assertion language for mutable data structures. In POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 14--26, New York, NY, USA, 2001. ACM Press. Google ScholarDigital Library
- L4Ka Team. L4 emphfootnotesize eXemphfootnotesize perimental Kernel Reference Manual Version X.2. University of Karlsruhe, Oct. 2001. http://l4ka.org/projects/version4/l4-x2.pdf.Google Scholar
- N. Marti, R. Affeldt, and A. Yonezawa. 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), pages 61--72, Jan. 2006.Google ScholarDigital Library
- F. Mehta and T. Nipkow. Proving pointer programs in higher-order logic. Information and Computation, 2005. To appear. Google ScholarDigital Library
- A. Moller and M. I. Schwartzbach. The pointer assertion logic engine. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '01, June 2001. Google ScholarDigital Library
- G. Necula, J. Condit, M. Harren, S. McPeak, and W. Weimer. CCured: type-safe retrofitting of legacy software. ACM Trans. Prog. Lang. Syst., 27(3):477--526, 2005. Google ScholarDigital Library
- P. G. Neumann, R. S. Boyer, R. J. Feiertag, K. N. Levitt, and L. Robinson. A provably secure operating system: The system, its applications, and proofs. Technical Report CSL-116, SRI International, 1980.Google Scholar
- T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL --- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google ScholarDigital Library
- M. Norrish. C formalised in HOL. PhD thesis, Computer Laboratory, University of Cambridge, 1998.Google Scholar
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. 17th IEEE Symposium on Logic in Computer Science, pages 55--74, 2002. Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 105--118. ACM Press, 1999. Google ScholarDigital Library
- N. Schirmer. Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technische Universit"at München, 2006.Google Scholar
- H. Tuch and G. Klein. A unified memory model for pointers. In G. Sutcliffe and A. Voronkov, editors, 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-12), volume 3835 ofLNCS, pages 474--488, 2005. Google ScholarDigital Library
- H. Tuch, G. Klein, and M. Norrish. Verification of the L4 kernel memory allocator. Formal proof document. http://www.ertos.nicta.com.au/research/l4.verified/kmalloc.pml, July 2006.Google Scholar
- B. Walker, R. Kemmerer, and G. Popek. Specification and verification of the UCLA Unix security kernel. CACM, 23(2):118--131, 1980. Google ScholarDigital Library
- T. Weber. Towards mechanized program verification with separation logic. In J. Marcinkowski and A. Tarlecki, editors,Computer Science Logic -- 18th International Workshop, CSL 2004, volume 3210 ofLecture Notes in Computer Science, pages 250--264. Springer, 2004.Google Scholar
- M. Wenzel. Type classes and overloading in higher-order logic. In E. L. Gunter and A. Felty, editors,Theorem Proving in Higher Order Logics'97, volume 1275 ofLNCS, pages 307--322. Springer, 1997. Google ScholarDigital Library
- M. Wildmoser and T. Nipkow. Certifying machine code safety: Shallow versus deep embedding. In K. Slind, A. Bunker, and G. Gopalakrishnan, editors,Theorem Proving in Higher Order Logics 2004, volume 3223 ofLNCS, pages 305--320. Springer, 2004.Google Scholar
- H. Yang and P. W. O'Hearn. A semantic basis for local reasoning. In Foundations of Software Science and Computation Structure, pages 402--416, 2002. Google ScholarDigital Library
- K. Zee, P. Lam, V. Kuncak, and M. Rinard. Combining theorem proving with static analysis for data structure consistency. In Int. Workshop on Software Verification and Validation, 2004.Google Scholar
Index Terms
- Types, bytes, and separation logic
Recommendations
Types, bytes, and separation logic
Proceedings of the 2007 POPL ConferenceWe present a formal model of memory that both captures the low-level features of C's pointers and memory, and that forms the basis for an expressive implementation of separation logic. At the low level, we do not commit common oversimplifications, but ...
Structured Types and Separation Logic
Structured types, such as C's arrays and structs, present additional challenges in pointer program verification. The conventional proof abstractions, multiple independent typed heaps and separation logic, which in previous work have been built on a low-...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesWhen using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Comments