{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:40:00Z","timestamp":1773193200262,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":92,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T00:00:00Z","timestamp":1636761600000},"content-version":"vor","delay-in-days":1,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1918573"],"award-info":[{"award-number":["CCF-1918573"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"CONIX Research Center"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,11,12]]},"DOI":"10.1145\/3460120.3484810","type":"proceedings-article","created":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T12:05:33Z","timestamp":1636805133000},"page":"429-444","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Solver-Aided Constant-Time Hardware Verification"],"prefix":"10.1145","author":[{"given":"Klaus","family":"v. Gleissenthall","sequence":"first","affiliation":[{"name":"Vrije Universiteit Amsterdam, Amsterdam, Netherlands"}]},{"given":"Rami G\u00f6khan","family":"K\u0131c\u0131","sequence":"additional","affiliation":[{"name":"University of California, San Diego, San Diego, CA, USA"}]},{"given":"Deian","family":"Stefan","sequence":"additional","affiliation":[{"name":"University of California, San Diego, San Diego, CA, USA"}]},{"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California, San Diego, San Diego, CA, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,11,13]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. BearSSL - Constant-Time Crypto. https:\/\/www.bearssl.org\/constanttime.html. (Accessed on 08\/19\/2020)."},{"key":"e_1_3_2_1_2_1","unstructured":"[n.d.]. fpga_mc\/fpu at master \u00b7monajalal\/fpga_mc \u00b7GitHub. https:\/\/github.com\/monajalal\/fpga_mc\/tree\/master\/fpu. (Accessed on 08\/16\/2020)."},{"key":"e_1_3_2_1_3_1","unstructured":"[n.d.]. GitHub - dawsonjon\/fpu: synthesiseable ieee 754 floating point library in verilog. https:\/\/github.com\/dawsonjon\/fpu. (Accessed on 08\/16\/2020)."},{"key":"e_1_3_2_1_4_1","unstructured":"[n.d.]. GitHub - scarv\/scarv-cpu: SCARV: a side-channel hardened RISC-V platform. https:\/\/github.com\/scarv\/scarv-cpu. (Accessed on 08\/16\/2020)."},{"key":"e_1_3_2_1_5_1","unstructured":"[n.d.]. GitHub - scarv\/xcrypto: XCrypto: a cryptographic ISE for RISC-V. https:\/\/github.com\/scarv\/xcrypto. (Accessed on 08\/19\/2020)."},{"key":"e_1_3_2_1_6_1","unstructured":"[n.d.]. GitHub - tommythorn\/yarvi: Yet Another RISC-V Implementation. https:\/\/github.com\/tommythorn\/yarvi. (Accessed on 08\/16\/2020)."},{"key":"e_1_3_2_1_7_1","unstructured":"[n.d.]. GLPK - GNU Project - Free Software Foundation (FSF). https:\/\/www.gnu.org\/software\/glpk\/. (Accessed on 08\/10\/2020)."},{"key":"e_1_3_2_1_8_1","unstructured":"[n.d.]. liquid-fixpoint: Horn Clause Constraint Solving for Liquid Types. https:\/\/github.com\/ucsd-progsys\/liquid-fixpoint. Accessed: 2018-08--29."},{"key":"e_1_3_2_1_9_1","unstructured":"[n.d.]. MIPS. https:\/\/github.com\/gokhankici\/iodine\/tree\/master\/benchmarks\/472-mips-pipelined. (Accessed on 08\/16\/2020)."},{"key":"e_1_3_2_1_10_1","unstructured":"[n.d.]. Overview :: AES :: OpenCores. https:\/\/opencores.org\/projects\/tiny_aes. (Accessed on 08\/05\/2020)."},{"key":"e_1_3_2_1_11_1","unstructured":"[n.d.]. Overview :: SHA cores :: OpenCores. https:\/\/opencores.org\/projects\/sha_core. (Accessed on 08\/16\/2020)."},{"key":"e_1_3_2_1_12_1","unstructured":"[n.d.]. TIS-CT. http:\/\/trust-in-soft.com\/tis-ct\/."},{"key":"e_1_3_2_1_13_1","volume-title":"IEEE Standard for Verilog Hardware Description Language","year":"2005","unstructured":"2005. IEEE Standard for Verilog Hardware Description Language. IEEE Std 1364--2005."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837628"},{"key":"e_1_3_2_1_15_1","volume-title":"USENIX Security Symposium.","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 USENIX Security Symposium."},{"key":"e_1_3_2_1_16_1","unstructured":"Jos\u00e9 Bacelar Almeida Manuel Barbosa Gilles Barthe Fran\u00e7ois Dupressoir and Michael Emmi. 2016. Verifying Constant-Time Implementations. In USENIX Security."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"J Bacelar Almeida Manuel Barbosa Jorge S Pinto and B\u00e1rbara Vieira. 2013. Formal verification of side-channel countermeasures using self-composition In Science of Computer Programming. Science of Computer Programming.","DOI":"10.1016\/j.scico.2011.10.008"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Marc Andrysco David Kohlbrenner Keaton Mowery Ranjit Jhala Sorin Lerner and Hovav Shacham. 2015. On subnormal floating point and abnormal timing. In S&P.","DOI":"10.1109\/SP.2015.44"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243766"},{"key":"e_1_3_2_1_21_1","volume-title":"SoK: Computer-Aided Cryptography. In IEEE Symposium on Security and Privacy.","author":"Barbosa Manuel","year":"2021","unstructured":"Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. 2021. SoK: Computer-Aided Cryptography. In IEEE Symposium on Security and Privacy."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660283"},{"key":"e_1_3_2_1_23_1","unstructured":"Daniel J. Bernstein. 2005. Cache-timing attacks on AES. Technical Report. https:\/\/cr.yp.to\/antiforgery\/cachetiming-20050414.pdf"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Nikolaj Bj\u00f8rner Arie Gurfinkel Ken McMillan and Andrey Rybalchenko. 2015. Horn Clause Solvers for Program Verification. In Fields of Logic and Computation.","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_3_2_1_25_1","volume-title":"Workshop on Offensive Technologies.","author":"Brasser Ferdinand","year":"2017","unstructured":"Ferdinand Brasser, Urs M\u00fcller, Alexandra Dmitrienko, Kari Kostiainen, Srdjan Capkun, and Ahmad-Reza Sadeghi. 2017. Software grand exposure:SGX cache attacks are practical. In Workshop on Offensive Technologies."},{"key":"e_1_3_2_1_26_1","volume-title":"Remote timing attacks are practical. Computer Networks","author":"Brumley David","year":"2005","unstructured":"David Brumley and Dan Boneh. 2005. Remote timing attacks are practical. Computer Networks (2005)."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Cristiano Calcagno Dino Distefano Peter W. O'Hearn and Hongseok Yang. [n.d.]. Compositional Shape Analysis by Means of Bi-Abduction. 58 6 ([n. d.]) 26:1--26:66. https:\/\/doi.org\/10.1145\/2049697.2049700","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Sunjay Cauligi Craig Disselkoen Klaus von Gleissenthall Dean Tullsen Deian Stefan Tamara Rzk and Gilles Barthe. 2020. Constant-time foundations for the new Spectre era. In Programming Language Design and Implementation (PLDI). ACM SIGPLAN.","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Sunjay Cauligi Gary Soeller Brian Johannesmeyer Fraser Brown Riad S. Wahby John Renner Benjamin Gregoire Gilles Barthe Ranjit Jhala and Deian Stefan. 2019. FaCT: A DSL for timing-sensitive computation. In Programming Language Design and Implementation (PLDI). ACM SIGPLAN.","DOI":"10.1145\/3314221.3314605"},{"key":"e_1_3_2_1_30_1","volume-title":"Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification. In International Conference on Functional Programming (ICFP). ACM SIGPLAN","author":"Choi Joonwon","year":"2017","unstructured":"Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. 2017. Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification. In International Conference on Functional Programming (ICFP). ACM SIGPLAN. http:\/\/plv.csail.mit.edu\/kami\/papers\/icfp17.pdf"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--35873--9_13"},{"key":"e_1_3_2_1_32_1","volume-title":"Schneider","author":"Clarkson Michael R.","year":"2010","unstructured":"Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. Journal of Computer Security (2010)."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00046"},{"key":"e_1_3_2_1_34_1","unstructured":"CHC competition (CHC-COMP). [n.d.]. ."},{"key":"e_1_3_2_1_35_1","first-page":"2","article-title":"CacheQuote: Efficiently Recovering Long-term Secrets of SGX EPID via Cache Attacks","volume":"2018","author":"Dall Fergus","year":"2018","unstructured":"Fergus Dall, Gabrielle De Micheli, Thomas Eisenbarth, Daniel Genkin, Nadia Heninger, Ahmad Moghimi, and Yuval Yarom. 2018. CacheQuote: Efficiently Recovering Long-term Secrets of SGX EPID via Cache Attacks. IACR Transactions on Cryptographic Hardware and Embedded Systems 2018, 2 (May 2018).","journal-title":"IACR Transactions on Cryptographic Hardware and Embedded Systems"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00074"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254087"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509511"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Isil Dillig Thomas Dillig Boyang Li Ken McMillan and Mooly Sagiv. [n.d.]. Synthesis of Circular Compositional Program Proofs via Abduction. 19 5 ([n. d.]) 535--547. https:\/\/doi.org\/10.1007\/s10009-015-0397--7","DOI":"10.1007\/s10009-015-0397--7"},{"key":"e_1_3_2_1_41_1","volume-title":"Cacheaudit: A tool for the static analysis of cache side channels. In USENIX Security.","author":"Doychev Goran","year":"2013","unstructured":"Goran Doychev, Dominik Feld, Boris K\u00f6pf, Laurent Mauborgne, and Jan Reineke. 2013. Cacheaudit: A tool for the static analysis of cache side channels. In USENIX Security."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--32759--9_17"},{"key":"e_1_3_2_1_43_1","unstructured":"Mohammad Rahmani Fadiheh Johannes M\u00fcller Raik Brinkmann Subhasish Mitra Dominik Stoffel and Wolfgang Kunz. 2020. A Formal Approach for Detecting Vulnerabilities to Transient Execution Attacks in Out-of-Order Processors. In DAC."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Grigory Fedyukovich Sumanth Prabhu Kumar Madhukar and Aarti Gupta. 2018. Solving Constrained Horn Clauses Using Syntax and Data. In FMCAD.","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Andrew Ferraiuolo Mark Zhao Andrew C Myers and G Edward Suh. 2018. HyperFlow: A processor architecture for nonmalleable timing-safe information flow security. In SIGSAC.","DOI":"10.1145\/3243734.3243743"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3--540--45251--6_29"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--319-08867--9_5"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/200616.200649"},{"key":"e_1_3_2_1_50_1","volume-title":"IODINE: Verifying Constant-Time Execution of Hardware. In USENIX Conference on Security Symposium.","author":"Gleissenthall Klaus V.","year":"2019","unstructured":"Klaus V. Gleissenthall, Rami G\u00f6khan Kici, Deian Stefan, and Ranjit Jhala. 2019. IODINE: Verifying Constant-Time Execution of Hardware. In USENIX Conference on Security Symposium."},{"key":"e_1_3_2_1_51_1","unstructured":"Michael J. C. Gordon. 1995. The semantic challenge of Verilog HDL. In LICS."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"crossref","unstructured":"Sergey Grebenshchikov Nuno P. Lopes Corneliu Popeea and Andrey Rybalchenko. 2012. Synthesizing software verifiers from proof rules.. In PLDI.","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"crossref","unstructured":"Marco Guarnieri Boris Koepf Jan Reineke and Pepe Vila. 2021. Hardware- Software Contracts for Secure Speculation. In S&P.","DOI":"10.1109\/SP40001.2021.00036"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0050-0"},{"key":"e_1_3_2_1_55_1","volume-title":"Navas","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In CAV."},{"key":"e_1_3_2_1_56_1","unstructured":"Andreas Haeberlen Benjamin C. Pierce and Arjun Narayan. 2011. Differential Privacy under Fire. In USENIX Security David Wagner (Ed.)."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"crossref","unstructured":"Hossein Hojjat and Philipp R\u00fcmmer. 2018. The Eldarica Horn Solver. In FMCAD.","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--319--10575--8_15"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--22110--1_40"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993550"},{"key":"e_1_3_2_1_61_1","unstructured":"Rami G\u00f6khan Kici. 2020. Personal communication."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"crossref","unstructured":"Paul C Kocher. 1996. Timing attacks on implementations of Diffie-Hellman RSA DSS and other systems. In CRYPTO.","DOI":"10.1007\/3-540-68697-5_9"},{"key":"e_1_3_2_1_63_1","unstructured":"David Kohlbrenner and Hovav Shacham. 2017. On the effectiveness of mitigations against floating-point timing channels. In USENIX Security."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"crossref","unstructured":"Hyoukjun Kwon William Harris and Hadi Esameilzadeh. 2017. Proving Flow Security of Sequential Logic via Automatically-Synthesized Relational Invariants. In CSF.","DOI":"10.1109\/CSF.2017.35"},{"key":"e_1_3_2_1_65_1","unstructured":"Adam Langley. [n.d.]. ctgrind: Checking that functions are constant time with Valgrind. https:\/\/github.com\/agl\/ctgrind\/."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"crossref","unstructured":"Xun Li Mohit Tiwari Jason K Oberg Vineeth Kashyap Frederic T Chong Timothy Sherwood and Ben Hardekopf. 2011. Caisson: a hardware description language for secure information flow. In PLDI.","DOI":"10.1145\/1993498.1993512"},{"key":"e_1_3_2_1_67_1","volume-title":"Martin Maas, Michael Hicks, Mohit Tiwari, and Elaine Shi.","author":"Liu Chang","year":"2015","unstructured":"Chang Liu, Austin Harris, Martin Maas, Michael Hicks, Mohit Tiwari, and Elaine Shi. 2015. Ghostrider: A hardware-software system for memory trace oblivious computation. SIGPLAN Notices (2015)."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542485"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/3--540--63166--6_6"},{"key":"e_1_3_2_1_70_1","unstructured":"Daniel Moghimi Berk Sunar Thomas Eisenbarth and Nadia Heninger. 2020. TPM-FAIL:TPM meets Timing and Lattice Attacks. In USENIX Security."},{"key":"e_1_3_2_1_71_1","volume-title":"Cryptographers' Track at the RSA Conference","author":"Osvik Dag Arne","unstructured":"Dag Arne Osvik, Adi Shamir, and Eran Tromer. 2006. Cache attacks and countermeasures: the case of AES. In Cryptographers' Track at the RSA Conference. Springer."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_3_2_1_73_1","volume-title":"Papadimitriou and Kenneth Steiglitz","author":"Christos","year":"1982","unstructured":"Christos H. Papadimitriou and Kenneth Steiglitz. 1982. Combinatorial Optimization: Algorithms and Complexity. Prentice-Hall, Inc., USA."},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"crossref","unstructured":"Sumanth Prabhu Grigory Fedyukovich Kumar Madhukar and Deepak D'Souza. 2021. Specification Synthesis with Constrained Horn Clauses. In PLDI.","DOI":"10.1145\/3453483.3454104"},{"key":"e_1_3_2_1_75_1","volume-title":"Raccoon: Closing Digital Side-Channels through Obfuscated Execution.. In USENIX Security.","author":"Rane Ashay","year":"2015","unstructured":"Ashay Rane, Calvin Lin, and Mohit Tiwari. 2015. Raccoon: Closing Digital Side-Channels through Obfuscated Execution.. In USENIX Security."},{"key":"e_1_3_2_1_76_1","unstructured":"Ashay Rane Calvin Lin and Mohit Tiwari. 2016. Secure Precise and Fast Floating-Point Operations on x86 Processors. In USENIX Security."},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"crossref","unstructured":"Oscar Reparaz Joseph Balasch and Ingrid Verbauwhede. 2017. Dude is my code constant time?. In DATE.","DOI":"10.23919\/DATE.2017.7927267"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_2_1_79_1","volume-title":"Fernando Magno Quint\u00e3o Pereira, and Diego F Aranha","author":"Rodrigues Bruno","year":"2016","unstructured":"Bruno Rodrigues, Fernando Magno Quint\u00e3o Pereira, and Diego F Aranha. 2016. Sparse representation of implicit flows with applications to side-channel detection. In CCC."},{"key":"e_1_3_2_1_80_1","volume-title":"Advances in Neural Information Processing Systems 31","author":"Si Xujie","unstructured":"Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song. [n.d.]. Learning Loop Invariants for Program Verification. In Advances in Neural Information Processing Systems 31, S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (Eds.). Curran Associates, Inc., 7751--7762. http:\/\/papers.nips.cc\/paper\/8001-learning-loop-invariants-for-program-verification.pdf"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--53291--8_9"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"crossref","unstructured":"Mohit Tiwari Jason K Oberg Xun Li Jonathan Valamehr Timothy Levin Ben Hardekopf Ryan Kastner Frederic T. Chong and Timothy Sherwood. 2011.Crafting a Usable Microkernel Processor and I\/O System with Strict and Provable Information Flow Security. In ISCA.","DOI":"10.1145\/2000064.2000087"},{"key":"e_1_3_2_1_83_1","volume-title":"Bita Mazloom, Shashidhar Mysore, Frederic T Chong, and Timothy Sherwood.","author":"Tiwari Mohit","year":"2009","unstructured":"Mohit Tiwari, Hassan MG Wassel, Bita Mazloom, Shashidhar Mysore, Frederic T Chong, and Timothy Sherwood. 2009. Complete information flow tracking from the gates up. In Sigplan Notices."},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--319--21668--3_7"},{"key":"e_1_3_2_1_85_1","doi-asserted-by":"crossref","unstructured":"Conrad Watt John Renner Natalie Popescu Sunjay Cauligi and Deian Stefan. 2019. CT-Wasm: Type-driven Secure Cryptography for the Web Ecosystem. POPL.","DOI":"10.1145\/3290390"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1109\/tse.2016.2521368"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134016"},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-017-0152-y"},{"key":"e_1_3_2_1_89_1","volume-title":"Mohamad El Hajj, and Christopher W Fletcher","author":"Yu Jiyong","year":"2019","unstructured":"Jiyong Yu, Lucas Hsiung, Mohamad El Hajj, and Christopher W Fletcher. 2019. Data Oblivious ISA Extensions for Side Channel-Resistant and High Performance Computing. In NDSS."},{"key":"e_1_3_2_1_90_1","volume-title":"Myers","author":"Zhang Danfeng","year":"2012","unstructured":"Danfeng Zhang, Aslan Askarov, and Andrew C. Myers. 2012. Language-based control and mitigation of timing channels. In PLDI."},{"key":"e_1_3_2_1_91_1","volume-title":"Myers","author":"Zhang Danfeng","year":"2015","unstructured":"Danfeng Zhang, Yao Wang, G. Edward Suh, and Andrew C. Myers. 2015. A Hardware Design Language for Timing-Sensitive Information-Flow Security. In ASPLOS."},{"key":"e_1_3_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--39322--9_10"}],"event":{"name":"CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security","location":"Virtual Event Republic of Korea","acronym":"CCS '21","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484810","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484810","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484810","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T20:48:02Z","timestamp":1763498882000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484810"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,12]]},"references-count":92,"alternative-id":["10.1145\/3460120.3484810","10.1145\/3460120"],"URL":"https:\/\/doi.org\/10.1145\/3460120.3484810","relation":{},"subject":[],"published":{"date-parts":[[2021,11,12]]},"assertion":[{"value":"2021-11-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}