Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 15:43 - 16:05 at Sala II - Time Chair(s): Andrew C. Myers

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.

CT-Wasm: Presentation Slides PDF (ctwasm_slides.pdf)682KiB

Thu 17 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

15:21 - 16:49: TimeResearch Papers at Sala II
Chair(s): Andrew C. MyersCornell University
15:21 - 15:43
Type-Guided Worst-Case Input Generation
Research Papers
Di WangCarnegie Mellon University, Jan HoffmannCarnegie Mellon University
Link to publication DOI Pre-print Media Attached File Attached
15:43 - 16:05
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Research Papers
Conrad WattUniversity of Cambridge, John RennerUniversity of California, San Diego, Natalie PopescuUniversity of California San Diego, Sunjay CauligiUCSD, Deian StefanUniversity of California San Diego
Link to publication DOI Media Attached File Attached
16:05 - 16:27
Modular Quantitative Monitoring
Research Papers
Rajeev AlurUniversity of Pennsylvania, Konstantinos MamourasUniversity of Pennsylvania, Caleb StanfordUniversity of Pennsylvania
Link to publication DOI Media Attached File Attached
16:27 - 16:49
CSS Minification via Constraint SolvingTOPLAS
Research Papers
Matthew HagueRoyal Holloway, University of London, Anthony Widjaja LinOxford University, Chih-Duo HongUniversity of Oxford
Media Attached File Attached