Conrad Watt
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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.
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.
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.
Supplemental Material
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-assurance and high-speed cryptography. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. ACM. Google Scholar
Digital Library
- José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and François Dupressoir. 2016a. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. In Revised Selected Papers of the International Conference on Fast Software Encryption. Springer-Verlag New York, Inc. Google ScholarDigital Library
- Jose Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. 2016b. Verifying ConstantTime Implementations. In Proceedings of the USENIX Security Symposium. USENIX Association. Google ScholarDigital Library
- Marc Andrysco, David Kohlbrenner, Keaton Mowery, Ranjit Jhala, Sorin Lerner, and Hovav Shacham. 2015. On Subnormal Floating Point and Abnormal Timing. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society. Google ScholarDigital Library
- Marc Andrysco, Andres Nötzli, Fraser Brown, Ranjit Jhala, and Deian Stefan. 2018. Towards Verified, Constant-time Floating Point Operations. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. ACM. Google ScholarDigital Library
- Roberto Baldoni, Emilio Coppa, Daniele Cono D’Elia, Camil Demetrescu, and Irene Finocchi. 2018. A Survey of Symbolic Execution Techniques. Comput. Surveys 51, 3, Article 50 (2018). Google ScholarDigital Library
- Manuel Barbosa, David Castro, and Paulo F. Silva. 2014. Compiling CAO: From Cryptographic Specifications to C Implementations. In Proceedings of Principles of Security and Trust, Martín Abadi and Steve Kremer (Eds.). Springer Berlin Heidelberg.Google Scholar
- Manuel Barbosa, Andrew Moss, Dan Page, Nuno F. Rodrigues, and Paulo F. Silva. 2012. Type Checking Cryptography Implementations. In Fundamentals of Software Engineering, Farhad Arbab and Marjan Sirjani (Eds.). Springer Berlin Heidelberg. Google ScholarDigital Library
- Gilles Barthe, Gustavo Betarte, Juan Campo, Carlos Luna, and David Pichardie. 2014. System-level Non-interference for Constant-time Cryptography. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. ACM. Google ScholarDigital Library
- Gilles Barthe, Benjamin Grégoire, and Vincent Laporte. 2017. Provably secure compilation of side-channel countermeasures. Cryptology ePrint Archive, Report 2017/1233. (2017). https://eprint.iacr.org/2017/1233 .Google Scholar
- Gilles Barthe, Benjamin Grégoire, and Vincent Laporte. 2018. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”. In Proceedings of the IEEE Computer Security Foundations Symposium. IEEE Computer Society.Google ScholarCross Ref
- Daniel J Bernstein. 2005a. Cache-timing attacks on AES. (2005).Google Scholar
- Daniel J Bernstein. 2005b. The Poly1305-AES message-authentication code. In Proceedings of the International Workshop on Fast Software Encryption. Springer. Google ScholarDigital Library
- Daniel J Bernstein. 2005c. salsa20-ref.c. (2005). Retrieved July 5, 2018 from https://cr.yp.to/snuffle/salsa20/ref/salsa20.cGoogle Scholar
- Daniel J Bernstein. 2006. Curve25519: new Diffie-Hellman speed records. In Proceedings of the International Workshop on Public Key Cryptography. Springer. Google ScholarDigital Library
- Daniel J Bernstein. 2007. Writing high-speed software. (2007). Retrieved June 11, 2018 from http://cr.yp.to/qhasm.htmlGoogle Scholar
- Daniel J Bernstein. 2008. The Salsa20 family of stream ciphers. In New stream cipher designs. Springer. Google ScholarDigital Library
- Daniel J Bernstein, Tanja Lange, and Peter Schwabe. 2016. NaCl: Networking and cryptography library. (2016). Retrieved June 23, 2018 from https://nacl.cr.yp.toGoogle Scholar
- Daniel J Bernstein, Bernard Van Gastel, Wesley Janssen, Tanja Lange, Peter Schwabe, and Sjaak Smetsers. 2014. TweetNaCl: A crypto library in 100 tweets. In Proceedings of the International Conference on Cryptology and Information Security in Latin America. Springer.Google Scholar
- Benjamin Beurdouche. 2017. Verified cryptography for Firefox 57. (2017). https://blog.mozilla.org/security/2017/09/13/ verified-cryptography-firefox-57/Google Scholar
- Karthikeyan Bhargavan, Antoine Delignat-Lavaud, and Sergio Maffeis. 2014. Defensive JavaScript. In Foundations of Security Analysis and Design VII. Springer.Google Scholar
- Sandrine Blazy, David Pichardie, and Alix Trieu. 2017. Verifying Constant-Time Implementations by Abstract Interpretation. In Proceedings of the European Symposium on Research in Computer Security, Simon N. Foley, Dieter Gollmann, and Einar Snekkenes (Eds.). Springer International Publishing.Google ScholarCross Ref
- Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In Proceedings of the USENIX Security Symposium. USENIX Association. Google ScholarDigital Library
- Michele Boreale. 2009. Quantifying Information Leakage in Process Calculi. Information and Computation 207, 6 (2009). Google ScholarDigital Library
- David Brumley and Dan Boneh. 2005. Remote timing attacks are practical. Computer Networks 48, 5 (2005). Google ScholarDigital Library
- Mykola Bubelich. 2017. JS-Salsa20. (2017). Retrieved July 5, 2018 from https://www.npmjs.com/package/js-salsa20Google Scholar
- Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, and Deian Stefan. 2017. FaCT: A Flexible, Constant-Time Programming Language. In Proceedings of the IEEE Cybersecurity Development Conference. IEEE.Google ScholarCross Ref
- Dmitry Chestnykh. 2016. TweetNaCl.js. (2016). Retrieved June 23, 2018 from https://www.npmjs.com/package/tweetnaclGoogle Scholar
- Cliff Click and Michael Paleczny. 1995. A Simple Graph-based Intermediate Representation. In Proceedings of the ACM SIGPLAN Workshop on Intermediate Representations. ACM. Google ScholarDigital Library
- Brad Conte. 2012. crypto-algorithms. (2012). Retrieved July 5, 2018 from https://github.com/B-Con/crypto-algorithmsGoogle Scholar
- Daniel Cousens. 2014. pbkdf2. (2014). Retrieved June 23, 2018 from https://www.npmjs.com/package/pbkdf2Google Scholar
- Cryptography Coding Standard. 2016. Coding rules. (2016). Retrieved June 11, 2018 from https://cryptocoding.net/index. php/Coding_rulesGoogle Scholar
- Jerry Cuomo. 2013. Mobile app development, JavaScript everywhere and “the three amigos". (2013). White paper, IBM.Google Scholar
- Denis, Frank. 2018. libsodium. (2018). Retrieved July 12, 2018 from https://github.com/jedisct1/libsodiumGoogle Scholar
- ECMA International. 2018. ECMAScript 2018 Language Specification. (2018). https://www.ecma-international.org/ publications/files/ECMA-ST/Ecma-262.pdfGoogle Scholar
- Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple High-Level Code For Cryptographic Arithmetic – With Proofs, Without Compromises. In Proceedings of the IEEE Symposium on Security and Privacy.Google Scholar
- Richard Forster. 1999. Non-Interference Properties for Nondeterministic Processes. Ph.D. Dissertation. University of Cambridge.Google Scholar
- Galois. 2016. Cryptol: The Language of Cryptography. https://cryptol.net/files/ProgrammingCryptol.pdf . (2016).Google Scholar
- Matthew Green. 2012. The anatomy of a bad idea. (2012). Retrieved June 23, 2018 from https://blog.cryptographyengineering. com/2012/12/28/the-anatomy-of-bad-idea/Google Scholar
- Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017. Bringing the Web Up to Speed with WebAssembly. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM. Google ScholarDigital Library
- Harry Halpin. 2014. The W3C Web Cryptography API: Design and Issues. In Proceedings of the International Workshop on Web APIs and RESTful design.Google Scholar
- David Herman, Luke Wagner, and Alon Zakai. 2014. asm.js. (2014). Retrieved October 7, 2017 from http://asmjs.org/spec/ latestGoogle Scholar
- Julio C Hernandez and Pedro Isasi. 2004. Finding efficient distinguishers for cryptographic mappings, with an application to the block cipher TEA. Computational Intelligence 20, 3 (2004).Google Scholar
- Peter V. Homeier. 2001. Quotient Types. In Supplemental Proceedings of the International Conference on Theorem Proving in Higher Order Logics. University of Edinburgh.Google Scholar
- Seokhie Hong, Deukjo Hong, Youngdai Ko, Donghoon Chang, Wonil Lee, and Sangjin Lee. 2003. Differential Cryptanalysis of TEA and XTEA. In Proceedings of the International Conference on Information Security and Cryptology. Springer.Google Scholar
- Brian Huffman and Ondřej Kunăar. 2013. Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. In Proceedings of the ACM SIGPLAN International Conference on Certified Programs and Proofs. Springer-Verlag. Google ScholarDigital Library
- Fedor Indutny. 2014. Elliptic. (2014). Retrieved June 23, 2018 from https://www.npmjs.com/package/ellipticGoogle Scholar
- Intel. 2016. Intel® 64 and IA-32 Architectures Software Developer’s Manual. Volume 2: Instruction Set Reference, A-Z (2016).Google Scholar
- Paul Johnston and Contributors. 2017. sha.js. (2017). Retrieved July 5, 2018 from https://www.npmjs.com/package/sha.jsGoogle Scholar
- John Kelsey, Bruce Schneier, and David Wagner. 1997. Related-key cryptanalysis of 3-way, biham-des, cast, des-x, newdes, rc2, and tea. In Proceedings of the International Conference on Information and Communications Security. Springer. Google ScholarDigital Library
- Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. 2017. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In Proceedings of the IEEE European Symposium on Security and Privacy. IEEE Computer Society.Google ScholarCross Ref
- Paul Kocher. 1996. Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In Proceedings of Advances in Cryptology. Springer. Google ScholarDigital Library
- David Kohlbrenner and Hovav Shacham. 2017. On the effectiveness of mitigations against floating-point timing channels. In Proceedings of the USENIX Security Symposium. USENIX Association. Google ScholarDigital Library
- K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Proceedings of the International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer. Google ScholarDigital Library
- Heiko Mantel. 2000. Possibilistic Definitions of Security - An Assembly Kit. In Proceedings of the IEEE Workshop on Computer Security Foundations. IEEE Computer Society. Google ScholarDigital Library
- Microsoft. 2018a. Type Compatibility - TypeScript. (2018). Retrieved June 11, 2018 from https://www.typescriptlang.org/ docs/handbook/type-compatibility.htmlGoogle Scholar
- Microsoft. 2018b. TypeScript. (2018). Retrieved June 11, 2018 from https://www.typescriptlang.org/Google Scholar
- Andrew C Myers. 1999. JFlow: Practical mostly-static information flow control. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM. Google ScholarDigital Library
- 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).Google Scholar
- Amos Ndegwa. 2016. What is Page Load Time? (2016). Retrieved June 11, 2018 from https://www.maxcdn.com/one/ visual-glossary/page-load-time/Google Scholar
- Nebulet. 2018. Lachlan Sneff. (2018). Retrieved July 4, 2018 from https://github.com/nebulet/nebuletGoogle Scholar
- NIST. 2002. Secure Hash Standard. FIPS PUB 180-2 (2002).Google Scholar
- Node.js Foundation. 2018. Node.js. (2018). Retrieved June 11, 2018 from https://nodejs.org/docs/latest-v10.x/api/crypto.htmlGoogle Scholar
- Open Whisper Systems. 2016. Signal Protocol library for JavaScript. (2016). Retrieved June 23, 2018 from https://github. com/signalapp/libsignal-protocol-javascriptGoogle Scholar
- Yossef Oren, Vasileios P. Kemerlis, Simha Sethumadhavan, and Angelos D. Keromytis. 2015. The Spy in the Sandbox: Practical Cache Attacks in JavaScript and Their Implications. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. ACM. Google ScholarDigital Library
- Dag Arne Osvik, Adi Shamir, and Eran Tromer. 2006. Cache attacks and countermeasures: the case of AES. In Proceedings of the Cryptographers’ Track at the RSA Conference. Springer. Google ScholarDigital Library
- D. Page. 2006. A Note On Side-Channels Resulting From Dynamic Compilation. In Cryptology ePrint Archive. https: //eprint.iacr.org/2006/349Google Scholar
- Andrei Popescu, Johannes Hölzl, and Tobias Nipkow. 2012. Proving Concurrent Noninterference. In Proceedings of the ACM SIGPLAN International Conference on Certified Programs and Proofs. Springer-Verlag. Google ScholarDigital Library
- Thomas Pornin. 2017. Why Constant-Time Crypto? (2017). Retrieved June 11, 2018 from https://www.bearssl.org/ constanttime.htmlGoogle Scholar
- François Pottier and Vincent Simonet. 2003. Information flow inference for ML. ACM Transactions on Programming Languages and Systems 25, 1 (2003). Google ScholarDigital Library
- Project Everest. 2018. HACL*, a formally verified cryptographic library written in F*. (2018). Retrieved July 12, 2018 from https://github.com/project-everest/hacl-starGoogle Scholar
- John Renner, Sunjay Cauligi, and Deian Stefan. 2018. Constant-Time WebAssembly. In Principles of Secure Compilation.Google Scholar
- Oscar Reparaz, Josep Balasch, and Ingrid Verbauwhede. 2017. Dude, is My Code Constant Time?. In Proceedings of the Conference on Design, Automation and Test in Europe. European Design and Automation Association. Google ScholarDigital Library
- A. Sabelfeld and A. C. Myers. 2006. Language-based Information-flow Security. IEEE Journal on Selected Areas in Communications 21, 1 (2006). Google ScholarDigital Library
- Andrei Sabelfeld and David Sands. 2000. Probabilistic Noninterference for Multi-Threaded Programs. In Proceedings of the IEEE Workshop on Computer Security Foundations. IEEE Computer Society. Google ScholarDigital Library
- Ryan Sleevi. 2013. W3C Web Crypto API Update. (2013). https://datatracker.ietf.org/meeting/86/materials/slides-86-saag-5 IETF 86.Google Scholar
- Dominik Strohmeier and Peter Dolanjski. 2017. Comparing Browser Page Load Time: An Introduction to Methodology. (2017). Retrieved June 11, 2018 from https://hacks.mozilla.org/2017/11/ comparing-browser-page-load-time-an-introduction-to-methodology/Google Scholar
- Torsten Stüber. 2017. TweetNacl-WebAssembly. (2017). https://github.com/TorstenStueber/TweetNacl-WebAssemblyGoogle Scholar
- Dominic Tarr. 2013. crypto-browserify. (2013). Retrieved June 23, 2018 from https://www.npmjs.com/package/ crypto-browserifyGoogle Scholar
- David Terei, Simon Marlow, Simon Peyton Jones, and David Mazières. 2012. Safe Haskell. In ACM SIGPLAN Notices, Vol. 47. ACM. Google ScholarDigital Library
- Tom Van Goethem, Wouter Joosen, and Nick Nikiforakis. 2015. The Clock is Still Ticking: Timing Attacks in the Modern Web. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. ACM. Google ScholarDigital Library
- Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 1996. A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4, 2-3 (1996). Google ScholarDigital Library
- Conrad Watt. 2018. Mechanising and Verifying the WebAssembly Specification. In Proceedings of the ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM. Google ScholarDigital Library
- 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/Google Scholar
- WebAssembly Community Group. 2018a. Module Instances. (2018). Retrieved June 11, 2018 from https://webassembly. github.io/spec/core/exec/runtime.html?highlight=instance#module-instancesGoogle Scholar
- WebAssembly Community Group. 2018b. reference-types. (2018). Retrieved June 11, 2018 from https://github.com/ WebAssembly/reference-typesGoogle Scholar
- WebAssembly Community Group. 2018c. WebAssembly. (2018). Retrieved June 11, 2018 from http://webassembly.orgGoogle Scholar
- WebAssembly Community Group. 2018d. WebAssembly. (2018). Retrieved June 11, 2018 from https://github.com/ WebAssembly/spec/tree/master/interpreterGoogle Scholar
- David J. Wheeler and Roger M. Needham. 1994. TEA, a tiny encryption algorithm. In Lecture Notes in Computer Science. Springer.Google Scholar
- A.K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation 115, 1 (1994). Google ScholarDigital Library
- Bennet Yee, David Sehr, Gregory Dardyk, J Bradley Chen, Robert Muth, Tavis Ormandy, Shiki Okasaka, Neha Narula, and Nicholas Fullagar. 2009. Native Client: A sandbox for portable, untrusted x86 native code. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society. Google ScholarDigital Library
- Alon Zakai. 2015. Compiling to WebAssembly: It’s Happening! (2015). Retrieved July 12, 2018 from https://hacks.mozilla. org/2015/12/compiling-to-webassembly-its-happening/Google Scholar
- Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017. HACL*: A verified modern cryptographic library. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. ACM. Google ScholarDigital Library
Index Terms
- CT-wasm: type-driven secure cryptography for the web ecosystem
Recommendations
Secure public-key encryption scheme without random oracles
Since the first practical and secure public-key encryption scheme without random oracles proposed by Cramer and Shoup in 1998, Cramer-Shoup's scheme and its variants remained the only practical and secure public-key encryption scheme without random ...
Cryptography in the Web: The Case of Cryptographic Design Flaws in ASP.NET
SP '11: Proceedings of the 2011 IEEE Symposium on Security and PrivacyThis paper discusses how cryptography is misused in the security design of a large part of the Web. Our focus is on ASP.NET, the web application framework developed by Microsoft that powers 25% of all Internet web sites. We show that attackers can abuse ...
Nonmalleable Cryptography
The notion of nonmalleable cryptography, an extension of semantically secure cryptography, is defined. Informally, in the context of encryption the additional requirement is that given the ciphertext it is impossible to generate a different ciphertext ...
Comments