{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:38:06Z","timestamp":1743028686711,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319121536"},{"type":"electronic","value":"9783319121543"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12154-3_6","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T08:20:23Z","timestamp":1413188423000},"page":"87-104","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Modeling and Verification of CloudProxy"],"prefix":"10.1007","author":[{"given":"Wei Yang","family":"Tan","sequence":"first","affiliation":[]},{"given":"Rohit","family":"Sinha","sequence":"additional","affiliation":[]},{"given":"John L.","family":"Manferdelli","sequence":"additional","affiliation":[]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,10,14]]},"reference":[{"key":"6_CR1","unstructured":"Adelard: ASCAD The Adelard Safety Case Development (ASCAD) Manual (1998)"},{"key":"6_CR2","unstructured":"GSN Community Standard Version 1, November 2011"},{"key":"6_CR3","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"825","volume-title":"Handbook of Satisfiability, Chap.\u00a026","author":"C Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Chap.\u00a026. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"issue":"1","key":"6_CR4","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/2133375.2133378","volume":"15","author":"K Bhargavan","year":"2012","unstructured":"Bhargavan, K., Fournet, C., Corin, R., Z\u0103linescu, E.: Verified cryptographic implementations for TLS. ACM Trans. Inf. Syst. Secur. 15(1), 3:1\u20133:32 (2012)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"RE Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"6_CR6","unstructured":"Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI\u201908, pp. 209\u2013224, Berkeley, CA, USA (2008)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Clarkson, M., Schneider, F.: Hyperproperties. In: IEEE 21st Computer Security Foundations Symposium, CSF \u201908, pp. 51\u201365 (2008)","DOI":"10.1109\/CSF.2008.7"},{"key":"6_CR8","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)"},{"issue":"2","key":"6_CR9","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Gu, L., Vaynberg, A., Ford, B., Shao, Z., Costanzo, D.: Certikos: a certified kernel for secure cloud computing. In: Proceedings of the Second Asia-Pacific Workshop on Systems, APSys \u201911, pp. 3:1\u20133:5. ACM, New York (2011)","DOI":"10.1145\/2103799.2103803"},{"issue":"5","key":"6_CR12","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1145\/1506409.1506429","volume":"52","author":"JA Halderman","year":"2009","unstructured":"Halderman, J.A., Schoen, S.D., Heninger, N., Clarkson, W., Paul, W., Calandrino, J.A., Feldman, A.J., Appelbaum, J., Felten, E.W.: Lest we remember: cold-boot attacks on encryption keys. Commun. ACM 52(5), 91\u201398 (2009)","journal-title":"Commun. ACM"},{"issue":"1\u20133","key":"6_CR13","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0167-6423(99)00024-6","volume":"37","author":"R Joshi","year":"2000","unstructured":"Joshi, R., Leino, K.M.: A semantic approach to secure information flow. Sci. Comput. Program. 37(1\u20133), 113\u2013138 (2000)","journal-title":"Sci. Comput. Program."},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., 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. In: Symposium On Operating Systems Principles, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-27813-9_40","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2004","unstructured":"Lahiri, S.K., Seshia, S.A.: The UCLID decision procedure. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 475\u2013478. Springer, Heidelberg (2004)"},{"key":"6_CR16","unstructured":"Manferdelli, J., Roeder, T., Schneider, F.: The cloudproxy tao for trusted computing. Technical report UCB\/EECS-2013-135, University of California, Berkeley, July 2013"},{"key":"6_CR17","unstructured":"Parno, B.: Bootstrapping trust in a \u201ctrusted\u201d platform. In: Proceedings of the 3rd Conference on Hot Topics in Security, HOTSEC\u201908, pp. 9:1\u20139:6, Berkeley, CA, USA (2008)"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/3-540-11494-7_23","volume-title":"International Symposium on Programming","author":"J Rushby","year":"1982","unstructured":"Rushby, J.: Proof of separability\u2013a verification technique for a class of security kernels. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol. 137, pp. 352\u2013367. Springer, Heidelberg (1982)"},{"key":"6_CR19","unstructured":"Shankar, N.: Building assurance cases with the evidential tool bus, March 2014. http:\/\/chess.eecs.berkeley.edu\/pubs\/1061.html"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Stephen Blanchette, J.: Assurance cases for design analysis of complex system of systems software. Technical report, Software Engineering Institute, Carnegie Mellon University, April 2009","DOI":"10.2514\/6.2009-1921"},{"key":"6_CR21","unstructured":"Sturton, C., Sinha, R., Dang, T.H., Jain, S., McCoyd, M., Tan, W.-Y., Maniatis, P., Seshia, S.A., Wagner, D.: Symbolic software model validation. In: Proceedings of the 10th ACM\/IEEE International Conference on Formal Methods and Models for Codesign, October 2013"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12154-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T02:57:25Z","timestamp":1675997845000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-12154-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319121536","9783319121543"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12154-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"14 October 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}