{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:05Z","timestamp":1780994525000,"version":"3.54.1"},"reference-count":91,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K008528\/1"],"award-info":[{"award-number":["EP\/K008528\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>A significant amount of both client and server-side cryptography is implemented in JavaScript. Despite widespread concerns about its security, no other language has been able to match the convenience that comes from its ubiquitous support on the \"web ecosystem\" - the wide variety of technologies that collectively underpins the modern World Wide Web. With the introduction of the new WebAssembly bytecode language (Wasm) into the web ecosystem, we have a unique opportunity to advance a principled alternative to existing JavaScript cryptography use cases which does not compromise this convenience.<\/jats:p>\n          <jats:p>We present Constant-Time WebAssembly (CT-Wasm), a type-driven, strict extension to WebAssembly which facilitates the verifiably secure implementation of cryptographic algorithms. CT-Wasm's type system ensures that code written in CT-Wasm is both information flow secure and resistant to timing side channel attacks; like base Wasm, these guarantees are verifiable in linear time. Building on an existing Wasm mechanization, we mechanize the full CT-Wasm specification, prove soundness of the extended type system, implement a verified type checker, and give several proofs of the language's security properties.<\/jats:p>\n          <jats:p>We provide two implementations of CT-Wasm: an OCaml reference interpreter and a native implementation for Node.js and Chromium that extends Google's V8 engine. We also implement a CT-Wasm to Wasm rewrite tool that allows developers to reap the benefits of CT-Wasm's type system today, while developing cryptographic algorithms for base Wasm environments. We evaluate the language, our implementations, and supporting tools by porting several cryptographic primitives - Salsa20, SHA-256, and TEA - and the full TweetNaCl library. We find that CT-Wasm is fast, expressive, and generates code that we experimentally measure to be constant-time.<\/jats:p>","DOI":"10.1145\/3290390","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":55,"title":["CT-wasm: type-driven secure cryptography for the web ecosystem"],"prefix":"10.1145","volume":"3","author":[{"given":"Conrad","family":"Watt","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Renner","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Natalie","family":"Popescu","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sunjay","family":"Cauligi","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Deian","family":"Stefan","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-52993-5_9"},{"key":"e_1_2_2_3_1","volume-title":"Proceedings of the USENIX Security Symposium. USENIX Association.","author":"Almeida Jose Bacelar","year":"2016"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.44"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243766"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_2_2_7_1","volume-title":"Silva","author":"Barbosa Manuel","year":"2014"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29320-7_21"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660283"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00031"},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Daniel J Bernstein. 2005","DOI":"10.2307\/j.ctvmx3j3j.105"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11502760_3"},{"key":"e_1_2_2_14_1","first-page":"a20","volume":"2005","journal-title":"Daniel J Bernstein."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11745853_14"},{"key":"e_1_2_2_16_1","unstructured":"Daniel J Bernstein. 200"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68351-3_8"},{"key":"e_1_2_2_18_1","volume-title":"Retrieved","author":"Bernstein Daniel J","year":"2016"},{"key":"e_1_2_2_19_1","volume-title":"Proceedings of the International Conference on Cryptology and Information Security in Latin America. Springer.","author":"Bernstein Daniel J","year":"2014"},{"key":"e_1_2_2_20_1","unstructured":"Benjamin Beurdouche. 2017. Verified cryptography for Firefox 57. (2017). https:\/\/blog.mozilla.org\/security\/2017\/09\/13\/ verified-cryptography-firefox-57\/  Benjamin Beurdouche. 2017. Verified cryptography for Firefox 57. (2017). https:\/\/blog.mozilla.org\/security\/2017\/09\/13\/ verified-cryptography-firefox-57\/"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","volume-title":"Defensive JavaScript","author":"Bhargavan Karthikeyan","DOI":"10.1007\/978-3-319-10082-1_4"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66402-6_16"},{"key":"e_1_2_2_23_1","volume-title":"Proceedings of the USENIX Security Symposium. USENIX Association.","author":"Bond Barry","year":"2017"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.12.007"},{"key":"e_1_2_2_25_1","volume-title":"Remote timing attacks are practical. Computer Networks 48, 5","author":"Brumley David","year":"2005"},{"key":"e_1_2_2_26_1","volume-title":"Retrieved","author":"Bubelich Mykola","year":"2017"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SecDev.2017.24"},{"key":"e_1_2_2_28_1","volume-title":"Retrieved","author":"Chestnykh Dmitry","year":"2016"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/202529.202534"},{"key":"e_1_2_2_30_1","volume-title":"crypto-algorithms. (2012). Retrieved","author":"Conte Brad","year":"2018"},{"key":"e_1_2_2_31_1","volume-title":"Retrieved","author":"Cousens Daniel","year":"2014"},{"key":"e_1_2_2_32_1","volume-title":"Retrieved","author":"Standard Cryptography Coding","year":"2016"},{"key":"e_1_2_2_33_1","volume-title":"JavaScript everywhere and \u201cthe three amigos\".","author":"Cuomo Jerry","year":"2013"},{"key":"e_1_2_2_34_1","volume-title":"Retrieved","year":"2018"},{"key":"e_1_2_2_35_1","unstructured":"ECMA International. 2018. ECMAScript 2018 Language Specification. (2018). https:\/\/www.ecma-international.org\/ publications\/files\/ECMA-ST\/Ecma-262.pdf  ECMA International. 2018. ECMAScript 2018 Language Specification. (2018). https:\/\/www.ecma-international.org\/ publications\/files\/ECMA-ST\/Ecma-262.pdf"},{"key":"e_1_2_2_36_1","volume-title":"Without Compromises. In Proceedings of the IEEE Symposium on Security and Privacy.","author":"Erbsen Andres","year":"2019"},{"key":"e_1_2_2_38_1","volume-title":"Cryptol: The Language of Cryptography. https:\/\/cryptol.net\/files\/ProgrammingCryptol.pdf .","year":"2016"},{"key":"e_1_2_2_39_1","volume-title":"Retrieved","author":"Green Matthew","year":"2012"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_2_2_41_1","volume-title":"Proceedings of the International Workshop on Web APIs and RESTful design.","author":"Halpin Harry","year":"2014"},{"key":"e_1_2_2_42_1","volume-title":"asm.js. (2014). Retrieved","author":"Herman David","year":"2017"},{"key":"e_1_2_2_43_1","volume-title":"Finding efficient distinguishers for cryptographic mappings, with an application to the block cipher TEA. Computational Intelligence 20, 3","author":"Hernandez Julio C","year":"2004"},{"key":"e_1_2_2_44_1","volume-title":"Quotient Types. In Supplemental Proceedings of the International Conference on Theorem Proving in Higher Order Logics","author":"Homeier Peter V.","year":"2001"},{"key":"e_1_2_2_45_1","volume-title":"Proceedings of the International Conference on Information Security and Cryptology. Springer.","author":"Hong Seokhie","year":"2003"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"e_1_2_2_47_1","volume-title":"Retrieved","author":"Indutny Fedor","year":"2014"},{"key":"e_1_2_2_48_1","volume-title":"A-Z","year":"2016"},{"key":"e_1_2_2_49_1","volume-title":"sha.js. (2017). Retrieved","author":"Johnston Paul","year":"2018"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/646277.687180"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.38"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/646761.706156"},{"key":"e_1_2_2_53_1","volume-title":"Proceedings of the USENIX Security Symposium. USENIX Association.","author":"Kohlbrenner David","year":"2017"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/794200.795152"},{"key":"e_1_2_2_56_1","volume-title":"Retrieved","year":"2018"},{"key":"e_1_2_2_57_1","volume-title":"Retrieved","year":"2018"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292561"},{"key":"e_1_2_2_59_1","volume-title":"Jif: Java information flow. Software release. Located at http:\/\/www. cs. cornell. edu\/jif 2005","author":"Myers Andrew C","year":"2001"},{"key":"e_1_2_2_60_1","volume-title":"Retrieved","author":"Ndegwa Amos","year":"2016"},{"key":"e_1_2_2_61_1","volume-title":"Retrieved","author":"Sneff Lachlan","year":"2018"},{"key":"e_1_2_2_62_1","first-page":"2","volume":"18","author":"NIST.","year":"2002","journal-title":"Secure Hash Standard. FIPS PUB"},{"key":"e_1_2_2_63_1","volume-title":"Retrieved","year":"2018"},{"key":"e_1_2_2_64_1","volume-title":"Retrieved","author":"Systems Open Whisper","year":"2016"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813708"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/11605805_1"},{"key":"e_1_2_2_67_1","unstructured":"D. Page. 2006. A Note On Side-Channels Resulting From Dynamic Compilation. In Cryptology ePrint Archive. https: \/\/eprint.iacr.org\/2006\/349  D. Page. 2006. A Note On Side-Channels Resulting From Dynamic Compilation. In Cryptology ePrint Archive. https: \/\/eprint.iacr.org\/2006\/349"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_11"},{"key":"e_1_2_2_69_1","volume-title":"Retrieved","author":"Pornin Thomas","year":"2017"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"e_1_2_2_71_1","volume-title":"Retrieved","author":"Everest Project","year":"2018"},{"key":"e_1_2_2_72_1","unstructured":"John Renner Sunjay Cauligi and Deian Stefan. 2018. Constant-Time WebAssembly. In Principles of Secure Compilation.  John Renner Sunjay Cauligi and Deian Stefan. 2018. Constant-Time WebAssembly. In Principles of Secure Compilation."},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.5555\/3130379.3130776"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.5555\/794200.795151"},{"key":"e_1_2_2_76_1","unstructured":"Ryan Sleevi. 2013. W3C Web Crypto API Update. (2013). https:\/\/datatracker.ietf.org\/meeting\/86\/materials\/slides-86-saag-5 IETF 86.  Ryan Sleevi. 2013. W3C Web Crypto API Update. (2013). https:\/\/datatracker.ietf.org\/meeting\/86\/materials\/slides-86-saag-5 IETF 86."},{"key":"e_1_2_2_77_1","volume-title":"Retrieved","author":"Strohmeier Dominik","year":"2017"},{"key":"e_1_2_2_78_1","volume-title":"https:\/\/github.com\/TorstenStueber\/TweetNacl-WebAssembly","author":"St\u00fcber Torsten","year":"2017"},{"key":"e_1_2_2_79_1","volume-title":"Retrieved","author":"Tarr Dominic","year":"2013"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/2430532.2364524"},{"key":"e_1_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813632"},{"key":"e_1_2_2_82_1","volume-title":"A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4, 2-3","author":"Volpano Dennis","year":"1996"},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167082"},{"key":"e_1_2_2_84_1","doi-asserted-by":"crossref","unstructured":"Conrad Watt John Renner Natalie Popescu Sunjay Cauligi and Deian Stefan. 2018. CT-Wasm: Type-driven Secure Cryptography for the Web Ecosystem. (2018). http:\/\/ct-wasm.programming.systems\/  Conrad Watt John Renner Natalie Popescu Sunjay Cauligi and Deian Stefan. 2018. CT-Wasm: Type-driven Secure Cryptography for the Web Ecosystem. (2018). http:\/\/ct-wasm.programming.systems\/","DOI":"10.1145\/3290390"},{"key":"e_1_2_2_85_1","volume-title":"Retrieved","author":"WebAssembly Community Group","year":"2018"},{"key":"e_1_2_2_86_1","volume-title":"Retrieved","author":"WebAssembly Community Group","year":"2018"},{"key":"e_1_2_2_87_1","volume-title":"Retrieved","author":"WebAssembly Community Group","year":"2018"},{"key":"e_1_2_2_88_1","volume-title":"Retrieved","author":"WebAssembly Community Group","year":"2018"},{"key":"e_1_2_2_89_1","volume-title":"Needham","author":"Wheeler David J.","year":"1994"},{"key":"e_1_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_91_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.25"},{"key":"e_1_2_2_92_1","volume-title":"Retrieved","author":"Zakai Alon","year":"2015"},{"key":"e_1_2_2_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290390","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290390","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290390"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":91,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290390"],"URL":"https:\/\/doi.org\/10.1145\/3290390","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}