Formal Specification Of A Generic Separation Kernel
Creators: name: Verbeek, Freek
name: Schmaltz, Julien
name: Tverdyshev, Sergey
name: Havle, Oto
name: Blasum, Holger
name: Langenstein, Bruno
name: Stephan, Werner
name: Feliachi, Abderrahmane
name: Nemouchi, Yakoub
name: Wolff, Burkhart
Publisher: name: Zenodo
Year: 2014
Subjects: separation kernel with control
formal model
IPC
instantiation
events
Isabelle/HOL

description: We introduce a theory of intransitive non-interference for separation kernels with control. We show that it can be instantiated for a simple API consisting of IPC and events.
description: {"references": ["Rushby, J.: Design and verification of secure systems. In: ACM SIGOPS Operating Systems Review. Volume 15., ACM (1981) 12\u201321", "Kaiser, R.,Wagner, S.: Evolution of the PikeOS microkernel. In: First International Workshop on Microkernels for Embedded Systems. (2007) 50", "Brygier, J., Fuchsen, R., Blasum, H.: PikeOS: Safe and secure virtualization in a separation microkernel. Technical report, Technical report, SYSGO (2009)", "Rushby, J.: Noninterference, transitivity, and channel-control security policies. SRI International, Computer Science Laboratory (1992)", "Murray, T., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: Certified Programs and Proofs. Springer (2012) 126\u2013142", "Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higherorder logic. Springer-Verlag (2012)", "Kamm\u00fcller, F.: Modular reasoning in isabelle. In McAllester, D., ed.: Automated Deduction - CADE-17. Volume 1831 of Lecture Notes in Computer Science. Springer Berlin Heidelberg (2000) 99\u2013114", "Goguen, J.A., Meseguer, J.: Unwinding and inference control. (1984)", "Haigh, J.T., Young, W.D.: Extending the noninterference version of MLS for SAT. IEEE Trans. Softw. Eng. 13(2) (February 1987) 141\u2013150", "Roscoe, A.W., Goldsmith, M.H.: What is intransitive noninterference? In: In Proc. of the 12th IEEE Computer Security Foundations Workshop. (1999) 228\u2013238", "van der Meyden, R.: What, indeed, is intransitive noninterference? In Biskup, J., Lpez, J., eds.: Computer Security ESORICS 2007. Volume 4734 of Lecture Notes in Computer Science. Springer Berlin Heidelberg (2007) 235\u2013250", "van der Meyden, R., Zhang, C.: A comparison of semantic models for noninterference. Theoretical Computer Science 411(47) (2010) 4123\u20134147", "Greve, D., Wilding, M., Vanfleet, W.M.: A separation kernel formal security policy. In: Fourth International Workshop on the ACL2 Prover and Its Applications (ACL2-2003). (2003)", "Alves-Foss, J., Taylor, C.: An analysis of the GWV security policy. In: Fifth International Workshop on the ACL2 Prover and its Applications (ACL2-2004). (2004)", "Gorrieri, R., Vernali, M.: On intransitive non-interference in some models of concurrency. In: Foundations of security analysis and design VI. Springer (2011) 125\u2013151", "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, ACM (2012) 869\u2013880", "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, ACM (2009) 207\u2013220"]}