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.

翻译：我们声称，现有用于生成和验证恒定时间代码的技术和工具是不完备的，因为它们依赖于编译器优化过程不会破坏恒定时间特性或某些操作在硬件上能恒定时间执行等假设。我们提出了首个端到端感知恒定时间的编译流程，该流程从高级语言到微架构保证的每一步都维护恒定时间语义，并由即将推出的ARM PSTATE.DIT特性提供保障。首先，我们提出了一套基于JIT风格运行时Wasmtime的新编译器-验证器套件，该套件经过修改，可将ct-wasm（一种基于WebAssembly的预存在类型安全的恒定时间扩展）编译为ARM机器码，同时在整个优化过程中保持恒定时间属性。生成的机器码随后被送入自动化验证器，该验证器无需人工干预，并利用Ghidra中的静态数据流分析检查输出的恒定时间特性。我们的验证器利用了ct-wasm生成代码独有的特征，以加速验证过程，同时保持可靠性和广泛适用性。我们还考虑了本编译与验证方案对Spectre等推测时序泄露的抵抗能力。最后，为在高级层面展示ct-Wasmtime，我们提出了将预存恒定时间感知DSL——FaCT移植到ct-wasm目标平台的方案。