While microarchitectural constant-time is a golden standard for cryptographic implementations and probability plays an essential role in cryptography, program analysis techniques for probabilistic constant-time are still under developed.

Our work aims to provide a call-by-contract-style modular verification technique for probabilistic constant-time, including code with public outputs, i.e., benign leakages. The technique is inspired by the correspondence between probabilistic constant-time and non-adaptive multiparty computation. Inspired by Theorem 5 in Canetti (2000), a modular logical verification approach emerges.