eprint.iacr.orgpaper

Secure Compilation of Probabilistic Side-Channel Countermeasures

Presents a language- and leakage-model-agnostic framework for provably secure compilation of probabilistic side-channel countermeasures. It uses a deterministic leakage-preservation relation that implies preservation of d-NI, d-SNI and cryptographic constant-time without probabilistic proof obligations. The authors prove in Rocq that a model of the Jasmin compiler's core pipeline and several optimizing passes preserve security in the value-probing model with glitches. They also add source-level annotations to harden against transition leakage and release libmasking, an arbitrary-order masked gadget library in Jasmin that compiles to ARM and RISC-V, with C bindings and hardware benchmarks.