[PriSC'22] Type-directed Program Transformation for Constant-Time Enforcement

Constant-time is a programming discipline which protects cryptographic code against a wide class of timing attacks. This discipline can be formalised as a non-interference property and enforced by an information-flow type-system which prevents branching and memory accesses over secret data. We propose a relaxed information-flow type system which tracks indirect flows but only rejects programs leaking secrets through direct flows. We exploit typing information to guide a program transformation which compiles any well-typed program into a semantically equivalent constant-time program.