{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T10:04:20Z","timestamp":1767261860827,"version":"3.41.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175232"},{"type":"electronic","value":"9783319175249"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17524-9_26","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"375-389","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Formal API Specification of the PikeOS Separation Kernel"],"prefix":"10.1007","author":[{"given":"Freek","family":"Verbeek","sequence":"first","affiliation":[]},{"given":"Oto","family":"Havle","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Schmaltz","sequence":"additional","affiliation":[]},{"given":"Sergey","family":"Tverdyshev","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Blasum","sequence":"additional","affiliation":[]},{"given":"Bruno","family":"Langenstein","sequence":"additional","affiliation":[]},{"given":"Werner","family":"Stephan","sequence":"additional","affiliation":[]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[]},{"given":"Yakoub","family":"Nemouchi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"26_CR1","unstructured":"Kaiser, R., Wagner, S.: Evolution of the PikeOS microkernel. In: First International Workshop on Microkernels for Embedded Systems, p. 50 (2007)"},{"key":"26_CR2","unstructured":"Rushby, J.: Noninterference, transitivity, and channel-control security policies. SRI International, Computer Science Laboratory (1992)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-540-74835-9_16","volume-title":"Computer Security ESORICS 2007","author":"R van der Meyden","year":"2007","unstructured":"van der Meyden, R.: What, indeed, is intransitive noninterference? In: Biskup, J., L\u00f3pez, J. (eds.) Computer Security ESORICS 2007. LNCS, vol. 4734, pp. 235\u2013250. Springer, Heidelberg (2007)"},{"key":"26_CR4","unstructured":"EURO-MILS: MILS architecture (2014). http:\/\/www.euromils.eu\/downloads\/2014-euro-mils-mils-architecture-white-paper.pdf"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"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\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1109\/SP.2013.35"},{"key":"26_CR7","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic (2012)"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Jacob, J.: On the derivation of secure components. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 242\u2013247, May 1989","DOI":"10.1109\/SECPRI.1989.36298"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"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\u2013340, July 2007","DOI":"10.1109\/CSF.2007.14"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Unwinding and inference control (1984)","DOI":"10.1109\/SP.1984.10019"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-45251-6_9","volume-title":"Formal Methods for Increasing Software Productivity (FME 2001)","author":"H Mantel","year":"2001","unstructured":"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\u2013172. Springer, Heidelberg (2001)"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Goldsmith, M.H.: What is intransitive noninterference? In: Proceedings of the 12th IEEE Computer Security Foundations Workshop, pp. 228\u2013238 (1999)","DOI":"10.1109\/CSFW.1999.779776"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","first-page":"243","volume-title":"Computer Security - ESORICS 2004","author":"D von Oheimb","year":"2004","unstructured":"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)","edition":"225"},{"key":"26_CR14","unstructured":"Leslie, R.: Dynamic intransitive noninterference. In: IEEE International Symposium on Secure Software Engineering (2006)"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"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\u2013880. ACM (2012)","DOI":"10.1145\/2382196.2382288"},{"issue":"2","key":"26_CR16","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1109\/TSE.1987.226478","volume":"13","author":"JT Haigh","year":"1987","unstructured":"Haigh, J.T., Young, W.D.: Extending the noninterference version of MLS for SAT. IEEE Trans. Softw. Eng. 13(2), 141\u2013150 (1987)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"26_CR17","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-1-4419-1539-9_13","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"M Whalen","year":"2010","unstructured":"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\u2013428. Springer, US (2010)"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"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\u2013211 (2011)","DOI":"10.1109\/SP.2011.30"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-35308-6_12","volume-title":"Certified Programs and Proofs","author":"T Murray","year":"2012","unstructured":"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\u2013142. Springer, Heidelberg (2012)"},{"issue":"1","key":"26_CR20","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"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)","journal-title":"ACM Trans. Comput. Syst."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T23:26:20Z","timestamp":1747869980000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}