{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:02:54Z","timestamp":1771700574187,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496732","type":"print"},{"value":"9783662496749","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_50","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"791-810","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication"],"prefix":"10.1007","author":[{"given":"Yongwang","family":"Zhao","sequence":"first","affiliation":[]},{"given":"David","family":"San\u00e1n","sequence":"additional","affiliation":[]},{"given":"Fuyuan","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"50_CR1","unstructured":"Lynxsecure separation kernel hypervisor. http:\/\/www.lynx.com\/products\/hypervisors\/ . Accessed July 2015"},{"key":"50_CR2","unstructured":"Sysgo pikeos hypervisor. https:\/\/www.sysgo.com\/products\/pikeos-rtos-and-virtualization-concept\/ . Accessed July 2015"},{"key":"50_CR3","unstructured":"Wind river vxworks 653 platform. http:\/\/www.windriver.com\/products\/vxworks\/certification-profiles\/ . Accessed July 2015"},{"key":"50_CR4","unstructured":"Wind river vxworks mils platform. http:\/\/www.windriver.com\/products\/vxworks\/certification-profiles\/ . Accessed July 2015"},{"key":"50_CR5","unstructured":"Aeronautical Radio Inc: ARINC Specification 653: Avionics Application Software Standard Interface, Part 1 - Required Services, November 2010"},{"issue":"6","key":"50_CR6","doi-asserted-by":"crossref","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"issue":"4","key":"50_CR7","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1002\/stvr.422","volume":"21","author":"P de la C\u00e1mara","year":"2011","unstructured":"de la C\u00e1mara, P., Castro, J.R., Gallardo, MdM, Merino, P.: Verification support for arinc-653-based avionics software. Softw. Test. Verification Reliab. 21(4), 267\u2013298 (2011)","journal-title":"Softw. Test. Verification Reliab."},{"key":"50_CR8","volume-title":"Formal Refinement for Operating System Kernels","author":"ID Craig","year":"2007","unstructured":"Craig, I.D.: Formal Refinement for Operating System Kernels. Springer, Heidelberg (2007). chap. 5"},{"key":"50_CR9","doi-asserted-by":"crossref","unstructured":"Dam, M., Guanciale, R., Khakpour, N., Nemati, H., Schwarz, O.: Formal verification of information flow security for a simple arm-based separation kernel. In: Proceedings of the 20th ACM Conference on Computer and Communications Security (CCS 2013). pp. 223\u2013234. ACM, New York, NY, USA (2013)","DOI":"10.1145\/2508859.2516702"},{"key":"50_CR10","unstructured":"Delange, J., Lec, L.: Pok, an arinc653-compliant operating system released under the bsd license. In: Proceedings of the 13th Real-Time Linux Workshop (2011)"},{"key":"50_CR11","unstructured":"Delange, J., Pautet, L., Kordon, F.: Modeling and validation of arinc653 architectures. In: Proceedings of Embedded Real-time Software and Systems Conference (ERTS 2010) (2010)"},{"issue":"5","key":"50_CR12","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/s10009-011-0195-9","volume":"13","author":"L Freitas","year":"2011","unstructured":"Freitas, L., McDermott, J.: Formal methods for security in the xenon hypervisor. Int. J. Softw. Tools Technol. Transf. 13(5), 463\u2013489 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"50_CR13","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1109\/TSE.2007.70772","volume":"34","author":"CL Heitmeyer","year":"2008","unstructured":"Heitmeyer, C.L., Archer, M.M., Leonard, E.I., McLean, J.D.: Applying formal methods to a certifiably secure software system. IEEE Trans. Softw. Eng. 34(1), 82\u201398 (2008)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"10","key":"50_CR14","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"50_CR15","doi-asserted-by":"crossref","unstructured":"Levin, T.E., Irvine, C.E., Weissman, C., Nguyen, T.D.: Analysis of three multilevel security architectures. In: Proceedings of the 2007 ACM Workshop on Computer Security Architecture (CSA 2007), pp. 37\u201346. ACM (2007)","DOI":"10.1145\/1314466.1314473"},{"key":"50_CR16","unstructured":"Masmano, M., Ripoll, I., Crespo, A., Metge, J.: Xtratum: a hypervisor for safety critical embedded systems. In: Proceedings of the 11th Real-Time Linux Workshop. pp. 263\u2013272 (2009)"},{"key":"50_CR17","doi-asserted-by":"crossref","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: Proceedings of IEEE Symposium on Security and Privacy (S&P 1988). pp. 177\u2013186. IEEE Computer Society (1988)","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"50_CR18","doi-asserted-by":"crossref","unstructured":"Millen, J.: 20 years of covert channel modeling and analysis. In: Proceedings of IEEE Symposium on Security and Privacy (S&P 1999). pp. 113\u2013114. IEEE (1999)","DOI":"10.1109\/SECPRI.1999.766906"},{"key":"50_CR19","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: Proceedings of IEEE Symposium on Security and Privacy (S&P 2013) (2013)","DOI":"10.1109\/SP.2013.35"},{"key":"50_CR20","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.) CPP 2012. LNCS, vol. 7679, pp. 126\u2013142. Springer, Heidelberg (2012)"},{"key":"50_CR21","unstructured":"National Security Agency: U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness (2007)"},{"key":"50_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.: Isabelle\/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, Berlin, Heidelberg (2002)"},{"key":"50_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-540-30108-0_14","volume-title":"Computer Security \u2013 ESORICS 2004","author":"D Oheimb von","year":"2004","unstructured":"von Oheimb, D.: Information flow control revisited: Noninfluence = Noninterference +Nonleakage. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 225\u2013243. Springer, Heidelberg (2004)"},{"key":"50_CR24","unstructured":"Oliveira Gomes, A.: Formal Specification of the ARINC 653 Architecture Using Circus. Master\u2019s thesis, University of York (2012)"},{"key":"50_CR25","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-1-4419-1539-9_10","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"RJ Richards","year":"2010","unstructured":"Richards, R.J.: Modeling and security analysis of a commercial real-time operating system kernel. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 301\u2013322. Springer, Heidelberg (2010)"},{"issue":"5","key":"50_CR26","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1067627.806586","volume":"15","author":"J Rushby","year":"1981","unstructured":"Rushby, J.: Design and verification of secure systems. ACM SIGOPS Oper. Syst. Rev. 15(5), 12\u201321 (1981)","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"50_CR27","unstructured":"Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical report, SRI International, Computer Science Laboratory (1992)"},{"issue":"1","key":"50_CR28","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5\u201319 (2003)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"50_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/978-3-319-12154-3_9","volume-title":"Verified Software: Theories, Tools and Experiments","author":"D San\u00e1n","year":"2014","unstructured":"San\u00e1n, D., Butterfield, A., Hinchey, M.: Separation kernel verification: the xtratum case study. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 133\u2013149. Springer, Heidelberg (2014)"},{"key":"50_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-14808-8_16","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"A Velykis","year":"2010","unstructured":"Velykis, A., Freitas, L.: Formal modelling of separation kernel components. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 230\u2013244. Springer, Heidelberg (2010)"},{"key":"50_CR31","doi-asserted-by":"crossref","unstructured":"Verbeek, F.F., Tverdyshev, S.S., etc.: Formal specification of a generic separation kernel. Archive of Formal Proofs (2014)","DOI":"10.1007\/978-3-319-17524-9_26"},{"key":"50_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/978-3-319-17524-9_26","volume-title":"NASA Formal Methods","author":"F Verbeek","year":"2015","unstructured":"Verbeek, F., Havle, O., Schmaltz, J., Tverdyshev, S., Blasum, H., Langenstein, B., Stephan, W., Wolff, B., Nemouchi, Y.: Formal API specification of the PikeOS separation kernel. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 375\u2013389. Springer, Heidelberg (2015)"},{"key":"50_CR33","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-1-4419-1539-9_6","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"MM Wilding","year":"2010","unstructured":"Wilding, M.M., Greve, D.A., Richards, R.J., Hardin, D.S.: Formal verification of partition management for the AAMP7G microprocessor. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 175\u2013191. Springer, Heidelberg (2010)"},{"key":"50_CR34","unstructured":"Zhao, Y.: Formal specification and verification of separation kernels: An overview. ArXiv e-prints (2015). http:\/\/arxiv.org\/abs\/1508.07066"},{"key":"50_CR35","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Yang, Z., Sanan, D., Liu, Y.: Event-based formalization of safety-critical operating system standards: An experience report on arinc 653 using event-b. In: Proceedings of the 26th IEEE International Symposium on Software Reliability Engineering (ISSRE 2015). pp. 281\u2013292. IEEE Computer Society (2015)","DOI":"10.1109\/ISSRE.2015.7381821"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_50","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T08:30:00Z","timestamp":1748853000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_50"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_50","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}