Document Open Access Logo

Generating Verified LLVM from Isabelle/HOL

Author Peter Lammich

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.22.pdf
  • Filesize: 0.5 MB
  • 19 pages

Document Identifiers

Author Details

Peter Lammich
  • The University of Manchester, UK

Funding

We received funding from DFG grant LA 3292/1 "Verifizierte Model Checker" and VeTSS grant "Formal Verification of Information Flow Security for Relational Databases".

Acknowledgements

We thank Maximilian P. L. Haslbeck and Simon Wimmer for proofreading and useful suggestions.

Cite As Get BibTex

Peter Lammich. Generating Verified LLVM from Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.22

Abstract

We present a framework to generate verified LLVM programs from Isabelle/HOL. It is based on a code generator that generates LLVM text from a simplified fragment of LLVM, shallowly embedded into Isabelle/HOL. On top, we have developed a separation logic, a verification condition generator, and an LLVM backend to the Isabelle Refinement Framework.
As case studies, we have produced verified LLVM implementations of binary search and the Knuth-Morris-Pratt string search algorithm. These are one order of magnitude faster than the Standard-ML implementations produced with the original Refinement Framework, and on par with unverified C implementations. Adoption of the original correctness proofs to the new LLVM backend was straightforward.
The trusted code base of our approach is the shallow embedding of the LLVM fragment and the code generator, which is a pretty printer combined with some straightforward compilation steps.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Logic and verification
  • Theory of computation → Separation logic
Keywords
  • Isabelle/HOL
  • LLVM
  • Separation Logic
  • Verification Condition Generator
  • Code Generation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Program Logics for Certified Compilers. Cambridge University Press, New York, NY, USA, 2014. Google Scholar
  2. Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk, and Thomas Sewell. Finite Machine Word Library. Archive of Formal Proofs, June 2016. , Formal proof development. URL: http://isa-afp.org/entries/Word_Lib.html.
  3. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT Solvers. J. Autom. Reasoning, 51(1):109-128, 2013. URL: https://doi.org/10.1007/s10817-013-9278-5.
  4. Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263-288, 2009. URL: http://xavierleroy.org/publi/Clight.pdf.
  5. Joshua Bloch. Extra, Extra - Read All About It: Nearly All Binary Searches and Mergesorts are Broken. URL: http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html.
  6. Julian Brunner and Peter Lammich. Formal Verification of an Executable LTL Model Checker with Partial Order Reduction. J. Autom. Reasoning, 60(1):3-21, 2018. URL: https://doi.org/10.1007/s10817-017-9418-4.
  7. Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, and John Matthews. Imperative Functional Programming with Isabelle/HOL. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, TPHOLs 2008, volume 5170 of LNCS, pages 134-149. Springer, 2008. Google Scholar
  8. C. Calcagno, P.W. O'Hearn, and Hongseok Yang. Local Action and Abstract Separation Logic. In LICS 2007, pages 366-378, July 2007. Google Scholar
  9. Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. Journal of Automated Reasoning, 61, February 2018. URL: https://doi.org/10.1007/s10817-018-9457-5.
  10. Clang: a C language family frontend for LLVM. URL: https://clang.llvm.org/.
  11. Luís Cruz-Filipe, Marijn Heule, Warren Hunt, Matt Kaufmann, and Peter Schneider-Kamp. Efficient Certified RAT Verification. In Proc. of CADE. Springer, 2017. Google Scholar
  12. Luís Cruz-Filipe, Joao Marques-Silva, and Peter Schneider-Kamp. Efficient Certified Resolution Proof Checking. In Proc. of TACAS, pages 118-135. Springer, 2017. Google Scholar
  13. Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Trans. Program. Lang. Syst., 13(4):451-490, October 1991. URL: https://doi.org/10.1145/115372.115320.
  14. Deep Spec Project Web Page. URL: https://deepspec.org/.
  15. Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A Fully Verified Executable LTL Model Checker. In CAV, volume 8044 of LNCS, pages 463-478. Springer, 2013. Google Scholar
  16. Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich. A verified SAT solver with watched literals using Imperative HOL. In Proc. of CPP, pages 158-171, 2018. Google Scholar
  17. David Greenaway, Japheth Lim, June Andronick, and Gerwin Klein. Don't sweat the small stuff: formal verification of C code without the pain. In Proc. of PLDI '14, pages 429-439, 2014. URL: https://doi.org/10.1145/2594291.2594296.
  18. Florian Haftmann, Alexander Krauss, Ondřej Kunčar, and Tobias Nipkow. Data Refinement in Isabelle/HOL. In Proc. of ITP, pages 100-115. Springer, 2013. Google Scholar
  19. Fabian Hellauer and Peter Lammich. The string search algorithm by Knuth, Morris and Pratt. Archive of Formal Proofs, December 2017. , Formal proof development. URL: http://isa-afp.org/entries/Knuth_Morris_Pratt.html.
  20. Marijn Heule, Warren Hunt, Matt Kaufmann, and Nathan Wetzler. Efficient, Verified Checking of Propositional Proofs. In Proc. of ITP. Springer, 2017. Google Scholar
  21. Lars Hupel and Tobias Nipkow. A Verified Compiler from Isabelle/HOL to CakeML. In Amal Ahmed, editor, Programming Languages and Systems, pages 999-1026, Cham, 2018. Springer International Publishing. Google Scholar
  22. Gerwin Klein, Rafal Kolanski, and Andrew Boyton. Mechanised Separation Algebra. In ITP, pages 332-337. Springer, August 2012. Google Scholar
  23. Gerwin Klein, Rafal Kolanski, and Andrew Boyton. Separation Algebra. Archive of Formal Proofs, May 2012. , Formal proof development. URL: http://isa-afp.org/entries/Separation_Algebra.html.
  24. Donald E. Knuth, Jr. James H. Morris, and Vaughan R. Pratt. Fast Pattern Matching in Strings. SIAM Journal on Computing, 6(2):323-350, 1977. URL: https://doi.org/10.1137/0206024.
  25. Alexander Krauss. Recursive definitions of monadic functions. In Proc. of PAR, volume 43, pages 1-13, 2010. Google Scholar
  26. Peter Lammich. Automatic Data Refinement. In ITP, volume 7998 of LNCS, pages 84-99. Springer, 2013. Google Scholar
  27. Peter Lammich. Refinement to Imperative/HOL. In ITP, volume 9236 of LNCS, pages 253-269. Springer, 2015. Google Scholar
  28. Peter Lammich. Refinement based verification of imperative data structures. In Jeremy Avigad and Adam Chlipala, editors, CPP 2016, pages 27-36. ACM, 2016. Google Scholar
  29. Peter Lammich. Efficient Verified (UN)SAT Certificate Checking. In Proc. of CADE. Springer, 2017. Google Scholar
  30. Peter Lammich. The GRAT Tool Chain - Efficient (UN)SAT Certificate Checking with Formal Correctness Guarantees. In SAT, pages 457-463, 2017. Google Scholar
  31. Peter Lammich and S. Reza Sefidgar. Formalizing the Edmonds-Karp Algorithm. In Proc. of ITP, pages 219-234, 2016. Google Scholar
  32. Peter Lammich and S. Reza Sefidgar. Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. J. Autom. Reasoning, 62(2):261-280, 2019. URL: https://doi.org/10.1007/s10817-017-9442-4.
  33. Peter Lammich and Thomas Tuerk. Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm. In Lennart Beringer and Amy P. Felty, editors, ITP 2012, volume 7406 of LNCS, pages 166-182. Springer, 2012. Google Scholar
  34. Yong Li. Knuth-Morris-Pratt code snippet. URL: https://gist.github.com/yongpitt/5704216.
  35. LLVM language reference manual. URL: https://llvm.org/docs/LangRef.html.
  36. Andreas Lochbihler. Java and the Java Memory Model - A Unified, Machine-Checked Formalisation. In Proc. of ESOP, pages 497-517, 2012. URL: https://doi.org/10.1007/978-3-642-28869-2_25.
  37. George Markowsky. Chain-complete posets and directed sets with applications. algebra universalis, 6(1):53-68, December 1976. URL: https://doi.org/10.1007/BF02485815.
  38. Daniel Matichuk, Toby Murray, and Makarius Wenzel. Eisbach: A Proof Method Language for Isabelle. Journal of Automated Reasoning, 56(3):261-282, March 2016. URL: https://doi.org/10.1007/s10817-015-9360-2.
  39. MLton. URL: http://mlton.org/.
  40. Magnus O. Myreen and Scott Owens. Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program., 24(2-3):284-315, 2014. URL: https://doi.org/10.1017/S0956796813000282.
  41. Tobias Nipkow and Gerwin Klein. Concrete Semantics: With Isabelle/HOL. Springer Publishing Company, Incorporated, 2014. Google Scholar
  42. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  43. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc of. Logic in Computer Science (LICS), pages 55-74. IEEE, 2002. Google Scholar
  44. StringBench Benchmark Suite. URL: https://github.com/almondtools/stringbench.
  45. Philip Wadler. Theorems for free! In Proc. of FPCA, pages 347-359. ACM, 1989. Google Scholar
  46. Conrad Watt. Mechanising and verifying the WebAssembly specification. In Proc. of CPP, pages 53-65, 2018. URL: https://doi.org/10.1145/3167082.
  47. Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, SAT 2014, volume 8561 of LNCS, pages 422-429. Springer, 2014. Google Scholar
  48. Simon Wimmer and Peter Lammich. Verified Model Checking of Timed Automata. In TACAS 2018, pages 61-78, 2018. Google Scholar
  49. Lei Yu. A Formal Model of IEEE Floating Point Arithmetic. Archive of Formal Proofs, July 2013. , Formal proof development. URL: http://isa-afp.org/entries/IEEE_Floating_Point.html.
  50. Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic. Formalizing the LLVM Intermediate Representation for Verified Program Transformations. In Proc. of POPL, pages 427-440. ACM, 2012. URL: https://doi.org/10.1145/2103656.2103709.
  51. Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic. Formal Verification of SSA-based Optimizations for LLVM. SIGPLAN Not., 48(6):175-186, June 2013. URL: https://doi.org/10.1145/2499370.2462164.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact