{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T22:10:05Z","timestamp":1748815805961,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496640"},{"type":"electronic","value":"9783662496657"}],"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-49665-7_13","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T08:09:42Z","timestamp":1458547782000},"page":"214-230","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Modeling and Abstraction of Memory Management in a Hypervisor"],"prefix":"10.1007","author":[{"given":"Pauline","family":"Bolignano","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[]},{"given":"Vincent","family":"Siles","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-27705-4_17","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E Alkassar","year":"2012","unstructured":"Alkassar, E., Cohen, E., Kovalev, M., Paul, W.J.: Verification of TLB virtualization implemented in C. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 209\u2013224. Springer, Heidelberg (2012). http:\/\/www-wjp.cs.uni-saarland.de\/publikationen\/ACKP12.pdf"},{"key":"13_CR2","unstructured":"AMD I\/O virtualization technology (IOMMU) specification (2015). http:\/\/support.amd.com\/TechDocs\/48882_IOMMU.pdf"},{"key":"13_CR3","unstructured":"Andrabi, S.J.: Verification of XMHF HPT protection setup. Technical report, University of North Carolina (2013). http:\/\/cs.unc.edu\/~sandrabi\/Project_work\/VerificationofXMHFHPTProtectionSetup.pdf"},{"key":"13_CR4","unstructured":"ARM system memory management unit (2012). http:\/\/infocenter.arm.com\/help\/index.jsp?topic=\/com.arm.doc.ihi0062b\/index.html"},{"key":"13_CR5","volume-title":"Operating Systems: Three Easy Pieces","author":"RH Arpaci-Dusseau","year":"2014","unstructured":"Arpaci-Dusseau, R.H., Arpaci-Dusseau, A.C.: Operating Systems: Three Easy Pieces, 0.80th edn. Arpaci-Dusseau Books, Wisconsin (2014)","edition":"0.80"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., Betarte, G., Campo, J., Luna, C.: Cache-leakage resilient OS isolation in an idealized model of virtualization. In: 2012 IEEE 25th Computer Security Foundations Symposium (CSF), pp. 186\u2013197, June 2012","DOI":"10.1109\/CSF.2012.17"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-19458-5_2","volume-title":"Formal Methods for Industrial Critical Systems","author":"A Blanchard","year":"2015","unstructured":"Blanchard, A., Kosmatov, N., Lemerre, M., Loulergue, F.: A case study on formal verification of the anaxagoros hypervisor paging system with frama-C. In: N\u00fa\u00f1ez, M., G\u00fcdemann, M. (eds.) Formal Methods for Industrial Critical Systems. LNCS, vol. 9128, pp. 15\u201330. Springer, Heidelberg (2015). http:\/\/dx.doi.org\/10.1007\/978-3-319-19458-5_2"},{"key":"13_CR8","unstructured":"Common criteria portal. http:\/\/www.commoncriteriaportal.org\/"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). http:\/\/research.microsoft.com\/apps\/pubs\/default.aspx?id=117859"},{"issue":"6","key":"13_CR10","doi-asserted-by":"publisher","first-page":"1205","DOI":"10.1007\/s00165-014-0296-9","volume":"26","author":"M Daum","year":"2014","unstructured":"Daum, M., Billing, N., Klein, G.: Concerned with the unprivileged: user programs in kernel refinement. Formal Asp. Comput. 26(6), 1205\u20131229 (2014). http:\/\/dx.doi.org\/10.1007\/s00165-014-0296-9","journal-title":"Formal Asp. Comput."},{"key":"13_CR11","unstructured":"Kovalev, M.: TLB virtualization in the context of hypervisor verification. Ph.D. thesis, Universit\u00e4t des Saarlandes, Postfach 151141, 66041 Saarbr\u00fccken (2013). http:\/\/scidok.sulb.unisaarland.de\/volltexte\/2013\/5215"},{"key":"13_CR12","unstructured":"Lescuyer, S.: ProvenCore: towards a verified isolation micro-kernel. In: International Workshop on MILS: Architecture and Assurance for Secure Systems (2015). http:\/\/milsworkshop2015.euromils.eu\/downloads\/hipeac_literature\/04-mils15_submission_6.pdf"},{"key":"13_CR13","unstructured":"Mijat, R., Nightingale, A.: Virtualization is coming to a platform near you (2011). https:\/\/www.arm.com\/files\/pdf\/System-MMU-Whitepaper-v8.0.pdf"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Murray, T.C., 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: 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, 19\u201322 May 2013. pp. 415\u2013429 (2013). http:\/\/dx.doi.org\/10.1109\/SP.2013.35","DOI":"10.1109\/SP.2013.35"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"578","DOI":"10.1007\/978-3-662-46078-8_48","volume-title":"SOFSEM 2015: Theory and Practice of Computer Science-Testing","author":"H Nemati","year":"2015","unstructured":"Nemati, H., Guanciale, R., Dam, M.: Trustworthy virtualization of the ARMv7 memory subsystem. In: Italiano, G.F., Margaria-Steffen, T., Pokorn\u00fd, J., Quisquater, J.-J., Wattenhofer, R. (eds.) SOFSEM 2015-Testing. LNCS, vol. 8939, pp. 578\u2013589. Springer, Heidelberg (2015). http:\/\/dx.doi.org\/10.1007\/978-3-662-46078-8_48"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Vasudevan, A., Chaki, S., Jia, L., McCune, J., Newsome, J., Datta, A.: Design, implementation and verification of an extensible and modular hypervisor framework. In: Proceedings of the 2013 IEEE Symposium on Security and Privacy, SP 2013, pp. 430\u2013444. IEEE Computer Society, Washington (2013). http:\/\/dx.doi.org\/10.1109\/SP.2013.36","DOI":"10.1109\/SP.2013.36"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Vetter, J., Petschik-Junker, M., Nordholz, J., Peter, M., Danisevskis, J.: Uncloaking rootkits on mobile devices with a hypervisor-based detector. In: ICISC (International Conference on Information Security and Cryptology), Seoul, Republic of Korea (2015)","DOI":"10.1007\/978-3-319-30840-1_17"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49665-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:29:19Z","timestamp":1748813359000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49665-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496640","9783662496657"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49665-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}