skip to main content
10.1145/1159842.1159850acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
Article

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

Published: 17 September 2006 Publication History

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]
A. Abel, M. Benke, A. Bove, J. Hughes, and U. Norell. Verifying Haskell programs using constructive type theory. In Haskell'05, Tallinn, Estonia, 2005.
[2]
W. R. Bevier. Kit: A study in operating system verification. IEEE Transactions on Software Engineering, 15(11):1382--1396, 1989.
[3]
M. Bishop and L. Snyder. The transfer of information and authority in a protection system. In SOSP '79: Proceedings of the seventh ACM symposium on Operating systems principles, pages 45--54, New York, NY, USA, 1979. ACM Press.
[4]
T. Cattel. Modelization and verification of a multiprocessor realtime OS kernel. In Proceedings of FORTE '94, Bern, Switzerland, October 1994.
[5]
N. A. Danielsson, J. Hughes, P. Jansson, and J. Gibbons. Fast and loose reasoning is morally correct. In J. G. Morrisett and S. L. P. Jones, editors, POPL, pages 206--217. ACM, 2006.
[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]
B. Ford, M. Hibler, J. Lepreau, R. McGrath, and P. Tullmann. Interface and execution models in the Fluke kernel. In Proceedings of the 3rd USENIX Symposium on Operating Systems Design and Implementation, pages 101--115, New Orleans, LA, USA, Feb. 1999. USENIX.
[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]
T. Hallgren, M. P. Jones, R. Leslie, and A. Tolmach. A principled approach to operating system construction in Haskell. In ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, pages 116--128, New York, NY, USA, 2005. ACM Press.
[13]
W. L. Harrison and R. B. Kieburtz. The logic of demand in Haskell. Journal of Functional Programming, 15(6):837--891, 2005.
[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]
R. Kolanski and G. Klein. Formalising the L4 microkernel API. In B. Jay and J. Gudmundsson, editors, Computing: The Australasian Theory Symposium (CATS 06), volume 51 of Conferences in Research and Practice in Information Technology, pages 53--68, Hobart, Australia, Jan. 2006.
[20]
L4Ka Team. L4Ka::Pistachio kernel. http://l4ka.org/projects/pistachio/.
[21]
R. Levin, E. Cohen, W. Corwin, F. Pollack, and W. Wulf. Policy/ mechanism separation in Hydra. In SOSP '75: Proc. Fifth Symposium on Operating Systems Principles, pages 132--140, New York, NY, USA, 1975. ACM Press.
[22]
J. Liedtke. Address space sparsity and fine granularity. SIGOPS Oper. Syst. Rev., 29(1):87--90, 1995.
[23]
J. Liedtke. Towards real microkernels. Communications of the ACM, 39(9):70--77, Sept. 1996.
[24]
R. J. Lipton and L. Snyder. A linear time algorithm for deciding subject security. J. ACM, 24(3):455--464, 1977.
[25]
The M5 simulator system. http://m5.eecs.umich.edu/, 2006.
[26]
T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer Verlag, 2002.
[27]
J. Shapiro. Coyotos. www.coyotos.org, 2006.
[28]
W. Stoye. Message-based functional operating systems. Science of Computer Programming, 6(3):291--311, 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, and G. Back. Formal methods: a practical tool for OS implementors. In Proceedings of the Sixth Workshop on Hot Topics in Operating Systems, pages 20--25, 1997.
[32]
B.Walker, R. Kemmerer, and G. Popek. Specification and verification of the UCLA Unix security kernel. CACM, 23(2):118--131, 1980.
[33]
M. Wallace and C. Runciman. Lambdas in the liftshaft-functional programming and an embedded architecture. In FPCA '95: Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, pages 249--258, New York, NY, USA, 1995. ACM Press.

Cited By

View all
  • (2018)Total Haskell is reasonable CoqProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 201810.1145/3176245.3167092(14-27)Online publication date: 2018
  • (2018)Total Haskell is reasonable CoqProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3167092(14-27)Online publication date: 8-Jan-2018
  • (2014)Comprehensive formal verification of an OS microkernelACM Transactions on Computer Systems10.1145/256053732:1(1-70)Online publication date: 26-Feb-2014
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
Haskell '06: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell
September 2006
131 pages
ISBN:1595934898
DOI:10.1145/1159842
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 September 2006

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Haskell
  2. Isabelle/HOL
  3. executable specification
  4. formalisation
  5. monads
  6. operating systems
  7. rapid prototyping
  8. verification

Qualifiers

  • Article

Conference

ICFP06
Sponsor:

Acceptance Rates

Overall Acceptance Rate 57 of 143 submissions, 40%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)9
  • Downloads (Last 6 weeks)1
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2018)Total Haskell is reasonable CoqProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 201810.1145/3176245.3167092(14-27)Online publication date: 2018
  • (2018)Total Haskell is reasonable CoqProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3167092(14-27)Online publication date: 8-Jan-2018
  • (2014)Comprehensive formal verification of an OS microkernelACM Transactions on Computer Systems10.1145/256053732:1(1-70)Online publication date: 26-Feb-2014
  • (2014)Market mechanisms for managing datacenters with heterogeneous microarchitecturesACM Transactions on Computer Systems10.1145/254125832:1(1-31)Online publication date: 26-Feb-2014
  • (2012)Large-scale formal verification in practice: a process perspectiveProceedings of the 34th International Conference on Software Engineering10.5555/2337223.2337352(1002-1011)Online publication date: 2-Jun-2012
  • (2012)xmonad in Coq (experience report)ACM SIGPLAN Notices10.1145/2430532.236452347:12(131-136)Online publication date: 13-Sep-2012
  • (2012)Reducing memory reference energy with opportunistic virtual cachingACM SIGARCH Computer Architecture News10.1145/2366231.233719440:3(297-308)Online publication date: 9-Jun-2012
  • (2012)A first-order mechanistic model for architectural vulnerability factorACM SIGARCH Computer Architecture News10.1145/2366231.233719140:3(273-284)Online publication date: 9-Jun-2012
  • (2012)Side-channel vulnerability factorACM SIGARCH Computer Architecture News10.1145/2366231.233717240:3(106-117)Online publication date: 9-Jun-2012
  • (2012)xmonad in Coq (experience report)Proceedings of the 2012 Haskell Symposium10.1145/2364506.2364523(131-136)Online publication date: 13-Sep-2012
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media