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

Garrett Gu, Hovav Shacham

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…