Constant-Time Wasmtime, for Real This Time: End-to-End Verified Zero-Overhead Constant-Time Programming for the Web and Beyond

TL;DR

This paper introduces a comprehensive end-to-end compilation and verification process for constant-time WebAssembly code, ensuring security against timing leaks and hardware optimizations, using a modified Wasmtime runtime and static analysis tools.

Contribution

It presents the first complete constant-time-aware compilation pipeline from high-level language to microarchitectural guarantees, including a new compiler-verifier suite and a port of the FaCT DSL.

Findings

Verified constant-time guarantees for generated code

Enhanced verification speed using ct-wasm-specific properties

Addressed resistance to speculative execution attacks like Spectre

Abstract

We claim that existing techniques and tools for generating and verifying constant-time code are incomplete, since they rely on assumptions that compiler optimization passes do not break constant-timeness or that certain operations execute in constant time on the hardware. We present the first end-to-end constant-time-aware compilation process that preserves constant-time semantics at every step from a high-level language down to microarchitectural guarantees, provided by the forthcoming ARM PSTATE.DIT feature. First, we present a new compiler-verifier suite based on the JIT-style runtime Wasmtime, modified to compile ct-wasm, a preexisting type-safe constant-time extension of WebAssembly, into ARM machine code while maintaining the constant-time property throughout all optimization passes. The resulting machine code is then fed into an automated verifier that requires no human intervention and uses static dataflow analysis in Ghidra to check the constant-timeness of the output. Our verifier leverages characteristics unique to ct-wasm-generated code in order to speed up verification while preserving both soundness and wide applicability. We also consider the resistance of our compilation and verification against speculative timing leakages such as Spectre. Finally, in order to expose ct-Wasmtime at a high level, we present a port of FaCT, a preexisting constant-time-aware DSL, to target ct-wasm.