一句话：在 WebAssembly 上引入类型驱动的严格扩展 CT-Wasm，用类型系统保证密码代码的信息流安全与恒定时间执行。
大量客户端与服务端密码学代码用 JavaScript 实现，虽广受安全质疑，却因其在 Web 生态中的无处不在而难以替代。WebAssembly 的引入为提出既有原则性又不牺牲便利性的替代方案提供了机会。本文提出 Constant-Time WebAssembly（CT-Wasm），一个类型驱动、严格的 WebAssembly 扩展，用于可验证安全地实现密码算法。其类型系统同时保证信息流安全与抵抗计时侧信道攻击，且与原 Wasm 一样可在多项式（线性）时间内验证。作者在已有 Wasm 机器化基础上机器化了完整 CT-Wasm 规约，证明了扩展类型系统的可靠性，实现了经验证的类型检查器，并给出若干安全性质证明。工作提供 OCaml 参考解释器、面向 Node.js 与 Chromium 的 V8 原生实现，以及 CT-Wasm 到 Wasm 的重写工具，使开发者可在基础 Wasm 环境中受益于该类型系统。作者移植了 Salsa20、SHA-256、TEA 及完整 TweetNaCl 库进行评估，结果显示 CT-Wasm 快速、表达力强，且生成代码经实验测量为恒定时间。
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.
@article{paperbot680,
title = {CT-wasm: type-driven secure cryptography for the web ecosystem},
author = {Conrad Watt and John Renner and Natalie Popescu and Sunjay Cauligi and Deian Stefan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290390}
}