Document Open Access Logo

Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification

Authors Hrutvik Kanabar , Anthony C. J. Fox, Magnus O. Myreen

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.20.pdf
  • Filesize: 0.77 MB
  • 22 pages

Document Identifiers

Author Details

Hrutvik Kanabar
  • University of Kent, UK
Anthony C. J. Fox
  • Arm Limited, Cambridge, UK
Magnus O. Myreen
  • Chalmers University of Technology, Gothenburg, Sweden

Funding

  • Kanabar, Hrutvik: UK Research Institute in Verified Trustworthy Software Systems (VeTSS).
  • Myreen, Magnus O.: Swedish Foundation for Strategic Research.

Cite As Get BibTex

Hrutvik Kanabar, Anthony C. J. Fox, and Magnus O. Myreen. Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ITP.2022.20

Abstract

Machine-readable specifications for the Armv8 instruction set architecture have become publicly available as part of Arm’s release processes, providing an official and unambiguous source of truth for the semantics of Arm instructions. To date, compiler and machine code verification efforts have made use of unofficial theorem-proving-friendly specifications of Armv8, e.g. CakeML uses an L3-based specification. The validity of these verification efforts hinges upon their unofficial ISA specifications being valid with respect to the official Arm specification.
Leveraging the Sail language ecosystem, we bridge this validation gap by formally verifying that an L3-based specification simulates the official Arm specification using the HOL4 interactive theorem prover. We exercise this simulation by proving a novel compiler correctness result for CakeML with respect to Arm’s official specification of the Armv8.6 A-class instruction set.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
  • Hardware → Theorem proving and SAT solving
  • Software and its engineering → Domain specific languages
Keywords
  • Compiler verification
  • ISA specification
  • HOL4
  • interactive theorem proving

Metrics

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

Supplementary Materials

References

  1. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Shaked Flur, Kathryn E. Gray, Prashanth Mundkur, Robert M. Norton, Christopher Pulte, Alastair Reid, Peter Sewell, Ian Stark, and Mark Wassell. Detailed models of instruction set architectures: From pseudocode to formal semantics. In Proceedings of the Automated Reasoning Workshop, 2018. Two-page abstract. URL: http://www.cl.cam.ac.uk/~pes20/sail/2018-04-12-arw-paper.pdf.
  2. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS. Proceedings of the ACM on Programming Languages (PACMPL), 3(POPL), 2019. URL: https://doi.org/10.1145/3290384.
  3. Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, and Peter Sewell. Isla: Integrating full-scale ISA semantics and axiomatic concurrency models. In Computer Aided Verification (CAV), volume 12759 of Lecture Notes in Computer Science. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81685-8_14.
  4. Alasdair Armstrong, Neel Krishnaswami, Peter Sewell, and Mark Wassell. Formalisation of MiniSail in the Isabelle theorem prover. In Proceedings of the Automated Reasoning Workshop, 2018. Two-page abstract. URL: https://www.cl.cam.ac.uk/~pes20/sail/arw18_mpew2.pdf.
  5. Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter Sewell. Verified security for the Morello capability-enhanced prototype Arm architecture. In European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer, 2022. To appear. URL: http://www.cl.cam.ac.uk/~pes20/morello-proofs-esop2022.pdf.
  6. Christoph Baumann, Mats Näslund, Christian Gehrmann, Oliver Schwarz, and Hans Thorsen. A high assurance virtualization platform for ARMv8. In European Conference on Networks and Communications (EuCNC). IEEE, 2016. URL: https://doi.org/10.1109/EuCNC.2016.7561034.
  7. Brian Campbell and Ian Stark. Extracting behaviour from an executable instruction set model. In Formal Methods in Computer-Aided Design (FMCAD). IEEE, 2016. URL: https://doi.org/10.1109/FMCAD.2016.7886658.
  8. Adam Chlipala. Algorithmic checking of security arguments for microprocessors. In GOMACTech Conference, 2019. URL: https://apps.dtic.mil/sti/citations/AD1075652.
  9. Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. Kami: a platform for high-level parametric hardware specification and its modular verification. Proceedings of the ACM on Programming Languages, 1(ICFP), 2017. URL: https://doi.org/10.1145/3110268.
  10. Alessandro Coglio and Shilpi Goel. Adding 32-bit mode to the ACL2 model of the x86 ISA. In Workshop on the ACL2 Theorem Prover and Its Applications, volume 280 of EPTCS, 2018. URL: https://doi.org/10.4204/EPTCS.280.6.
  11. Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, and Adam Chlipala. Integration verification across software and hardware for a simple embedded system. In Programming Language Design and Implementation (PLDI). ACM, 2021. URL: https://doi.org/10.1145/3453483.3454065.
  12. Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. Modelling the ARMv8 architecture, operationally: concurrency and ISA. In Principles of Programming Languages (POPL). ACM, 2016. URL: https://doi.org/10.1145/2837614.2837615.
  13. Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. Mixed-size concurrency: ARM, POWER, C/C++11, and SC. In Principles of Programming Languages (POPL). ACM, 2017. URL: https://doi.org/10.1145/3009837.3009839.
  14. Anthony C. J. Fox. Formal specification and verification of ARM6. In Theorem Proving in Higher Order Logics (TPHOLs), volume 2758 of Lecture Notes in Computer Science. Springer, 2003. URL: https://doi.org/10.1007/10930755_2.
  15. Anthony C. J. Fox. Directions in ISA specification. In Interactive Theorem Proving (ITP), volume 7406 of Lecture Notes in Computer Science. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_23.
  16. Anthony C. J. Fox. Improved tool support for machine-code decompilation in HOL4. In Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_12.
  17. Anthony C. J. Fox and Magnus O. Myreen. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In Interactive Theorem Proving (ITP), volume 6172 of Lecture Notes in Computer Science. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_18.
  18. Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, and Ramana Kumar. Verified compilation of CakeML to multiple machine-code targets. In Certified Programs and Proofs (CPP). ACM, 2017. URL: https://doi.org/10.1145/3018610.3018621.
  19. Shilpi Goel and Warren A. Hunt Jr. Automated code proofs on a formal model of the X86. In Verified Software: Theories, Tools, Experiments (VSTTE), volume 8164 of Lecture Notes in Computer Science. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-54108-7_12.
  20. Shilpi Goel, Warren A. Hunt Jr., and Matt Kaufmann. Engineering a formal, executable x86 ISA simulator for software verification. In Provably Correct Systems, NASA Monographs in Systems and Software Engineering. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-48628-4_8.
  21. Shilpi Goel, Anna Slobodová, Rob Sumners, and Sol Swords. Verifying x86 instruction implementations. In Certified Programs and Proofs (CPP). ACM, 2020. URL: https://doi.org/10.1145/3372885.3373811.
  22. Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. In Microarchitecture (MICRO). ACM, 2015. URL: https://doi.org/10.1145/2830772.2830775.
  23. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Operating Systems Design and Implementation (OSDI). USENIX Association, 2016. URL: https://doi.org/10.5555/3026877.3026928.
  24. Roberto Guanciale, Hamed Nemati, Mads Dam, and Christoph Baumann. Provably secure memory isolation for linux on ARM. Journal of Computer Security, 24(6), 2016. URL: https://doi.org/10.3233/JCS-160558.
  25. Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, 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 Operating Systems Principles (SOSP). ACM, 2009. URL: https://doi.org/10.1145/1629575.1629596.
  26. Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1), 2014. URL: https://doi.org/10.1145/2560537.
  27. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: a verified implementation of ML. In Principles of Programming Languages (POPL). ACM, 2014. URL: https://doi.org/10.1145/2535838.2535841.
  28. Dirk Leinenbach and Thomas Santen. Verifying the Microsoft Hyper-V hypervisor with VCC. In Formal Methods (FM), volume 5850 of Lecture Notes in Computer Science. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-05089-3_51.
  29. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7), 2009. URL: https://doi.org/10.1145/1538788.1538814.
  30. Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. A secure and formally verified Linux KVM hypervisor. In Security and Privacy (SP). IEEE, 2021. URL: https://doi.org/10.1109/SP40001.2021.00049.
  31. Andreas Lindner, Roberto Guanciale, and Roberto Metere. TrABin: Trustworthy analyses of binaries. Science of Computer Programming, 174, 2019. URL: https://doi.org/10.1016/j.scico.2019.01.001.
  32. Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony C. J. Fox. Verified compilation on a verified processor. In Programming Language Design and Implementation (PLDI). ACM, 2019. URL: https://doi.org/10.1145/3314221.3314622.
  33. Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. Lem: reusable engineering of real-world semantics. In International Conference on Functional Programming (ICFP). ACM, 2014. URL: https://doi.org/10.1145/2628136.2628143.
  34. Magnus O. Myreen. Verified just-in-time compiler on x86. In Principles of Programming Languages (POPL). ACM, 2010. URL: https://doi.org/10.1145/1706299.1706313.
  35. Magnus O. Myreen. The CakeML project’s quest for ever stronger correctness theorems (invited paper). In Interactive Theorem Proving (ITP), volume 193 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.1.
  36. Magnus O. Myreen and Jared Davis. A verified runtime for a verified theorem prover. In Interactive Theorem Proving (ITP), volume 6898 of Lecture Notes in Computer Science. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22863-6_20.
  37. Magnus O. Myreen and Michael J. C. Gordon. Verified LISP implementations on ARM, x86 and PowerPC. In Theorem Proving in Higher Order Logics (TPHOLs), volume 5674 of Lecture Notes in Computer Science. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_25.
  38. Magnus O. Myreen and Scott Owens. Proof-producing translation of higher-order logic into pure and stateful ML. Journal of Functional Programming (JFP), 24(2-3), 2014. URL: https://doi.org/10.1017/S0956796813000282.
  39. Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, and Swen Jacobs. Validation of abstract side-channel models for computer architectures. In Computer Aided Verification (CAV), volume 12224 of Lecture Notes in Computer Science. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53288-8_12.
  40. Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony C. J. Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell. Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. In Security and Privacy (SP). IEEE, 2020. URL: https://doi.org/10.1109/SP40000.2020.00055.
  41. Scott Owens, Peter Böhm, Francesco Zappa Nardelli, and Peter Sewell. Lem: A lightweight tool for heavyweight semantics. In Interactive Theorem Proving (ITP), volume 6898 of Lecture Notes in Computer Science. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22863-6_27.
  42. Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. Proceedings of the ACM on Programming Languages, 2(POPL), 2018. URL: https://doi.org/10.1145/3158107.
  43. Alastair Reid. Arm releases machine readable architecture specification. URL: https://alastairreid.github.io/ARM-v8a-xml-release/.
  44. Alastair Reid. Arm v8.3 machine readable specification released. URL: https://alastairreid.github.io/arm-v8_3/.
  45. Alastair Reid. Arm’s architecture specification language. URL: https://alastairreid.github.io/specification_languages/.
  46. Alastair Reid. ASL lexical syntax. URL: https://alastairreid.github.io/using-asli/.
  47. Alastair Reid. Dissecting Arm’s machine readable specification. URL: https://alastairreid.github.io/dissecting-Arm-MRA/.
  48. Alastair Reid. Formal validation of the Arm v8-M specification. URL: https://alastairreid.github.io/validating-specs/.
  49. Alastair Reid. Limitations of ISA-Formal. URL: https://alastairreid.github.io/isa-formal-limitations/.
  50. Alastair Reid. Using ASLi with Arm’s v8.6-A ISA specification. URL: https://alastairreid.github.io/asl-lexical-syntax/.
  51. Alastair Reid. Verifying against the official Arm specification. URL: https://alastairreid.github.io/using-armarm/.
  52. Alastair Reid. What can you do with an ISA specification? URL: https://alastairreid.github.io/uses-for-isa-specs/.
  53. Alastair Reid. Trustworthy specifications of ARMregistered v8-A and v8-M system level architecture. In Formal Methods in Computer-Aided Design (FMCAD). IEEE, 2016. URL: https://doi.org/10.1109/FMCAD.2016.7886675.
  54. Alastair Reid. Who guards the guards? Formal validation of the Arm v8-M architecture specification. Proceedings of the ACM on Programming Languages (PACMPL), 1(OOPSLA), 2017. URL: https://doi.org/10.1145/3133912.
  55. Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi. End-to-end verification of processors with ISA-Formal. In Computer Aided Verification (CAV), volume 9780 of Lecture Notes in Computer Science. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_3.
  56. Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell. Islaris: verification of machine code against authoritative ISA semantics. In Programming Language Design and Implementation (PLDI). ACM, 2022. URL: https://doi.org/10.1145/3519939.3523434.
  57. Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein. Translation validation for a verified OS kernel. In Programming Language Design and Implementation (PLDI). ACM, 2013. URL: https://doi.org/10.1145/2491956.2462183.
  58. Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter Neumann. An introduction to CHERI. Technical Report UCAM-CL-TR-941, University of Cambridge, Computer Laboratory, September 2019. URL: https://doi.org/10.48456/tr-941.
  59. Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, Graeme Barnes, David Chisnall, Jessica Clarke, Brooks Davis, Lee Eisen, Nathaniel Wesley Filardo, Richard Grisenthwaite, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert Norton, Alexander Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan Xia. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8). Technical Report UCAM-CL-TR-951, University of Cambridge, Computer Laboratory, October 2020. URL: https://doi.org/10.48456/tr-951.
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