  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.
