Adam Chlipala
ABSTRACT
Several recent projects have shown the feasibility of verifying low-level systems software. Verifications based on automated theorem-proving have omitted reasoning about first-class code pointers, which is critical for tasks like certifying implementations of threads and processes. Conversely, verifications that deal with first-class code pointers have featured long, complex, manual proofs. In this paper, we introduce the Bedrock framework, which supports mostly-automated proofs about programs with the full range of features needed to implement, e.g., language runtime systems.
The heart of our approach is in mostly-automated discharge of verification conditions inspired by separation logic. Our take on separation logic is computational, in the sense that function specifications are usually written in terms of reference implementations in a purely functional language. Logical quantifiers are the most challenging feature for most automated verifiers; by relying on functional programs (written in the expressive language of the Coq proof assistant), we are able to avoid quantifiers almost entirely. This leads to some dramatic improvements compared to both past work in classical verification, which we compare against with implementations of data structures like binary search trees and hash tables; and past work in verified programming with code pointers, which we compare against with examples like function memoization and a cooperative threading library.
- Mike Barnett, Bor-Yuh Evan Chang, Robert Deline, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Proc. FMCO, 2006. Google Scholar
Digital Library
- Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Proc. FMCO, 2005. Google ScholarDigital Library
- Hongxu Cai, Zhong Shao, and Alexander Vaynberg. Certified self-modifying code. In Proc. PLDI, 2007. Google ScholarDigital Library
- Cristiano Calcagno, Dino Distefano, Peter O'Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. In Proc. POPL, 2009. Google ScholarDigital Library
- Bor-Yuh Evan Chang and Xavier Rival. Relational inductive shape analysis. In Proc. POPL, 2008. Google ScholarDigital Library
- Arthur Charguéraud. Program verification through characteristic formulae. In Proc. ICFP, 2010. Google ScholarDigital Library
- Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. Effective interactive proofs for higher-order imperative programs. In Proc. ICFP, 2009. Google ScholarDigital Library
- Coq Development Team. The Coq proof assistant reference manual, version 8.3. 2010.Google Scholar
- David Delahaye. A tactic language for the system Coq. In Proc. LPAR, 2000. Google ScholarDigital Library
- David Detlefs, Greg Nelson, and James B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52(3):365--473, 2005. Google ScholarDigital Library
- Xinyu Feng and Zhong Shao. Modular verification of concurrent assembly code with dynamic thread creation and termination. In Proc. ICFP, 2005. Google ScholarDigital Library
- Xinyu Feng, Zhong Shao, Yuan Dong, and Yu Guo. Certifying low-level programs with hardware interrupts and preemptive threads. In Proc. PLDI, 2008. Google ScholarDigital Library
- Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, and Zhaozhong Ni. Modular verification of assembly code with stack-based control abstractions. In Proc. PLDI, 2006. Google ScholarDigital Library
- Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In Proc. PLDI, 2002. Google ScholarDigital Library
- Nadeem Abdul Hamid and Zhong Shao. Interfacing Hoare logic and type systems for foundational proof-carrying code. In Proc. TPHOLs, 2004.Google ScholarCross Ref
- Chris Hawblitzel and Erez Petrank. Automated verification of practical garbage collectors. In Proc. POPL, 2009. Google ScholarDigital Library
- Bart Jacobs, Jan Smans, and Frank Piessens. A quick tour of the VeriFast program verifier. In Proc. APLAS, 2010. Google ScholarDigital Library
- Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proc. SOSP, 2009. Google ScholarDigital Library
- Viktor Kuncak, Ruzica Piskac, Philippe Suter, and Thomas Wies. Building a calculus of data structures (invited paper). In Proc. VMCAI, 2010. Google ScholarDigital Library
- Andrew McCreight. Practical tactics for separation logic. In Proc. TPHOLs, 2009. Google ScholarDigital Library
- Andrew McCreight, Zhong Shao, Chunxiao Lin, and Long Li. A general framework for certifying garbage collectors and their mutators. In Proc. PLDI, 2007. Google ScholarDigital Library
- Farhad Mehta and Tobias Nipkow. Proving pointer programs in higher-order logic. In Proc. CADE, 2003.Google ScholarCross Ref
- Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: Reasoning with the awkward squad. In Proc. ICFP, 2008.Google Scholar
- Zhaozhong Ni and Zhong Shao. Certified assembly programming with embedded code pointers. In Proc. POPL, 2006. Google ScholarDigital Library
- Zhaozhong Ni, Dachuan Yu, and Zhong Shao. Modular verification of machine-level thread implementation. Technical report, 2006.Google Scholar
- Zhaozhong Ni, Dachuan Yu, and Zhong Shao. Using XCAP to certify realistic system code: Machine context management. In Proc. TPHOLs, 2007. Google ScholarDigital Library
- Lawrence C. Paulson. Isabelle: A generic theorem prover. Journal of Automated Reasoning, 5, 1994.Google Scholar
- John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. LICS, 2002. Google ScholarDigital Library
- Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. TOPLAS, 24, 2002. Google ScholarDigital Library
- Jean Yang and Chris Hawblitzel. Safe to the last instruction: automated verification of a type-safe operating system. In Proc. PLDI, 2010. Google ScholarDigital Library
- Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In Proc. PLDI, 2008. Google ScholarDigital Library
- Karen Zee, Viktor Kuncak, and Martin Rinard. An integrated proof language for imperative programs. In Proc. PLDI, 2009. Google ScholarDigital Library
Index Terms
- Mostly-automated verification of low-level programs in computational separation logic
Recommendations
Mostly-automated verification of low-level programs in computational separation logic
PLDI '11Several recent projects have shown the feasibility of verifying low-level systems software. Verifications based on automated theorem-proving have omitted reasoning about first-class code pointers, which is critical for tasks like certifying ...
Effective interactive proofs for higher-order imperative programs
ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programmingWe present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, ...
The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier
ICFP '13We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is ...
Comments