How optimizing compilers can inadvertently introduce timing side-channels into constant-time source code, and how to verify binary execution using formal tools.
Even if source code is written without conditional branches (e.g., using bitwise operations), modern optimizing compilers like LLVM can recognize equivalent logic patterns and substitute them with conditional jump instructions (such as CMOV or conditional branches) to optimize execution speed, inadvertently re-introducing timing vulnerabilities.
We examine formal toolchains such as Jasmin, which combine high-level algorithmic expressiveness with strict assembly-level control. Jasmin allows developers to prove constant-time behavior at the binary level while maintaining mathematical verification links to high-level Coq proofs.
MLKEMSafe integrates automated binary analysis in CI/CD using Valgrind-based ct-grind and dudect. These tools trace memory accesses and program counter movements, flagging any instruction where execution depends on un-poisoned secret memory buffers.