Verifying and Quantifying Side-channel Resistance of Masked Software Implementations

Power side-channel attacks, capable of deducing secret data using statistical analysis, have become a serious threat. Random masking is a widely used countermeasure for removing the statistical dependence between secret data and side-channel information. Although there are techniques for verifying whether a piece of software code is perfectly masked, they are limited in accuracy and scalability. To bridge this gap, we propose a refinement-based method for verifying masking countermeasures. Our method is more accurate than prior type-inference-based approaches and more scalable than prior model-counting-based approaches using SAT or SMT solvers. Indeed, our method can be viewed as a gradual refinement of a set of type-inference rules for reasoning about distribution types. These rules are kept abstract initially to allow fast deduction and then made concrete when the abstract version is not able to resolve the verification problem. We also propose algorithms for quantifying the amount of side-channel information leakage from a software implementation using the notion of quantitative masking strength. We have implemented our method in a software tool and evaluated it on cryptographic benchmarks including AES and MAC-Keccak. The experimental results show that our method significantly outperforms state-of-the-art techniques in terms of accuracy and scalability.