{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:32Z","timestamp":1776305252203,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":81,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,30]],"date-time":"2017-10-30T00:00:00Z","timestamp":1509321600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100007245","name":"Microelectronics Advanced Research Corporation","doi-asserted-by":"publisher","award":["STARnet center TerraSwarm"],"award-info":[{"award-number":["STARnet center TerraSwarm"]}],"id":[{"id":"10.13039\/100007245","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1413920, CNS-1528108"],"award-info":[{"award-number":["CNS-1413920, CNS-1528108"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,30]]},"DOI":"10.1145\/3133956.3134098","type":"proceedings-article","created":{"date-parts":[[2017,10,27]],"date-time":"2017-10-27T12:48:18Z","timestamp":1509108498000},"page":"2435-2450","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":76,"title":["A Formal Foundation for Secure Remote Execution of Enclaves"],"prefix":"10.1145","author":[{"given":"Pramod","family":"Subramanyan","sequence":"first","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}]},{"given":"Rohit","family":"Sinha","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}]},{"given":"Ilia","family":"Lebedev","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, USA"}]},{"given":"Srinivas","family":"Devadas","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, USA"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,10,30]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"Lenovo ThinkPad System Management Mode Arbitrary Code Execution 0day Exploit. Available at https:\/\/github.com\/Cr4sh\/ThinkPwn.git."},{"issue":"4","key":"e_1_3_2_2_2_1","first-page":"18","volume":"3","author":"Alves T.","year":"2004","unstructured":"T. Alves and D. Felton. TrustZone: Integrated Hardware and Software Security. Information Quarterly, 3(4):18--24, 2004.","journal-title":"TrustZone: Integrated Hardware and Software Security. Information Quarterly"},{"key":"e_1_3_2_2_3_1","volume-title":"Proceedings of the 2nd International Workshop on Hardware and Architectural Support for Security and Privacy, HASP","volume":"13","author":"Anati I.","year":"2013","unstructured":"I. Anati, S. Gueron, S. P. Johnson, and V. R. Scarlata. Innovative Technology for CPU Based Attestation and Sealing. In Proceedings of the 2nd International Workshop on Hardware and Architectural Support for Security and Privacy, HASP, volume 13, 2013."},{"key":"e_1_3_2_2_4_1","volume-title":"The Rocket Chip Generator. EECS Department","author":"Asanovic K.","year":"2016","unstructured":"K. Asanovic, R. Avizienis, J. Bachrach, S. Beamer, D. Biancolin, C. Celio, H. Cook, D. Dabbelt, J. Hauser, A. Izraelevitz, et al. The Rocket Chip Generator. EECS Department, University of California, Berkeley, Tech. Rep. UCB\/EECS-2016--17, 2016."},{"key":"e_1_3_2_2_5_1","volume-title":"Instruction Sets Should Be Free: The Case For RISC-V. EECS Department","author":"Asanovi\u0107 K.","year":"2014","unstructured":"K. Asanovi\u0107 and D. A. Patterson. Instruction Sets Should Be Free: The Case For RISC-V. EECS Department, University of California, Berkeley, Tech. Rep. UCB\/EECS- 2014--146, 2014."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.28"},{"key":"e_1_3_2_2_7_1","first-page":"364","volume-title":"Leino. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO '05","author":"Barnett M.","year":"2005","unstructured":"M. Barnett, B. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO '05, LNCS 4111, pages 364--387, 2005."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_3_2_2_9_1","volume-title":"Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Y.","year":"2013","unstructured":"Y. Bertot and P. Cast\u00e9ran. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Springer Science & Business Media, 2013."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2016.123"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11894063_16"},{"key":"e_1_3_2_2_12_1","volume-title":"Software Grand Exposure: SGX Cache Attacks Are Practical. CoRR, abs\/1702.07521","author":"Brasser F.","year":"2017","unstructured":"F. Brasser, U. M\u00fcller, A. Dmitrienko, K. Kostiainen, S. Capkun, and A. Sadeghi. Software Grand Exposure: SGX Cache Attacks Are Practical. CoRR, abs\/1702.07521, 2017."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23822-2_20"},{"key":"e_1_3_2_2_15_1","first-page":"1","volume-title":"Proceedings of the 12th Conference on USENIX Security Symposium -","volume":"12","author":"Brumley D.","year":"2003","unstructured":"D. Brumley and D. Boneh. Remote Timing Attacks Are Practical. In Proceedings of the 12th Conference on USENIX Security Symposium - Volume 12, SSYM'03, pages 1--1, Berkeley, CA, USA, 2003. USENIX Association."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2010.5416657"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1554339.1554341"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_2_21_1","first-page":"857","volume-title":"Sanctum: Minimal Hardware Extensions for Strong Software Isolation. In 25th USENIX Security Symposium (USENIX Security 16)","author":"Costan V.","year":"2016","unstructured":"V. Costan, I. Lebedev, and S. Devadas. Sanctum: Minimal Hardware Extensions for Strong Software Isolation. In 25th USENIX Security Symposium (USENIX Security 16), pages 857--874, Austin, TX, 2016. USENIX Association."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.16"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_25_1","volume-title":"Transactions on Architecture and Code Optimization (TACO)","author":"Domnitser L.","year":"2012","unstructured":"L. Domnitser, A. Jaleel, J. Loew, N. Abu-Ghazaleh, and D. Ponomarev. Nonmonopolizable caches: Low-complexity mitigation of cache side channel attacks. Transactions on Architecture and Code Optimization (TACO), 2012."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1002\/sec.166"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382536.2382540"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_2_29_1","volume-title":"Dynamics of a Trusted Platform: A building block approach","author":"Grawrock D.","year":"2009","unstructured":"D. Grawrock. Dynamics of a Trusted Platform: A building block approach. Intel Press, 2009."},{"key":"e_1_3_2_2_30_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."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487726.2488370"},{"key":"e_1_3_2_2_33_1","unstructured":"Intel Software Guard Extensions Programming Reference. Available at https: \/\/software.intel.com\/sites\/default\/files\/329298-001.pdf."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.42"},{"key":"e_1_3_2_2_35_1","unstructured":"Joanna Rutkowska. Red Pill... or how to detect VMM using (almost) one CPU instruction. https:\/\/github.com\/Cr4sh\/ThinkPwn.git."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68697-5_9"},{"key":"e_1_3_2_2_38_1","volume-title":"Inferring Fine-grained Control Flow Inside SGX Enclaves with Branch Shadowing. CoRR, abs\/1611.06952","author":"Lee S.","year":"2016","unstructured":"S. Lee, M. Shih, P. Gera, T. Kim, H. Kim, and M. Peinado. Inferring Fine-grained Control Flow Inside SGX Enclaves with Branch Shadowing. CoRR, abs\/1611.06952, 2016."},{"key":"e_1_3_2_2_39_1","first-page":"144","volume-title":"CAV 2015, San Francisco, CA, USA, July 18--24, 2015, Proceedings, Part II","author":"Leslie-Hurd R.","year":"2015","unstructured":"R. Leslie-Hurd, D. Caspi, and M. Fernandez. Verifying Linearizability of Intel\u00ae Software Guard Extensions. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18--24, 2015, Proceedings, Part II, pages 144--160, 2015."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541947"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993512"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/356989.357005"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2016.7446082"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.28"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.43"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516692"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487726.2488368"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1992-1103"},{"key":"e_1_3_2_2_49_1","volume-title":"CacheZoom: How SGX Amplifies The Power of Cache Attacks. CoRR, abs\/1703.06986","author":"Moghimi A.","year":"2017","unstructured":"A. Moghimi, G. Irazoqui, and T. Eisenbarth. CacheZoom: How SGX Amplifies The Power of Cache Attacks. CoRR, abs\/1703.06986, 2017."},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_2_52_1","first-page":"41","volume-title":"7th International Conference, DIMVA 2010, Bonn, Germany, July 8--9, 2010. Proceedings","author":"Neugschwandtner M.","year":"2010","unstructured":"M. Neugschwandtner, C. Platzer, P. M. Comparetti, and U. Bayer. dAnubis - Dynamic Device Driver Analysis Based on Virtual Machine Introspection. In Detection of Intrusions and Malware, and Vulnerability Assessment, 7th International Conference, DIMVA 2010, Bonn, Germany, July 8--9, 2010. Proceedings, pages 41--60, 2010."},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_2_54_1","first-page":"479","volume-title":"Proceedings of the 22Nd USENIX Conference on Security, SEC'13","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, SEC'13, pages 479--494, Berkeley, CA, USA, 2013. USENIX Association."},{"key":"e_1_3_2_2_55_1","first-page":"619","volume-title":"Oblivious Multi-Party Machine Learning on Trusted Processors. In 25th USENIX Security Symposium (USENIX Security 16)","author":"Ohrimenko O.","year":"2016","unstructured":"O. Ohrimenko, F. Schuster, C. Fournet, A. Mehta, S. Nowozin, K. Vaswani, and M. Costa. Oblivious Multi-Party Machine Learning on Trusted Processors. In 25th USENIX Security Symposium (USENIX Security 16), pages 619--636, Austin, TX, 2016. USENIX Association."},{"key":"e_1_3_2_2_56_1","volume-title":"The Spy in the Sandbox - Practical Cache Attacks in Javascript. CoRR, abs\/1502.07373","author":"Oren Y.","year":"2015","unstructured":"Y. Oren, V. P. Kemerlis, S. Sethumadhavan, and A. D. Keromytis. The Spy in the Sandbox - Practical Cache Attacks in Javascript. CoRR, abs\/1502.07373, 2015."},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.38"},{"key":"e_1_3_2_2_58_1","volume-title":"Formal Abstractions for Attested Execution Secure Processors. IACR Cryptology ePrint Archive","author":"Pass R.","year":"2016","unstructured":"R. Pass, E. Shi, and F. Tram\u00e8r. Formal Abstractions for Attested Execution Secure Processors. IACR Cryptology ePrint Archive, 2016:1027, 2016."},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699503"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2554850.2554865"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2015.03.002"},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1995.398927"},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_23"},{"key":"e_1_3_2_2_64_1","unstructured":"J. Rutkowska. Security challenges in virtualized environments."},{"key":"e_1_3_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_2_66_1","volume-title":"Malware Guard Extension: Using SGX to Conceal Cache Attacks. CoRR, abs\/1702.08719","author":"Schwarz M.","year":"2017","unstructured":"M. Schwarz, S. Weiser, D. Gruss, C. Maurice, and S. Mangard. Malware Guard Extension: Using SGX to Conceal Cache Attacks. CoRR, abs\/1702.08719, 2017."},{"key":"e_1_3_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2017.23037"},{"key":"e_1_3_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2017.23193"},{"key":"e_1_3_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2897845.2897885"},{"key":"e_1_3_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908113"},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813608"},{"key":"e_1_3_2_2_72_1","unstructured":"T. Skolem. Logico-combinatorial investigations in the satisfiability or provability of mathematical propositions: a simplified proof of a theorem by L. L\u00f6wenheim and generalizations of the theorem. From Frege to G\u00f6del. A Source Book in Mathematical Logic 1879--1931 pages 252--263 1967."},{"key":"e_1_3_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268975"},{"key":"e_1_3_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382200"},{"key":"e_1_3_2_2_75_1","unstructured":"P. Subramanyan R. Sinha I. Lebedev S. Devadas and S. A. Seshia. Models and Proofs for the Trusted Abstract Platform (TAP) Intel SGX and MIT Sanctum. https:\/\/github.com\/0tcb\/TAP."},{"key":"e_1_3_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/782814.782838"},{"key":"e_1_3_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_3_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-009-9049-y"},{"key":"e_1_3_2_2_79_1","first-page":"109","volume-title":"CAV 2015, San Francisco, CA, USA, July 18--24, 2015, Proceedings, Part II","author":"Vijayaraghavan M.","year":"2015","unstructured":"M. Vijayaraghavan, A. Chlipala, Arvind, and N. Dave. Modular Deductive Verification of Multiprocessor Hardware Designs. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18--24, 2015, Proceedings, Part II, pages 109--127, 2015."},{"key":"e_1_3_2_2_80_1","author":"Volpano D.","year":"1996","unstructured":"D. Volpano, C. Irvine, and G. Smith. A Sound Type System for Secure Flow Analysis. Journal of Computer Security, 4(2--3):167--187, Jan. 1996.","journal-title":"Journal of Computer Security, 4(2--3):167--187"},{"key":"e_1_3_2_2_83_1","first-page":"640","volume-title":"Controlled-Channel Attacks: Deterministic Side Channels for Untrusted Operating Systems. In 2015 IEEE Symposium on Security and Privacy, SP 2015","author":"Xu Y.","year":"2015","unstructured":"Y. Xu, W. Cui, and M. Peinado. Controlled-Channel Attacks: Deterministic Side Channels for Untrusted Operating Systems. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17--21, 2015, pages 640--656, 2015."},{"key":"e_1_3_2_2_84_1","first-page":"719","volume-title":"Proceedings of the 23rd USENIX Security Symposium","author":"Yarom Y.","year":"2014","unstructured":"Y. Yarom and K. Falkner. FLUSH+RELOAD: A High Resolution, Low Noise, L3 Cache Side-Channel Attack. In Proceedings of the 23rd USENIX Security Symposium, San Diego, CA, USA, August 20--22, 2014., pages 719--732, 2014."},{"key":"e_1_3_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694372"}],"event":{"name":"CCS '17: 2017 ACM SIGSAC Conference on Computer and Communications Security","location":"Dallas Texas USA","acronym":"CCS '17","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133956.3134098","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134098","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134098","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:03Z","timestamp":1750212663000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133956.3134098"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,30]]},"references-count":81,"alternative-id":["10.1145\/3133956.3134098","10.1145\/3133956"],"URL":"https:\/\/doi.org\/10.1145\/3133956.3134098","relation":{},"subject":[],"published":{"date-parts":[[2017,10,30]]},"assertion":[{"value":"2017-10-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}