David Greenaway
ABSTRACT
We present an approach for automatically generating provably correct abstractions from C source code that are useful for practical implementation verification. The abstractions are easier for a human verification engineer to reason about than the implementation and increase the productivity of interactive code proof. We guarantee soundness by automatically generating proofs that the abstractions are correct.
In particular, we show two key abstractions that are critical for verifying systems-level C code: automatically turning potentially overflowing machine-word arithmetic into ideal integers, and transforming low-level C pointer reasoning into separate abstract heaps. Previous work carrying out such transformations has either done so using unverified translations, or required significant proof engineering effort.
We implement these abstractions in an existing proof-producing specification transformation framework named AutoCorres, developed in Isabelle/HOL, and demonstrate its effectiveness in a number of case studies. We show scalability on multiple OS microkernels, and we show how our changes to AutoCorres improve productivity for total correctness by porting an existing high-level verification of the Schorr-Waite algorithm to a low-level C implementation with minimal effort.
- E. Alkassar, M. Hillebrand, D. Leinenbach, N. Schirmer, and A. Starostin. The Verisoft approach to systems verification. In VSTTE 2008, volume 5295 of LNCS, pages 209--224. Springer, 2008. Google Scholar
Digital Library
- A. Appel. Verified software toolchain. In 20th ESOP, volume 6602 of LNCS, pages 1--17. Springer, 2011. Google ScholarDigital Library
- T. Ball, E. Bounimova, R. Kumar, and V. Levin. SLAM2: Static driver verification with under 4% false alarms. In 2010 FMCAD, pages 35--42, Lugano, Switzerland, 2010. FMCAD Inc. Google ScholarDigital Library
- J. Bloch. Nearly all binary searches and mergesorts are broken. http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html, Jun 2006.Google Scholar
- R. Bornat. Proving pointer programs in Hoare Logic. In 5th MPC, volume 1837 of LNCS, pages 102--126. Springer, Jul 2000. Google ScholarDigital Library
- A. Chlipala. The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In 18th ICFP, pages 391--402. ACM, 2013. Google ScholarDigital Library
- D. Cock, G. Klein, and T. Sewell. Secure microkernels, state monads and scalable refinement. In 21st TPHOLs, volume 5170 of LNCS, pages 167--182, Montreal, Canada, Aug 2008. Springer. Google ScholarDigital Library
- E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In 22nd TPHOLs, volume 5674 of LNCS, pages 23--42, Munich, Germany, 2009. Springer. Google ScholarDigital Library
- C. Ellison and G. Roşu. An executable formal semantics of C with applications. In 39th POPL, pages 533--544. ACM, 2012. Google ScholarDigital Library
- D. Greenaway. Autocorres tool. http://ssrg.nicta.com.au/projects/TS/autocorres/, 2014.Google Scholar
- D. Greenaway, J. Andronick, and G. Klein. Bridging the gap: Automatic verified abstraction of C. In 3rd ITP, volume 7406 of LNCS, pages 99--115, Princeton, New Jersey, Aug 2012. Springer.Google Scholar
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with Blast. In 10th SPIN, volume 2648 of LNCS, pages 235--239, Portland, OR, USA, May 2003. Springer. Google ScholarDigital Library
- T. Hubert and C. Marché. A case study of C source code verification: the Schorr-Waite algorithm. In 3rd Int. Conf. Softw. Engin. & Formal Methods, pages 190--199. IEEE, Sep 2005. Google ScholarDigital Library
- ISO/IEC. Programming languages --- C. Technical Report 9899:TC2, ISO/IEC JTC1/SC22/WG14, May 2005.Google Scholar
- G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. In SOSP, pages 207--220, Big Sky, MT, USA, Oct 2009. ACM. Google ScholarDigital Library
- G. Klein, R. Kolanski, and A. Boyton. Mechanised separation algebra. In 3rd ITP, volume 7406 of LNCS, pages 332--337. Springer, 2012.Google Scholar
- X. Leroy. Formal verification of a realistic compiler. CACM, 52(7): 107--115, 2009. Google ScholarDigital Library
- F. Mehta and T. Nipkow. Proving pointer programs in higher-order logic. In 19th CADE, volume 2741 of LNCS, pages 121--135, 2003.Google Scholar
- Y. Moy. Automatic Modular Static Safety Checking for C Programs. PhD thesis, Université Paris-Sud, Paris, France, Jan 2009.Google Scholar
- T. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein. seL4: from general purpose to a proof of information flow enforcement. In IEEE Symp. Security & Privacy, pages 415--429, San Francisco, CA, May 2013. Google ScholarDigital Library
- T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL --- A Proof Assistant for Higher-Order Logic. Springer, 2002. Google ScholarDigital Library
- L. Noschinski, C. Rizkallah, and K. Mehlhorn. Verification of certifying computations through AutoCorres and Simpl. In NASA Formal Methods, volume 8430 of LNCS. Springer, 2014. To appear.Google ScholarDigital Library
- N. Schirmer. Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technische Universität München, 2006.Google Scholar
- H. Schorr and W. M. Waite. An efficient machine-independent procedure for garbage collection in various list structures. CACM, 10 (8):501--506, 1967. Google ScholarDigital Library
- T. Sewell, M. Myreen, and G. Klein. Translation validation for a verified OS kernel. In 2013 PLDI, pages 471--481. ACM, 2013. Google ScholarDigital Library
- N. Suzuki. Automatic Verification of Programs with Complex Data Structures. Garland Publishing, New York, 1980.Google Scholar
- H. Tuch, G. Klein, and M. Norrish. Types, bytes, and separation logic. In 34th POPL, pages 97--108, Nice, France, Jan 2007. ACM. Google ScholarDigital Library
- D. von Oheimb and T. Nipkow. Machine-checking the java specification: Proving type-safety. In Formal Syntax and Semantics of Java, volume 1523 of LNCS, pages 119--156. Springer, 1999. Google ScholarDigital Library
- X. Wang, H. Chen, A. Cheung, Z. Jia, N. Zeldovich, and M. F. Kaashoek. Undefined behavior: what happened to my code? In 3rd APSys, pages 9:1--9:7, New York, NY, USA, 2012. ACM. Google ScholarDigital Library
- S. Winwood, G. Klein, T. Sewell, J. Andronick, D. Cock, and M. Norrish. Mind the gap: A verification framework for low-level C. In 22nd TPHOLs, volume 5674 of LNCS, pages 500--515. Springer, 2009. Google ScholarDigital Library
Index Terms
- Don't sweat the small stuff: formal verification of C code without the pain
Recommendations
Don't sweat the small stuff: formal verification of C code without the pain
PLDI '14We present an approach for automatically generating provably correct abstractions from C source code that are useful for practical implementation verification. The abstractions are easier for a human verification engineer to reason about than the ...
Coinductive Verification of Program Optimizations Using Similarity Relations
Formal verification methods have gained increased importance due to their ability to guarantee system correctness and improve reliability. Nevertheless, the question how proofs are to be formalized in theorem provers is far from being trivial, yet very ...
Formalization of the Resolution Calculus for First-Order Logic
I present a formalization in Isabelle/HOL of the resolution calculus for first-order logic with formal soundness and completeness proofs. To prove the calculus sound, I use the substitution lemma, and to prove it complete, I use Herbrand interpretations ...
Comments