Running the manual: an approach to high-assurance microkernel development

ABSTRACT

We propose a development methodology for designing and prototyping high assurance microkernels, and describe our application of it. The methodology is based on rapid prototyping and iterative refinement of the microkernel in a functional programming language. The prototype provides a precise semi-formal model, which is also combined with a machine simulator to form a reference implementation capable of executing real user-level software, to obtain accurate feedback on the suitability of the kernel API during development phases. We extract from the prototype a machine-checkable formal specification in higher-order logic, which may be used to verify properties of the design, and also results in corrections to the design without the need for full verification. We found the approach leads to productive, highly iterative development where formal modelling, semi-formal design and prototyping, and end use all contribute to a more mature final design in a shorter period of time.

REFERENCES

• 1: Andreas Abel , Marcin Benke , Ana Bove , John Hughes , Ulf Norell, Verifying haskell programs using constructive type theory, Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, p.62-73, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088348.1088355]
• 2: W. R. Bevier, Kit: A Study in Operating System Verification, IEEE Transactions on Software Engineering, v.15 n.11, p.1382-1396, November 1989 [doi>10.1109/32.41331]
• 3: Matt Bishop , Lawrence Snyder, The transfer of information and authority in a protection system, Proceedings of the seventh ACM symposium on Operating systems principles, p.45-54, December 10-12, 1979, Pacific Grove, California, United States [doi>10.1145/800215.806569]
• 4: Thierry Cattel, Modelization and verification of a multiprocessor realtime OS kernel, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, p.55-70, January 1995
• 5: Nils Anders Danielsson , John Hughes , Patrik Jansson , Jeremy Gibbons, Fast and loose reasoning is morally correct, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.206-217, January 11-13, 2006, Charleston, South Carolina, USA
• 6: G. Duval and J. Julliand. Modelling and verification of the RUBIS ?-kernel with SPIN. In SPIN95 Workshop Proceedings, 1995.
• 7: R. J. Feiertag and P. G. Neumann. The foundations of a provably secure operating system (PSOS). In AFIPS Conference Proceedings (NCC 79), pages 329--334, New York, NY, USA, June 1979.
• 8: Bryan Ford , Mike Hibler , Jay Lepreau , Roland McGrath , Patrick Tullmann, Interface and execution models in the Fluke kernel, Proceedings of the third symposium on Operating systems design and implementation, p.101-115, February 1999, New Orleans, Louisiana, United States
• 9: G. Fu. Design and implementation of an operating system in Standard ML. Master's thesis, Dept. of Information and Computer Sciences, University of Hawaii at Manoa, 1999. Available: http://www2. ics.hawaii.edu/~esb/prof/proj/hello/index.html.
• 10: M. Gargano, M. Hillebrand, D. Leinenbach, and W. Paul. On the correctness of operating system kernels. In Proc. 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'05), pages 1--16, Oxford, UK, 2005.
• 11: T. Hallgren, J. Hook, M. P. Jones, and R. B. Kieburtz. An overview of the Programatica ToolSet. High Confidence Software and Systems Conference, HCSS04, 2004.
• 12: Thomas Hallgren , Mark P. Jones , Rebekah Leslie , Andrew Tolmach, A principled approach to operating system construction in Haskell, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 13: William L. Harrison , Richard B. Kieburtz, The logic of demand in Haskell, Journal of Functional Programming, v.15 n.6, p.837-891, November 2005 [doi>10.1017/S0956796805005666]
• 14: Haskell hierarchical libraries. http://www.haskell.org/ghc/ docs/latest/html/libraries/index.html, 2006.
• 15: M. Hohmuth and H. Tews. The VFiasco approach for a verified operating system. In Proc. 2nd ECOOP Workshop on Programm Languages and Operating Systems, Glasgow, UK, Oct. 2005.
• 16: B. Huffman, J. Matthews, and P. White. Axiomatic constructor classes in Isabelle/HOLCF. In J. Hurd and T. F. Melham, editors, TPHOLs, volume 3603 of Lecture Notes in Computer Science, pages 147--162. Springer Verlag, 2005.
• 17: K. Karlsson. Nebula: a functional operating system. Technical Report LPM11, Laboratory for Programming Methodology, Chalmers University of Technology and University of Goteburg, 1981.
• 18: G. Klein and H. Tuch. Towards verified virtual memory in L4. In K. Slind, editor, TPHOLs Emerging Trends '04, Park City, Utah, USA, 2004.
• 19: Rafal Kolanski , Gerwin Klein, Formalising the L4 microkernel API, Proceedings of the 12th Computing: The Australasian Theroy Symposium, p.53-68, January 16-19, 2006, Hobart, Australia
• 20: L4Ka Team. L4Ka::Pistachio kernel. http://l4ka.org/projects/pistachio/.
• 21: R. Levin , E. Cohen , W. Corwin , F. Pollack , W. Wulf, Policy/mechanism separation in Hydra, Proceedings of the fifth ACM symposium on Operating systems principles, p.132-140, November 19-21, 1975, Austin, Texas, United States
• 22: Jochen Liedtke, Address space sparsity and fine granularity, ACM SIGOPS Operating Systems Review, v.29 n.1, p.87-90, Jan. 1995 [doi>10.1145/202453.202477]
• 23: Jochen Liedtke, Toward real microkernels, Communications of the ACM, v.39 n.9, p.70-77, Sept. 1996 [doi>10.1145/234215.234473]
• 24: R. J. Lipton , L. Snyder, A Linear Time Algorithm for Deciding Subject Security, Journal of the ACM (JACM), v.24 n.3, p.455-464, July 1977 [doi>10.1145/322017.322025]
• 25: The M5 simulator system. http://m5.eecs.umich.edu/, 2006.
• 26: Isabelle/HOL: a proof assistant for higher-order logic, Springer-Verlag, London, 2002
• 27: J. Shapiro. Coyotos. www.coyotos.org, 2006.
• 28: W Stoye, Message-based functional operating systems, Science of Computer Programming, v.6 n.3, p.291-311, May 1986
• 29: H. Tuch and G. Klein. A unified memory model for pointers. In Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pages 474--488, Montego Bay, Jamaica, Dec. 2005.
• 30: H. Tuch, G. Klein, and G. Heiser. OS verification - now! In Proceedings of the 10th Workshop on Hot Topics in Operating Systems, Santa Fe, NM, USA, June 2005.
• 31: P. Tullmann , J. Turner , J. McCorquodale , J. Lepreau , A. Chitturi , G. Back, Formal Methods: A Practical Tool for OS Implementors, Proceedings of the 6th Workshop on Hot Topics in Operating Systems (HotOS-VI), p.20, May 05-06, 1997
• 32: Bruce J. Walker , Richard A. Kemmerer , Gerald J. Popek, Specification and verification of the UCLA Unix security kernel, Communications of the ACM, v.23 n.2, p.118-131, Feb. 1980 [doi>10.1145/358818.358825]
• 33: Malcolm Wallace , Colin Runciman, Lambdas in the liftshaft—functional programming and an embedded architecture, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.249-258, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224213]

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability
          Subjects: Verification

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.3 Applications

General Terms:
Design, Documentation, Languages, Verification

Keywords:
Haskell, Isabelle/HOL, executable specification, formalisation, monads, operating systems, rapid prototyping, verification