Avoiding Instruction-Centric Microarchitectural Timing Channels Via Binary-Code Transformations

Future processors may skip a store whose value is already in memory, or shortcut a multiply by 1, and each such shortcut leaks the secret operand that triggered it, in places (register spills, address arithmetic) that source-level constant-time rules cannot reach — cio, a compiler-plus-binary-analysis tool, finds every instruction in a cryptographic library whose secret operand could trigger the shortcut, rewrites it into a proven-equivalent sequence that cannot trigger it, and then re-checks the final binary, hardening libsodium at a cost of 1.1 to 28 times slower code.

Why this problem is worth solving

Processor designers, pushed by the end of Dennard scaling, keep proposing

The consequences are nasty. Zeroing a key with silent stores issues a different number of writes depending on how many key bytes are already zero. Prior work showed, in a gem5 simulation, that a single attacker-prepared silent store leaks a key from a bitsliced AES that is constant-time by every classic rule. And because the compiler inserts stores (register spills, stack arguments) and arithmetic (address computation with lea) that never appear in source, no amount of careful C can avoid them. Every newly disclosed optimization would otherwise start the cycle again: attack paper, rules update, rewrite every library.

What people did before

Vendors have begun offering modes. ARM’s Data Independent Timing (DIT, since ARMv8.4-A in 2017) lets any privilege level set a bit that promises constant timing for most arithmetic and stores, but the only processors known to honor it are Apple’s M-series. Intel’s Data Operand Independent Timing (DOIT, 2022) can be set only by the kernel, is not guaranteed under speculation, and no operating system exposed it to user code as of December 2023. AMD has none. The authors also verified experimentally that Apple’s prefetcher still activates with DIT set, showing that vendors and software may disagree about what such a mode should cover. Vendors also ship microcode switches for disclosed attacks (Intel’s SSBD for speculative store bypass), but those are global, per-thread state bits that are awkward to manage.

On the software side, verification tools check the classic constant-time properties, domain-specific languages such as FaCT and CT-Wasm compile to guaranteed constant-time code, and compiler transforms such as Constantine linearize control and data flow. Closest is SynthCT, which synthesizes safe replacements for instructions outside a declared safe subset; it is complementary but coarser, because it replaces every instance of a flagged instruction rather than only those that could see secret trigger values.

The idea

The threat model is deliberately strong: the adversary sees every time the optimization fires, and the program is already constant-time in the classic sense. cio’s promise is that the hardened binary leaks nothing more on a processor with the optimization than on one without it.

Everything happens at the

Prune, do not enumerate. Computation simplification can apply to almost every arithmetic and bitwise instruction in a binary; transforming them all would be ruinous. So the checkers start by assuming everything leaks and use increasingly precise analyses to remove instructions that provably cannot see a trigger value. Taint analysis from the annotated secret arguments drops anything a secret never reaches. Interval analysis with machine-integer semantics drops instructions whose operand range excludes 0, 1 or all-ones; in ed25519, for example, values are often bit-masked before use, which incidentally makes them safe. A memory domain from Miné handles register-indirect operands. Any stopping point is safe, because whatever is not pruned gets transformed.

Transforms that make the trigger value unreachable. For computation simplification, three approaches ordered by cost. Arithmetic transforms widen a 32-bit or smaller operand into a 64-bit register and set a high bit, shifting its range from 0 to 2^32 minus 1 up to 2^32 to 2^33 minus 1 so it can never be 0 or 1; the operation runs on the wide register and the low bits of the result are correct unchanged. Split-and-recombine handles 64-bit operands and bitwise ops by splitting each operand into a 48-bit and a 16-bit piece (not 32/32, because writing the low 32 bits of an x86 register clears the upper 32, but writing the low 16 does not), setting spare bits in each piece to exclude unsafe values, operating, and recombining; for shifts the recombination is an addition that itself must be made safe. Conditional move transforms use the guaranteed constant-time cmov to build two straight-line branches, substituting a safe static operand in the trigger case and fixing up the result afterward; they cost many instructions and are used only for shift amounts that are dynamic.

For silent stores the trick is a

Verify the transforms once, then verify the binary cheaply. Each transform is proven offline with Serval to be equivalent in observable behavior (x86 transforms need not preserve unused status flags) and free of trigger conditions from any starting state. Because the checkers verify transforms in isolation under the most general state, and every unpruned instruction in the final binary belongs to a transform, double-checking the whole library stays tractable.

Why it works

• Operand values, not instruction identity, decide safety. By reasoning about value ranges in the binary, cio transforms 4,858 of 13,198 candidate instructions for computation simplification in libsodium instead of all of them, and 1,879 of 2,695 stores for silent stores. Taint alone removed 4,940 CS candidates.
• Range-shifting is cheap and provable. Setting a high bit is a one-line invariant an interval analysis can check, which is what lets the same checker both find leaks and verify the fix.
• Transforms are self-contained. Every instruction a transform adds is itself chosen not to trigger the optimizations, so the safety of the whole binary reduces to the safety of each transform in isolation, which is checked once.
• Late placement. Running just before assembly printing means no later compiler optimization can undo the protection.

What it costs

• Run time. On libsodium’s reference implementations, all CS and SS transforms together slowed argon2id by 27.84 times, ed25519 by 20.32 times, aesni256gcm by 8.22 times and chacha20-poly1305 by 3.37 times. The single worst contributor is the transform for 64-bit multiply (116 instructions), which alone costs 15.71 times on argon2id and 8.79 times on ed25519. Silent-store mitigation alone is far cheaper: around 1.05 to 1.2 times on most primitives. Just reserving three scratch registers with no transforms costs under 6 percent.
• Binary size. libsodium’s text grew from 363 kB to 588 kB with SS, 1,118 kB with CS and 1,327 kB with both.
• Build time. A baseline libsodium build takes about 390 seconds; checking and mitigation each add a similar amount, but CS double-checking takes 11,836 seconds, about 3.3 hours, because Z3 times out on many large nonlinear bit-vector queries. Paid once per release build.
• Coverage limits. Only x86-64; only libsodium’s reference C code (the faster assembly implementations cannot be seen by compiler passes); transient execution is not modeled, so secrets reaching instructions only speculatively may be missed; the silent-store transform assumes no store-buffer merging before the silence check. Some instructions are deliberately not transformed (rotates, double shifts, add-with-carry, most vector ops besides add, multiply and store).
• Implementation. 16,503 lines of C++ for the LLVM passes, 10,293 lines of OCaml for checkers, 5,343 lines of Racket for the offline verifier, 474 lines of Bash for cio itself.

Evaluation

The evaluation hardens libsodium built with --disable-asm on an Intel Xeon Gold 6312U. Because no Intel chip implements the target optimizations, the baseline does not benefit from them, so the reported ratios may understate overhead on a real optimizing processor. Each primitive is run 1,000 times (100 for argon2id) with warmup and outlier removal.