{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T04:49:29Z","timestamp":1764305369199,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,10,12]],"date-time":"2015-10-12T00:00:00Z","timestamp":1444608000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF STARSS","award":["1528108"],"award-info":[{"award-number":["1528108"]}]},{"name":"SRC","award":["2460.001"],"award-info":[{"award-number":["2460.001"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,10,12]]},"DOI":"10.1145\/2810103.2813608","type":"proceedings-article","created":{"date-parts":[[2015,10,6]],"date-time":"2015-10-06T15:22:12Z","timestamp":1444144932000},"page":"1169-1184","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":85,"title":["Moat"],"prefix":"10.1145","author":[{"given":"Rohit","family":"Sinha","sequence":"first","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}]},{"given":"Sriram","family":"Rajamani","sequence":"additional","affiliation":[{"name":"Microsoft Research, Bangalore, India"}]},{"given":"Sanjit","family":"Seshia","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}]},{"given":"Kapil","family":"Vaswani","sequence":"additional","affiliation":[{"name":"Microsoft Research, Bangalore, India"}]}],"member":"320","published-online":{"date-parts":[[2015,10,12]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Available at http:\/\/www.cryptopp.com\/.  Available at http:\/\/www.cryptopp.com\/."},{"key":"e_1_3_2_1_2_1","unstructured":"https:\/\/devmoat.github.io.  https:\/\/devmoat.github.io."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.30"},{"key":"e_1_3_2_1_4_1","unstructured":"ARM Security Technology - Building a Secure System using TrustZone Technology. ARM Technical White Paper.  ARM Security Technology - Building a Secure System using TrustZone Technology. ARM Technical White Paper."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660322"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108792.1108813"},{"key":"e_1_3_2_1_8_1","volume-title":"Handbook of Satisfiability","author":"Barrett C.","year":"2009","unstructured":"C. Barrett , R. Sebastiani , S. A. Seshia , and C. Tinelli . Satisfiability modulo theories . In A. Biere, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability , volume 4 , chapter 8. IOS Press , 2009 . C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In A. Biere, H. van Maaren, and T. Walsh, editors, Handbook of Satisfiability, volume 4, chapter 8. IOS Press, 2009."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1370677.1370680"},{"key":"e_1_3_2_1_10_1","volume-title":"USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Baumann A.","year":"2014","unstructured":"A. Baumann , M. Peinado , and G. Hunt . Shielding applications from an untrusted cloud with Haven . In USENIX Symposium on Operating Systems Design and Implementation (OSDI) , 2014 . A. Baumann, M. Peinado, and G. Hunt. Shielding applications from an untrusted cloud with Haven. In USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2014."},{"key":"e_1_3_2_1_11_1","first-page":"82","volume-title":"An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop","author":"Blanchet B.","year":"2001","unstructured":"B. Blanchet . An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop , pages 82 -- 96 , Cape Breton, Canada , June 2001 . B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop, pages 82--96, Cape Breton, Canada, June 2001."},{"key":"e_1_3_2_1_12_1","volume-title":"Workshop on the link between formal and computational models","author":"Blanchet B.","year":"2005","unstructured":"B. Blanchet . A computationally sound automatic prover for cryptographic protocols . In Workshop on the link between formal and computational models , Paris, France , June 2005 . B. Blanchet. A computationally sound automatic prover for cryptographic protocols. In Workshop on the link between formal and computational models, Paris, France, June 2005."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1029179.1029200"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032342"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734437"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891830"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663716.2663755"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328478"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062518"},{"key":"e_1_3_2_1_21_1","first-page":"165","volume-title":"Proceedings of the 11th USENIX conference on Operating Systems Design and Implementation","author":"Hawblitzel C.","year":"2014","unstructured":"C. Hawblitzel , J. Howell , J. R. Lorch , A. Narayan , B. Parno , D. Zhang , and B. Zill . Ironclad apps: end-to-end security via automated full-system verification . In Proceedings of the 11th USENIX conference on Operating Systems Design and Implementation , pages 165 -- 181 , 2014 . C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. Ironclad apps: end-to-end security via automated full-system verification. In Proceedings of the 11th USENIX conference on Operating Systems Design and Implementation, pages 165--181, 2014."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1920261.1920300"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487726.2488370"},{"key":"e_1_3_2_1_24_1","unstructured":"Intel Software Guard Extensions Programming Reference. Available at https:\/\/software.intel.com\/sites\/default\/files\/329298-001.pdf.  Intel Software Guard Extensions Programming Reference. Available at https:\/\/software.intel.com\/sites\/default\/files\/329298-001.pdf."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487726.2488368"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2699855.2699858"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/268998.266669"},{"key":"e_1_3_2_1_29_1","first-page":"479","volume-title":"Proceedings of the 22nd USENIX Conference on Security","author":"Noorman J.","year":"2013","unstructured":"J. Noorman , P. Agten , W. Daniels , R. Strackx , A. Van Herrewege , C. Huygens , B. Preneel , I. Verbauwhede , and F. Piessens . Sancus: Low-cost trustworthy extensible networked devices with a zero-software trusted computing base . In Proceedings of the 22nd USENIX Conference on Security , pages 479 -- 494 , 2013 . J. Noorman, P. Agten, W. Daniels, R. Strackx, A. Van Herrewege, C. Huygens, B. Preneel, I. Verbauwhede, and F. Piessens. Sancus: Low-cost trustworthy extensible networked devices with a zero-software trusted computing base. In Proceedings of the 22nd USENIX Conference on Security, pages 479--494, 2013."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-37621-7_9"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541949"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.10"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"}],"event":{"name":"CCS'15: The 22nd ACM Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Denver Colorado USA","acronym":"CCS'15"},"container-title":["Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2810103.2813608","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2810103.2813608","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:36Z","timestamp":1750225716000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2810103.2813608"}},"subtitle":["Verifying Confidentiality of Enclave Programs"],"short-title":[],"issued":{"date-parts":[[2015,10,12]]},"references-count":35,"alternative-id":["10.1145\/2810103.2813608","10.1145\/2810103"],"URL":"https:\/\/doi.org\/10.1145\/2810103.2813608","relation":{},"subject":[],"published":{"date-parts":[[2015,10,12]]},"assertion":[{"value":"2015-10-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}