Document Open Access Logo

All Watched Over by Machines of Loving Grace

Author Dominic P. Mulligan

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2022.1.pdf
  • Filesize: 0.77 MB
  • 23 pages

Document Identifiers

Author Details

Dominic P. Mulligan
  • Automated Reasoning Group, Amazon Web Services, Cambridge, UK

Acknowledgements

We would like to thank Nick Spinale for many insightful conversations regarding Supervisionary, and Nathan Chong and two anonymous referees for their helpful feedback on earlier drafts of this paper.

Cite AsGet BibTex

Dominic P. Mulligan. All Watched Over by Machines of Loving Grace. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 1:1-1:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TYPES.2022.1

Abstract

Modern operating systems are typically built around a trusted system component called the kernel which amongst other things is charged with enforcing system-wide security policies. Crucially, this component must be kept isolated from untrusted software at all times, which is facilitated by exploiting machine-oriented notions of separation: private memories, privilege levels, and similar. Modern proof-assistants are typically built around a trusted system component called the kernel which is charged with enforcing system-wide soundness. Crucially, this component must be kept isolated from untrusted automation at all times, which is facilitated by exploiting programming-language notions of separation: module-private data structures, type-abstraction, and similar. Whilst markedly different in purpose, in some essential ways operating system and proof-assistant kernels are tasked with the same job, namely enforcing system-wide invariants in the face of unbridled interaction with untrusted code. Yet the mechanisms through which the two types of kernel protect themselves are significantly different. In this paper, we introduce Supervisionary, the kernel of a programmable proof-checking system for Gordon’s HOL, organised in a manner more reminiscent of an operating system than a typical LCF-style proof-checker. Supervisionary’s kernel executes at a relative level of privilege compared to untrusted automation, with trusted and untrusted system components communicating across a limited system call boundary. Kernel objects, managed on behalf of user-space by Supervisionary, are referenced by handles and are passed back-and-forth by system calls. Unusually, Supervisionary has no "metalanguage" in the LCF sense, as the language used to implement the kernel, and the language used to implement automation, need not be the same. Any programming language can be used to implement automation for Supervisionary, providing the resulting binary respects the kernel calling convention and binary interface, with no risk to system soundness. Lastly, Supervisionary allows arbitrary programming languages to be endowed with facilities for proof-checking. Indeed, the handles that Supervisionary uses to denote kernel objects may be thought of as an extremely expressive form of capability - in the computer security sense of that word - and can potentially be used to enforce fine-grained correctness and security properties of programs at runtime.

Subject Classification

ACM Subject Classification
  • Theory of computation → Higher order logic
  • Theory of computation → Automated reasoning
  • Theory of computation → Logic and verification
  • Software and its engineering → Operating systems
Keywords
  • Proof assistant design
  • operating systems
  • HOL
  • LCF
  • Supervisionary
  • system description
  • capabilities

Metrics

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

Supplementary Materials

References

  1. Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell. Candle: A verified implementation of HOL light. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 237 of LIPIcs, pages 3:1-3:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.3.
  2. Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo. The Nuprl open logical environment. In David A. McAllester, editor, Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, volume 1831 of Lecture Notes in Computer Science, pages 170-176. Springer, 2000. URL: https://doi.org/10.1007/10721959_12.
  3. Arm Holdings, Ltd. AArch64 virtual memory system architecture. URL: https://developer.arm.com/documentation/ddi0406/b/System-Level-Architecture/Virtual-Memory-System-Architecture--VMSA-, 2023. Accessed 1^st May 2023.
  4. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. The Matita interactive theorem prover. In Nikolaj S. Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 64-69. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_7.
  5. Edwin C. Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program., 23(5):552-593, 2013. URL: https://doi.org/10.1017/S095679681300018X.
  6. Edwin C. Brady. Idris 2: Quantitative Type Theory in practice. In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference), volume 194 of LIPIcs, pages 9:1-9:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.9.
  7. Alonzo Church. A formulation of the Simple Theory of Types. J. Symb. Log., 5(2):56-68, 1940. URL: https://doi.org/10.2307/2266170.
  8. de Ng Dick Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Studies in logic and the foundations of mathematics, 133:375-388, 1972. Google Scholar
  9. D. R. Engler, M. F. Kaashoek, and J. O'Toole. Exokernel: an operating system architecture for application-level resource management. In SOSP '95: Proceedings of the fifteenth ACM symposium on Operating systems principles, pages 251-266, New York, NY, USA, 1995. ACM. URL: https://doi.org/10.1145/224056.224076.
  10. Michael J. C. Gordon. Introduction to the HOL system. In Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA, pages 2-3. IEEE Computer Society, 1991. Google Scholar
  11. Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. Springer, 1979. URL: https://doi.org/10.1007/3-540-09724-4.
  12. Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and J. F. Bastien. Bringing the web up to speed with WebAssembly. In Albert Cohen and Martin T. Vechev, editors, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, pages 185-200. ACM, 2017. URL: https://doi.org/10.1145/3062341.3062363.
  13. Norman Hardy. KeyKOS architecture. ACM SIGOPS Oper. Syst. Rev., 19(4):8-25, 1985. URL: https://doi.org/10.1145/858336.858337.
  14. John Harrison. HOL light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 60-66. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_4.
  15. Gérard P. Huet and Hugo Herbelin. 30 years of research and development around Coq. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 249-250. ACM, 2014. URL: https://doi.org/10.1145/2535838.2537848.
  16. Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In Chris Hankin and Dave Schmidt, editors, Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, pages 14-26. ACM, 2001. URL: https://doi.org/10.1145/360204.375719.
  17. Ralf Jung. Understanding and evolving the Rust programming language. PhD thesis, Saarland University, Saarbrücken, Germany, 2020. URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/29647.
  18. Stephen Kell, Dominic P. Mulligan, and Peter Sewell. The missing link: explaining ELF static linking, semantically. In Eelco Visser and Yannis Smaragdakis, editors, Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, pages 607-623. ACM, 2016. URL: https://doi.org/10.1145/2983990.2983996.
  19. 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 Jeanna Neefe Matthews and Thomas E. Anderson, editors, Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009, pages 207-220. ACM, 2009. URL: https://doi.org/10.1145/1629575.1629596.
  20. Anil Madhavapeddy, Richard Mortier, Charalampos Rotsos, David Scott, Balraj Singh, Thomas Gazagnaire, Steven Smith, Steven Hand, and Jon Crowcroft. Unikernels: Library operating systems for the cloud. SIGARCH Comput. Archit. News, 41(1):461-472, March 2013. URL: https://doi.org/10.1145/2490301.2451167.
  21. Anil Madhavapeddy, Richard Mortier, Charalampos Rotsos, David Scott, Balraj Singh, Thomas Gazagnaire, Steven Smith, Steven Hand, and Jon Crowcroft. Unikernels: Library operating systems for the cloud. In Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '13, pages 461-472, New York, NY, USA, 2013. Association for Computing Machinery. URL: https://doi.org/10.1145/2451116.2451167.
  22. Robin Milner, Mads Tofte, and Robert Harper. Definition of Standard ML. MIT Press, 1990. Google Scholar
  23. Georg Moser and Richard Zach. The epsilon calculus (tutorial). In Matthias Baaz and Johann A. Makowsky, editors, Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt Gödel Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings, volume 2803 of Lecture Notes in Computer Science, page 455. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45220-1_36.
  24. George C. Necula. Proof-carrying code. In Henk C. A. van Tilborg and Sushil Jajodia, editors, Encyclopedia of Cryptography and Security, 2nd Ed, pages 984-986. Springer, 2011. URL: https://doi.org/10.1007/978-1-4419-5906-5_864.
  25. 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 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 2020, pages 1003-1020. IEEE, 2020. URL: https://doi.org/10.1109/SP40000.2020.00055.
  26. Ulf Norell. Interactive programming with dependent types. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 1-2. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500610.
  27. Lawrence C. Paulson, Tobias Nipkow, and Makarius Wenzel. From LCF to Isabelle/HOL. Form. Asp. Comput., 31(6):675-698, December 2019. URL: https://doi.org/10.1007/s00165-019-00492-1.
  28. Robert Pollack. How to believe a machine-checked proof. In Twenty Five Years of Constructive Type Theory. Oxford University Press, October 1998. Google Scholar
  29. S. A. Rajunas, Norman Hardy, Allen C. Bomberger, William S. Frantz, and Charles R. Landau. Security in KeyKOStrademark. In Proceedings of the 1986 IEEE Symposium on Security and Privacy, Oakland, California, USA, April 7-9, 1986, pages 78-85. IEEE Computer Society, 1986. URL: https://doi.org/10.1109/SP.1986.10000.
  30. John C. Reynolds. Separation Logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55-74. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  31. Amitabha Sanyal and Uday P. Khedker. Garbage collection techniques. In Y. N. Srikant and Priti Shankar, editors, The Compiler Design Handbook: Optimizations and Machine Code Generation, Second Edition, page 6. CRC Press, 2007. Google Scholar
  32. Jonathan S. Shapiro and Norman Hardy. EROS: A principle-driven operating system from the ground up. IEEE Softw., 19(1):26-33, 2002. URL: https://doi.org/10.1109/52.976938.
  33. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 28-32. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  34. Antonis Stampoulis and Zhong Shao. VeriML: typed computation of logical terms inside a language with effects. In Paul Hudak and Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 333-344. ACM, 2010. URL: https://doi.org/10.1145/1863543.1863591.
  35. Andrew S. Tanenbaum and Albert S. Woodhull. Operating systems - design and implementation, 3rd Edition. Pearson Education, 2006. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact