{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T20:36:16Z","timestamp":1759091776835},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2011,5,21]],"date-time":"2011-05-21T00:00:00Z","timestamp":1305936000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2011,10]]},"DOI":"10.1007\/s10009-011-0195-9","type":"journal-article","created":{"date-parts":[[2011,5,19]],"date-time":"2011-05-19T22:16:46Z","timestamp":1305843406000},"page":"463-489","source":"Crossref","is-referenced-by-count":17,"title":["Formal methods for security in the Xenon hypervisor"],"prefix":"10.1007","volume":"13","author":[{"given":"Leo","family":"Freitas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"McDermott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,5,21]]},"reference":[{"key":"195_CR1","volume-title":"Security Engineering: A Guide to Building Dependable Distributed Systems","author":"R. Anderson","year":"2008","unstructured":"Anderson R.: Security Engineering: A Guide to Building Dependable Distributed Systems. 2nd edn. Wiley, New York (2008)","edition":"2"},{"key":"195_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction. Graduate Text in Computer Science","author":"R.-J. Back","year":"1998","unstructured":"Back R.-J., von Wright J.: Refinement Calculus: A Systematic Introduction. Graduate Text in Computer Science. Springer, New York (1998)"},{"key":"195_CR3","doi-asserted-by":"crossref","unstructured":"Barham, P., Dragovic, B., Fraiser, K., Hand, S., Harris, T., Ho, A., Neugebauer, R., Pratt, I., Warfield, A.: Xen and the art of virtualization. In: Proceedings of 19th ACM Symposium on Operating Systems Principles (SOSP-19), Bolton Landing, New York, USA, October 2003","DOI":"10.1145\/945445.945462"},{"issue":"4","key":"195_CR4","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/j.scico.2008.09.014","volume":"74","author":"A. Butterfield","year":"2009","unstructured":"Butterfield A., Freitas L., Woodcock J.: Mechanising a formal model of flash memory. Sci. Comput. Program. 74(4), 219\u2013237 (2009)","journal-title":"Sci. Comput. Program."},{"key":"195_CR5","volume-title":"The Definitive Guide to the Xen Hypervisor","author":"D. Chisnall","year":"2008","unstructured":"Chisnall D.: The Definitive Guide to the Xen Hypervisor. Prentice-Hall, Englewood Cliffs (2008)"},{"key":"195_CR6","unstructured":"Coker, G.: Xen security modules. Xen Summit 2007 Presentation, April 2007. http:\/\/www.xensource.com\/xen\/xensummit.html"},{"key":"195_CR7","unstructured":"The Common Criteria Project Sponsoring Organizations.: Common Criteria for Information Technology Security Evaluation, v. 3.1, rev. 1 (edn.), September 2006. Also referred to as ISO 15408"},{"key":"195_CR8","unstructured":"The Common Criteria Project Sponsoring Organizations.: Common Methodology for Information Technology Security Evaluation, v. 3.1, rev. 1 (edn.), September 2006"},{"key":"195_CR9","doi-asserted-by":"crossref","unstructured":"Denning, D.: A lattice model of secure information flow. Commun. ACM 19(5) (1976)","DOI":"10.1145\/360051.360056"},{"issue":"1","key":"195_CR10","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/s00165-007-0059-y","volume":"20","author":"L. Freitas","year":"2008","unstructured":"Freitas L., Woodcock J.: Mechanising Mondex with Z\/Eves. Form. Asp. Comput. 20(1), 117\u2013139 (2008)","journal-title":"Form. Asp. Comput."},{"issue":"2\u20133","key":"195_CR11","first-page":"357","volume":"3","author":"L. Freitas","year":"2009","unstructured":"Freitas L., Woodcock J.: A chain datatype in z. Int. J. Softw. Inform. 3(2\u20133), 357\u2013374 (2009)","journal-title":"Int. J. Softw. Inform."},{"key":"195_CR12","unstructured":"Greeve, D., Wilding, M., Vanfleet, W.M.: A separation kernel formal security policy. In: Proceedings of ACL2 Workshop, Boulder, Colorado, USA, July 2003"},{"key":"195_CR13","volume-title":"Communicating Sequential Processes","author":"C. Hoare","year":"1985","unstructured":"Hoare C.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"195_CR14","unstructured":"IA-32 Intel Architecture Software Developer\u2019s Manual: vol. 3A: System Programming Guide, part 1. Technical Report 253668-020US, Intel Corp., June 2006"},{"key":"195_CR15","unstructured":"ISO\/IEC.: ISO\/IEC 13568: Information Technology\u2014Z Formal Specification Notation\u2014Syntax, Type System and Semantics (2002)"},{"issue":"4","key":"195_CR16","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1145\/1498765.1498787","volume":"52","author":"D. Jackson","year":"2009","unstructured":"Jackson D.: A direct path to dependable software. Commun. ACM 52(4), 78\u201388 (2009)","journal-title":"Commun. ACM"},{"issue":"6","key":"195_CR17","doi-asserted-by":"crossref","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. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"key":"195_CR18","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cook, D., Derrin, P., Elkaduwe, D., Englehardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of 22nd ACM Symposium on Operating System Principles, Big Sky, MT, USA, October 2009","DOI":"10.1145\/1629575.1629596"},{"key":"195_CR19","doi-asserted-by":"crossref","first-page":"806","DOI":"10.1007\/978-3-642-05089-3_51","volume-title":"FM 2009: Formal Methods. Lecture Notes in Computer Science, vol. 5850","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: Formal Methods. Lecture Notes in Computer Science, vol. 5850, pp. 806\u2013809. Springer, Berlin (2009)"},{"issue":"3","key":"195_CR20","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/322017.322025","volume":"24","author":"R. Lipton","year":"1977","unstructured":"Lipton R., Lawrence S.: A linear-time algorithm for deciding subject security. JACM 24(3), 455\u2013464 (1977)","journal-title":"JACM"},{"key":"195_CR21","doi-asserted-by":"crossref","unstructured":"Mantel, H.: The framework of selective interleaving functions and the modular assembly kit. In: Proceedings of Formal Methods in Security Engineering, Fairfax, Virginia, USA, November 2005","DOI":"10.1145\/1103576.1103584"},{"key":"195_CR22","doi-asserted-by":"crossref","unstructured":"McDermott, J.: Fine-grained inspection for higher-assurance software security in open source. In: Proceedings of 43rd Hawaii International Conference on Systems and Sciences, pp. 1\u201310, Kauai, HI, January 2010","DOI":"10.1109\/HICSS.2010.211"},{"key":"195_CR23","doi-asserted-by":"crossref","unstructured":"McDermott, J., Freitas, L.: A formal security policy model for Xenon. In: Proceedings of Formal Methods in Security Engineering (FMSE \u201908), October 2008","DOI":"10.1145\/1456396.1456401"},{"issue":"1","key":"195_CR24","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.istr.2008.01.001","volume":"13","author":"J. McDermott","year":"2008","unstructured":"McDermott J., Kirby J., Montrose B., Johnson T., Kang M.: Re-engineering Xen internals for higher-assurance security. Inform. Secur. Tech. Rep. 13(1), 17\u201324 (2008)","journal-title":"Inform. Secur. Tech. Rep."},{"key":"195_CR25","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proceedings of IEEE Symposium on Research in Security and Privacy, Oakland, California, USA, May 1994"},{"issue":"1","key":"195_CR26","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s00165-007-0052-5","volume":"21","author":"M. Oliveira","year":"2007","unstructured":"Oliveira M., Cavalcanti A., Woodcock J.: A UTP semantics for Circus. Form. Asp. Comput. 21(1), 3\u201332 (2007)","journal-title":"Form. Asp. Comput."},{"key":"195_CR27","volume-title":"REFINE\u20192006, Eletronic Notes in Theoretical Computer Science","author":"M.V.M. Oliveira","year":"2006","unstructured":"Oliveira M.V.M., Cavalcanti A.L.C., Woodcock J.C.P.: A denotational semantics for Circus. In: Aichernig, B., Derrick, J. (eds) REFINE\u20192006, Eletronic Notes in Theoretical Computer Science, Elsevier, Amsterdam (2006)"},{"key":"195_CR28","volume-title":"The Theory and Practice of Concurrency","author":"A. Roscoe","year":"1997","unstructured":"Roscoe A.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"195_CR29","doi-asserted-by":"crossref","unstructured":"Roscoe, A., Woodcock, J., Wulf, L.: Non-interference through determinism. In: Proc. ESORICS, Brighton, UK, November 1994","DOI":"10.1007\/3-540-58618-0_55"},{"key":"195_CR30","volume-title":"Modelling and Analysis of Security Protocols","author":"P. Ryan","year":"2001","unstructured":"Ryan P., Schneider S.: Modelling and Analysis of Security Protocols. Addison-Wesley, Reading (2001)"},{"key":"195_CR31","unstructured":"Sailer, R., Jaeger, T., Valdez, E., C\u00e1ceres, R., Perez, R., Berger, S., Griffin, J., van Doorn, L.: Building a MAC-based security architecture for the Xen open-source hypervisor. In: Proceedings of 21st Annual Computer Security Applications Conference, Tucson, Arizona, USA, December 2005"},{"key":"195_CR32","volume-title":"Using Z: Specification, Refinement, and Proof. International Series in Computer Science","author":"J. Woodcock","year":"1996","unstructured":"Woodcock J., Davies J.: Using Z: Specification, Refinement, and Proof. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1996)"},{"key":"195_CR33","unstructured":"Woodcock, J.C.P., Cavalcanti, A.L.C., Gaudel, M.-C., Freitas, L.J.S.: Operational Semantics for Circus. Form. Asp. Comput. (2009, in press)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0195-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0195-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0195-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T00:01:08Z","timestamp":1560211268000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0195-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,21]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2011,10]]}},"alternative-id":["195"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0195-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,5,21]]}}}