Abstract
PikeOS is an industrial operating system for safety and security critical applications in, for example, avionics and automotive contexts. A consortium of several European partners from industry and academia works on the certification of PikeOS up to at least Common Criteria EAL5+, with “+” being applying formal methods compliant up to EAL7. We have formalized the hardware independent security-relevant part of PikeOS that is to be used in a certification context. Over this model, intransitive noninterference has been proven. We present the model and the methodology used to create the model. All results have been formalized in the Isabelle/HOL theorem prover.
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
Kaiser, R., Wagner, S.: Evolution of the PikeOS microkernel. In: First International Workshop on Microkernels for Embedded Systems, p. 50 (2007)
Rushby, J.: Noninterference, transitivity, and channel-control security policies. SRI International, Computer Science Laboratory (1992)
van der Meyden, R.: What, indeed, is intransitive noninterference? In: Biskup, J., López, J. (eds.) Computer Security ESORICS 2007. LNCS, vol. 4734, pp. 235–250. Springer, Heidelberg (2007)
EURO-MILS: MILS architecture (2014). http://www.euromils.eu/downloads/2014-euro-mils-mils-architecture-white-paper.pdf
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pp. 207–220. ACM (2009)
Murray, T., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: from general purpose to a proof of information flow enforcement. In: 34th IEEE Symposium on Security and Privacy (2013)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic (2012)
Jacob, J.: On the derivation of secure components. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 242–247, May 1989
Mantel, H., Sudbrock, H.: Comparing countermeasures against interrupt-related covert channels in an information-theoretic framework. In: Proceedings of 20th IEEE Computer Security Foundations Symposium (CSF 2007), pp. 326–340, July 2007
Goguen, J.A., Meseguer, J.: Unwinding and inference control (1984)
Mantel, H.: Information flow control and applications - bridging a gap -. In: Oliveira, J., Zave, P. (eds.) Formal Methods for Increasing Software Productivity (FME 2001). LNCS, vol. 2021, pp. 153–172. Springer, Heidelberg (2001)
Roscoe, A.W., Goldsmith, M.H.: What is intransitive noninterference? In: Proceedings of the 12th IEEE Computer Security Foundations Workshop, pp. 228–238 (1999)
von Oheimb, D.: Information flow control revisited: Noninfluence = noninterference + nonleakage. In: Samarati, P., Ryan, P., Gollmann, D., Molva, R. (eds.) Computer Security - ESORICS 2004. LNCS, vol. 3193, 225th edn, p. 243. Springer, Heidelberg (2004)
Leslie, R.: Dynamic intransitive noninterference. In: IEEE International Symposium on Secure Software Engineering (2006)
Engelhardt, K., van der Meyden, R., Zhang, C.: Intransitive noninterference in nondeterministic systems. In: Proceedings of the 2012 ACM Conference on Computer and Communications Security, pp. 869–880. ACM (2012)
Haigh, J.T., Young, W.D.: Extending the noninterference version of MLS for SAT. IEEE Trans. Softw. Eng. 13(2), 141–150 (1987)
Whalen, M., Greve, D., Wagner, L.: Model checking information flow. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 381–428. Springer, US (2010)
Eggert, S., van der Meyden, R., Schnoor, H., Wilke, T.: The complexity of intransitive noninterference. In: 2011 IEEE Symposium on Security and Privacy (SP), pp. 196–211 (2011)
Murray, T., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: Hawblitzel, C., Miller, D. (eds.) Certified Programs and Proofs. LNCS, vol. 7679, pp. 126–142. Springer, Heidelberg (2012)
Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Verbeek, F. et al. (2015). Formal API Specification of the PikeOS Separation Kernel. In: Havelund, K., Holzmann, G., Joshi, R. (eds) NASA Formal Methods. NFM 2015. Lecture Notes in Computer Science(), vol 9058. Springer, Cham. https://doi.org/10.1007/978-3-319-17524-9_26
Download citation
DOI: https://doi.org/10.1007/978-3-319-17524-9_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-17523-2
Online ISBN: 978-3-319-17524-9
eBook Packages: Computer ScienceComputer Science (R0)