{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T02:47:51Z","timestamp":1769741271416,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":74,"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\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1712067"],"award-info":[{"award-number":["CCF-1712067"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"DARPA","award":["FA8750-15-2-0096"],"award-info":[{"award-number":["FA8750-15-2-0096"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,30]]},"DOI":"10.1145\/3133956.3134058","type":"proceedings-article","created":{"date-parts":[[2017,10,27]],"date-time":"2017-10-27T12:48:18Z","timestamp":1509108498000},"page":"875-890","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":63,"title":["Precise Detection of Side-Channel Vulnerabilities using Quantitative Cartesian Hoare Logic"],"prefix":"10.1145","author":[{"given":"Jia","family":"Chen","sequence":"first","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}]},{"given":"Yu","family":"Feng","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,10,30]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"2017. A timing channel in Jetty. https:\/\/github.com\/eclipse\/jetty.project\/commit\/ 2baa1abe4b1c380a30deacca1ed367466a1a62ea. (2017)."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1229285.1266999"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1791688.1791711"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_6"},{"key":"e_1_3_2_2_5_1","volume-title":"Lucky Thirteen: Breaking the TLS and DTLS Record Protocols. In 2013 IEEE Symposium on Security and Privacy, SP 2013","author":"Nadhem","year":"2013","unstructured":"Nadhem J. AlFardan and Kenneth G. Paterson. 2013. Lucky Thirteen: Breaking the TLS and DTLS Record Protocols. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19--22, 2013. 526--540."},{"key":"e_1_3_2_2_6_1","volume-title":"Verifying Constant-Time Implementations. In 25th USENIX Security Symposium, USENIX Security 16","author":"Almeida Jos\u00e9 Bacelar","year":"2016","unstructured":"Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Fran\u00e7ois Dupressoir, and Michael Emmi. 2016. Verifying Constant-Time Implementations. In 25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, August 10--12, 2016. 53--70."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_27"},{"key":"e_1_3_2_2_8_1","volume-title":"Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI).","author":"Antonopoulos Timos","year":"2017","unstructured":"Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Ter- auchi, and Shiyi Wei. 2017. Decomposition Instead of Self-Composition for k-Safety. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI)."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594299"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950362"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Gustavo Betarte Juan Campo Carlos Luna and David Pichardie. 2014. System-level Non-interference for Constant-time Cryptography. In Pro- ceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security (CCS '14). ACM 1267--1279. 10.1145\/2660267.2660283","DOI":"10.1145\/2660267.2660283"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_3_2_2_13_1","volume-title":"International Symposium, LFCS 2013, San Diego, CA, USA, January 6--8, 2013. Proceedings, Sergei N. Art\u00ebmov and Anil Nerode (Eds.)","volume":"7734","author":"Barthe Gilles","year":"2013","unstructured":"Gilles Barthe, Juan Manuel Crespo, and C\u00e9sar Kunz. 2013. Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. In Logical Foundations of Computer Science, International Symposium, LFCS 2013, San Diego, CA, USA, January 6--8, 2013. Proceedings, Sergei N. Art\u00ebmov and Anil Nerode (Eds.), Vol. 7734. Springer, 29--43."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985827"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","unstructured":"Andrew Bortz and Dan Boneh. 2007. Exposing Private Information by Timing Web Applications. In World Wide Web. ACM 621--628. 10.1145\/1242572.1242656","DOI":"10.1145\/1242572.1242656"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2866575"},{"key":"e_1_3_2_2_19_1","volume-title":"Proceedings of the 12th USENIX Security Symposium, Washington, D.C., USA, August 4--8","author":"Brumley David","year":"2003","unstructured":"David Brumley and Dan Boneh. 2003. Remote Timing Attacks Are Practical. In Proceedings of the 12th USENIX Security Symposium, Washington, D.C., USA, August 4--8, 2003."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.20"},{"key":"e_1_3_2_2_23_1","volume-title":"Side-Channels of Cyber-Physical Systems: Case Study in Additive Manufacturing","author":"Chhetri Sujit Rokka","year":"2017","unstructured":"Sujit Rokka Chhetri and Mohammad Abdullah Al Faruque. 2017. Side-Channels of Cyber-Physical Systems: Case Study in Additive Manufacturing. IEEE Design & Test (2017)."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_9"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/352600.352606"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1994\/1995-3103"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44709-1_21"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813688"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44709-3_14"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_2_35_1","first-page":"3","article-title":"Toward a mathematical foundation for information flow security","volume":"1","author":"James W","year":"1992","unstructured":"James W Gray III. 1992. Toward a mathematical foundation for information flow security. Journal of Computer Security 1, 3--4 (1992), 255--294.","journal-title":"Journal of Computer Security"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.22"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani Krishna K. Mehra and Trishul Chilimbi. 2009. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In Pro- ceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '09). ACM 127--139.","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_3_2_2_38_1","volume-title":"Differential Privacy Under Fire. In 20th USENIX Security Symposium","author":"Haeberlen Andreas","year":"2011","unstructured":"Andreas Haeberlen, Benjamin C. Pierce, and Arjun Narayan. 2011. Differential Privacy Under Fire. In 20th USENIX Security Symposium, San Francisco, CA, USA, August 8--12, 2011, Proceedings."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_10"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68697-5_9"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68697-5_9"},{"key":"e_1_3_2_2_47_1","volume-title":"Proceedings of the 22Nd International Conference on Automated Deduction (CADE-22)","author":"Shuvendu","unstructured":"Shuvendu K. Lahiri and Shaz Qadeer. 2009. Complexity and Algorithms for Mono- mial and Clausal Predicate Abstraction. In Proceedings of the 22Nd International Conference on Automated Deduction (CADE-22). Springer-Verlag, 214--229."},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694385"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2366231.2337173"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/11734727_14"},{"key":"e_1_3_2_2_51_1","volume-title":"Jif: Java information flow. Software release. Located at http:\/\/www. cs. cornell. edu\/jif 2005","author":"Myers Andrew C","year":"2001","unstructured":"Andrew C Myers, Lantian Zheng, Steve Zdancewic, Stephen Chong, and Nathaniel Nystrom. 2001. Jif: Java information flow. Software release. Located at http:\/\/www. cs. cornell. edu\/jif 2005 (2001)."},{"key":"e_1_3_2_2_52_1","volume-title":"From Coupling Relations to Mated Invariants for Check- ing Information Flow","author":"Naumann David A.","unstructured":"David A. Naumann. 2006. From Coupling Relations to Mated Invariants for Check- ing Information Flow. Springer Berlin Heidelberg, 279--296."},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.53"},{"key":"e_1_3_2_2_54_1","volume-title":"Multi-Run Side-Channel Analysis Using Symbolic Execution and Max-SMT. In Computer Security Foundations Symposium. IEEE.","author":"Pasareanu Corina","year":"2016","unstructured":"Corina Pasareanu, Quoc-Sang Phan, and Pasquale Malacaria. 2016. Multi-Run Side-Channel Analysis Using Symbolic Execution and Max-SMT. In Computer Security Foundations Symposium. IEEE."},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.34"},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"e_1_3_2_2_57_1","volume-title":"24th USENIX Security Symposium (USENIX Security 15)","author":"Rane Ashay","year":"2015","unstructured":"Ashay Rane, Calvin Lin, and Mohit Tiwari. 2015. Raccoon: Closing Digital Side- Channels through Obfuscated Execution. In 24th USENIX Security Symposium (USENIX Security 15). USENIX Association, Washington, D.C., 431--446."},{"key":"e_1_3_2_2_58_1","volume-title":"25th USENIX Security Symposium (USENIX Security 16)","author":"Rane Ashay","year":"2016","unstructured":"Ashay Rane, Calvin Lin, and Mohit Tiwari. 2016. Secure, Precise, and Fast Floating- Point Operations on x86 Processors. In 25th USENIX Security Symposium (USENIX Security 16). USENIX Association, Austin, TX, 71--86."},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892230"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813687"},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9402-4"},{"key":"e_1_3_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_3_2_2_67_1","volume-title":"Pro- ceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research (CASCON '99)","author":"Vall\u00e9e-Rai Raja","unstructured":"Raja Vall\u00e9e-Rai, Phong Co, Etienne Gagnon, Laurie Hendren, Patrick Lam, and Vijay Sundaresan. 1999. Soot - a Java Bytecode Optimization Framework. In Pro- ceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research (CASCON '99). IBM Press, 13--."},{"key":"e_1_3_2_2_68_1","volume-title":"IPSEC, WTLS .... In Advances in Cryptology - EUROCRYPT","author":"Vaudenay Serge","year":"2002","unstructured":"Serge Vaudenay. 2002. Security Flaws Induced by CBC Padding - Applications to SSL, IPSEC, WTLS .... In Advances in Cryptology - EUROCRYPT 2002, Inter- national Conference on the Theory and Applications of Cryptographic Techniques, Amsterdam, The Netherlands, April 28 - May 2, 2002, Proceedings. 534--546."},{"key":"e_1_3_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103669"},{"key":"e_1_3_2_2_70_1","volume-title":"CacheBleed: A Timing Attack on OpenSSL Constant Time RSA","author":"Yarom Yuval","unstructured":"Yuval Yarom, Daniel Genkin, and Nadia Heninger. 2016. CacheBleed: A Timing Attack on OpenSSL Constant Time RSA. Springer Berlin Heidelberg, 346--367."},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"e_1_3_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254078"},{"key":"e_1_3_2_2_73_1","doi-asserted-by":"crossref","unstructured":"Kehuan Zhang Zhou Li Rui Wang XiaoFeng Wang and Shuo Chen. 2010. Side- buster: Automated Detection and Quantification of Side-channel Leaks in Web Application Development. In Computer and Communications Security. ACM 595-- 606.","DOI":"10.1145\/1866307.1866374"},{"key":"e_1_3_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_22"}],"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.3134058","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134058","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134058","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.3134058"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,30]]},"references-count":74,"alternative-id":["10.1145\/3133956.3134058","10.1145\/3133956"],"URL":"https:\/\/doi.org\/10.1145\/3133956.3134058","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"}}]}}