Abstract
Separation kernels are key components in embedded applications. Their small size and widespread use in high-integrity environments make them good targets for formal modelling and verification. We summarise results from the mechanisation of a separation kernel scheduler using the Z/Eves theorem prover. We concentrate on key data structures to model scheduler operations. The results are part of an experiment in a Grand Challenge in software verification, as part of a pilot project in verified OS kernels. The project aims at creating a mechanised formal model of kernel components that gets refined to code. This provides a set of reusable components, proof strategies, and general lemmas. Important findings about properties and requirements are also discussed.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barden, R., et al.: Z in Practice. Prentice Hall, Englewood Cliffs (1994)
Bicarregui, J., et al.: The verified software repository. Formal Aspects of Computing 18(2), 143–151 (2006)
Berry, R.: A free real-time operating system (FreeRTOS)
Boerger, E.: Refinement of distributed agents. In: Dagstuhl Seminar 09381 (2009)
Cohen, E., et al.: VCC: A practical system for verifying concurrent C. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)
Craig, I.D.: Formal Refinement for Operating System Kernels. Springer, Heidelberg (2007)
Freitas, L.: Proving Theorems with Z/Eves. T. Report, University of Kent (2004)
Freitas, L., et al.: Posix and the verification grand challenge: A roadmap. In: 13th ICECCS, pp. 153–162. IEEE Computer Society, Los Alamitos (2008)
Freitas, L.: Extended Z mathematical toolkit – Verified Software Repository. Technical Report CRG13, University of York (2008)
Freitas, L.: Mechanising data-types for kernel design in Z. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol. 5902, pp. 186–203. Springer, Heidelberg (2009)
Hall, A., Chapman, R.: Correctness by Construction: Developing a Commercial Secure System. IEEE Software 19(1), 18–25 (2002)
Jones, C., Woodcock, J. (eds.): Formal Aspects of Computing: Special Issue on the Mondex Verification, vol. 20(1). Springer, Heidelberg (2008)
Klein, G., et al.: seL4: Formal verification of an OS kernel. In: 22nd ACM Symposium on Operating Systems Principles (SOSP). ACM, New York (2009)
McDermott, J., Freitas, L.: Formal security policy of Xenon. In: FMSE (2008)
Rushby, J.M.: Design and verification of secure systems. ACM SIGOPS Operating Systems Review 15(5), 12–21 (1981)
Saaltink, M.: Z/Eves 2.2 User’s Guide. Technical report, ORA (1999)
Saaltink, M.: Z/Eves 2.2 Mathematical Toolkit. Technical report, ORA (2003)
SKPP: U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness, v.1.0.3. National Security Agency (June 2007)
Velykis, A.: Formal modelling of separation kernels. Master’s thesis, Department of Computer Science, University of York (2009)
Woodcock, J., Davies, J.: Using Z. Prentice-Hall, Englewood Cliffs (1996)
Woodcock, J.: First steps in the verified software grand challenge. IEEE Computer 39(10), 57–64 (2006)
Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal Methods: Practice and Experience. ACM Computing Surveys (2009) (in Press)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Velykis, A., Freitas, L. (2010). Formal Modelling of Separation Kernel Components. In: Cavalcanti, A., Deharbe, D., Gaudel, MC., Woodcock, J. (eds) Theoretical Aspects of Computing – ICTAC 2010. ICTAC 2010. Lecture Notes in Computer Science, vol 6255. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14808-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-14808-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14807-1
Online ISBN: 978-3-642-14808-8
eBook Packages: Computer ScienceComputer Science (R0)