{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:56:35Z","timestamp":1762865795044},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214363"},{"type":"electronic","value":"9783642214370"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_19","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T07:33:16Z","timestamp":1308382396000},"page":"231-245","source":"Crossref","is-referenced-by-count":18,"title":["Formally Verifying Isolation and Availability in an Idealized Model of Virtualization"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Gustavo","family":"Betarte","sequence":"additional","affiliation":[]},{"given":"Juan Diego","family":"Campo","sequence":"additional","affiliation":[]},{"given":"Carlos","family":"Luna","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","volume-title":"10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010","author":"E. Alkassar","year":"2010","unstructured":"Alkassar, E., Cohen, E., Hillebrand, M., Kovalev, M., Paul, W.: Verifying shadow page table algorithms. In: Bloem, R., Sharygina, N. (eds.) 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010. IEEE CS, Switzerland (2010)"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-15057-9_3","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Alkassar","year":"2010","unstructured":"Alkassar, E., Hillebrand, M., Paul, W., Petrova, E.: Automated Verification of a Small Hypervisor. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 40\u201354. Springer, Heidelberg (2010)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-15057-9_5","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Alkassar","year":"2010","unstructured":"Alkassar, E., Paul, W., Starostin, A., Tsyban, A.: Pervasive verification of an os microkernel: Inline assembly, memory consumption, concurrent devices. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 71\u201385. Springer, Heidelberg (2010)"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/10930755_22","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Andronick","year":"2003","unstructured":"Andronick, J., Chetali, B., Ly, O.: Using Coq to Verify Java Card Applet Isolation Properties. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 335\u2013351. Springer, Heidelberg (2003)"},{"key":"19_CR5","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"15","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.: Stack-based access control for secure information flow. Journal of Functional Programming\u00a015, 131\u2013177 (2005); Special Issue on Language-Based Security","journal-title":"Journal of Functional Programming"},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1145\/945445.945462","volume-title":"SOSP 2003: Proceedings of the Nineteenth ACM Symposium on Operating Systems Principles","author":"P. Barham","year":"2003","unstructured":"Barham, P., Dragovic, B., Fraser, K., Hand, S., Harris, T., Ho, A., Neugebauer, R., Pratt, I., Warfield, A.: Xen and the art of virtualization. In: SOSP 2003: Proceedings of the Nineteenth ACM Symposium on Operating Systems Principles, pp. 164\u2013177. ACM Press, New York (2003)"},{"issue":"6","key":"19_CR7","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"M.R. Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. Journal of Computer Security\u00a018(6), 1157\u20131210 (2010)","journal-title":"Journal of Computer Security"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11813040_6","volume-title":"FM 2006: Formal Methods","author":"E. Cohen","year":"2006","unstructured":"Cohen, E.: Validating the microsoft hypervisor. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, p. 81. Springer, Heidelberg (2006)"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-540-87873-5_11","volume-title":"Verified Software: Theories, Tools, Experiments","author":"D. Elkaduwe","year":"2008","unstructured":"Elkaduwe, D., Klein, G., Elphinstone, K.: Verified protection model of the seL4 microkernel. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 99\u2013114. Springer, Heidelberg (2008)"},{"unstructured":"Garfinkel, T., Warfield, A.: What virtualization can do for security. login: The USENIX Magazine\u00a032 (December 2007)","key":"19_CR10"},{"key":"19_CR11","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/MC.1974.6323581","volume":"7","author":"R.P. Goldberg","year":"1974","unstructured":"Goldberg, R.P.: Survey of virtual machine research. IEEE Computer Magazine\u00a07, 34\u201345 (1974)","journal-title":"IEEE Computer Magazine"},{"unstructured":"Greve, D., Wilding, M., Mark Van Eet, W.: A separation kernel formal security policy. In: Proc. Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (2003)","key":"19_CR12"},{"key":"19_CR13","first-page":"346","volume-title":"Proceedings of the 13th ACM Conference on Computer and Communications Security, CCS 2006","author":"C.L. Heitmeyer","year":"2006","unstructured":"Heitmeyer, C.L., Archer, M., Leonard, E.I., McLean, J.: Formal specification and verification of data separation in a separation kernel for an embedded system. In: Proceedings of the 13th ACM Conference on Computer and Communications Security, CCS 2006, pp. 346\u2013355. ACM, New York (2006)"},{"issue":"6","key":"19_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G. Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. Communications of the ACM (CACM)\u00a053(6), 107\u2013115 (2010)","journal-title":"Communications of the ACM (CACM)"},{"issue":"1","key":"19_CR15","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/s12046-009-0002-4","volume":"34","author":"G. Klein","year":"2009","unstructured":"Klein, G.: Operating system verification \u2013 an overview. S\u0101dhan\u0101\u00a034(1), 27\u201369 (2009)","journal-title":"S\u0101dhan\u0101"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1007\/978-3-642-05089-3_51","volume-title":"FM 2009: Formal Methods","author":"D. Leinenbach","year":"2009","unstructured":"Leinenbach, D., Santen, T.: Verifying the microsoft hyper-V hypervisor with VCC. In: Cavalcanti, A., Dams, D. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 806\u2013809. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Martin, W., White, P., Taylor, F.S., Goldberg, A.: Formal construction of the mathematically analyzed separation kernel. In: The Fifteenth IEEE International Conference on Automated Software Engineering (2000)","key":"19_CR17","DOI":"10.1109\/ASE.2000.873658"},{"key":"19_CR18","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., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol.\u00a03193, pp. 225\u2013243. Springer, Heidelberg (2004)"},{"issue":"3","key":"19_CR19","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10207-004-0057-5","volume":"4","author":"D. Oheimb von","year":"2005","unstructured":"von Oheimb, D., Lotz, V., Walter, G.: Analyzing SLE 88 memory management security using Interacting State Machines. International Journal of Information Security\u00a04(3), 155\u2013171 (2005)","journal-title":"International Journal of Information Security"},{"unstructured":"Rushby, J.M.: Noninterference, Transitivity, and Channel-Control Security Policies. Technical Report CSL-92-02, SRI International (1992)","key":"19_CR20"},{"unstructured":"The Coq\u00a0Development Team. The Coq Proof Assistant Reference Manual \u2013 Version V8.2 (2008)","key":"19_CR21"},{"unstructured":"Tews, H., Weber, T., Poll, E., van Eekelen, M.C.J.D.: Formal Nova interface specification. Technical Report ICIS\u2013R08011, Radboud University Nijmegen, Robin deliverable D12 (May 2008)","key":"19_CR22"},{"key":"19_CR23","first-page":"99","volume-title":"Proceedings of PLDI 2010","author":"J. Yang","year":"2010","unstructured":"Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Proceedings of PLDI 2010, pp. 99\u2013110. ACM, New York (2010)"}],"container-title":["Lecture Notes in Computer Science","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,29]],"date-time":"2019-03-29T02:16:20Z","timestamp":1553825780000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}