Quantile: Quantifying Information Leakage

The masking countermeasure is very effective against side-channel attacks
such as differential power analysis. However, the design of masked circuits is a
challenging problem since one has to ensure security while minimizing performance
overheads. The security of masking is often studied in the t-probing model, and
multiple formal verification tools can verify this notion. However, these tools generally
cannot verify large masked computations due to computational complexity.
We introduce a new verification tool named Quantile, which performs randomized
simulations of the masked circuit in order to bound the mutual information between
the leakage and the secret variables. Our approach ensures good scalability with the
circuit size and results in proven statistical security bounds. Further, our bounds
are quantitative and, therefore, more nuanced than t-probing security claims: by
bounding the amount of information contained in the lower-order leakage, Quantile
can evaluate the security provided by masking even when they are not 1-probing
secure, i.e., when they are classically considered as insecure. As an example, we apply
Quantile to masked circuits of Prince and AES, where randomness is aggressively
reused.