CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
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 JanDisplayed time zone: Belfast change
15:21 - 16:49
|Type-Guided Worst-Case Input Generation|
Research PapersLink to publication DOI Pre-print Media Attached File Attached
|CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem|
Conrad Watt University of Cambridge, John Renner University of California, San Diego, Natalie Popescu University of California San Diego, Sunjay Cauligi UCSD, Deian Stefan University of California San DiegoLink to publication DOI Media Attached File Attached
|Modular Quantitative Monitoring|
Rajeev Alur University of Pennsylvania, Konstantinos Mamouras University of Pennsylvania, Caleb Stanford University of PennsylvaniaLink to publication DOI Media Attached File Attached
|CSS Minification via Constraint SolvingTOPLAS|
Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Chih-Duo Hong University of OxfordMedia Attached File Attached