{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T23:49:45Z","timestamp":1725752985958},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642412011"},{"type":"electronic","value":"9783642412028"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41202-8_22","type":"book-chapter","created":{"date-parts":[[2013,10,21]],"date-time":"2013-10-21T05:11:19Z","timestamp":1382332279000},"page":"329-346","source":"Crossref","is-referenced-by-count":4,"title":["vTRUST: A Formal Modeling and Verification Framework for Virtualization Systems"],"prefix":"10.1007","author":[{"given":"Jianan","family":"Hao","sequence":"first","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Wentong","family":"Cai","sequence":"additional","affiliation":[]},{"given":"Guangdong","family":"Bai","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Process Analysis Toolkit, http:\/\/www.comp.nus.edu.sg\/"},{"key":"22_CR2","unstructured":"vTRUST Website, http:\/\/www.comp.nus.edu.sg\/%7Epat\/vtrust"},{"key":"22_CR3","unstructured":"AMD. Secure Virtual Machine Architecture Reference Manual"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Bleikertz, S., Gro\u00df, T., M\u00f6dersheim, S.: Automated Verification of Virtualized Infrastructures. In: CCSW, pp. 47\u201358 (2011)","DOI":"10.1145\/2046660.2046672"},{"key":"22_CR5","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.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Datta, A., Franklin, J., Garg, D., Kaynar, D.: A Logic of Secure Systems and its Application to Trusted Computing. In: SP, pp. 221\u2013236 (2009)","DOI":"10.1109\/SP.2009.16"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Hao, J., Cai, W.: Trusted Block as a Service: Towards Sensitive Applications on the Cloud. In: TrustCom, pp. 73\u201382 (2011)","DOI":"10.1109\/TrustCom.2011.13"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: Formal Verification of an OS Kernel. In: SOSP, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"22_CR9","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.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 806\u2013809. Springer, Heidelberg (2009)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"22_CR11","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1145\/361011.361073","volume":"17","author":"G.J. Popek","year":"1974","unstructured":"Popek, G.J., Goldberg, R.P.: Formal Requirements for Virtualizable Third Generation Architectures. Communications of the ACM\u00a017, 412\u2013421 (1974)","journal-title":"Communications of the ACM"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating Specification and Programs for System Modeling and Verification. In: TASE, pp. 127\u2013135 (2009)","DOI":"10.1109\/TASE.2009.32"},{"key":"22_CR13","unstructured":"Trusted Computing Group. Trusted Platform Module Main Specification. Version 1.2, Revision 116 (2011)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-13869-0_10","volume-title":"Trust and Trustworthy Computing","author":"A. Vasudevan","year":"2010","unstructured":"Vasudevan, A., McCune, J.M., Qu, N., van Doorn, L., Perrig, A.: Requirements for an Integrity-protected Hypervisor on the x86 Hardware Virtualized Architecture. In: Acquisti, A., Smith, S.W., Sadeghi, A.-R. (eds.) TRUST 2010. LNCS, vol.\u00a06101, pp. 141\u2013165. Springer, Heidelberg (2010)"},{"key":"22_CR15","unstructured":"Williams, B., Cross, T.: Virtualization System Security. In: IBM (2010)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41202-8_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,31]],"date-time":"2019-07-31T01:29:54Z","timestamp":1564536594000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41202-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642412011","9783642412028"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41202-8_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}