Power side-channel attacks, capable of deducing secret using statistical analysis techniques, have become a serious threat to devices in cyber-physical systems and the Internet of things. Random masking is a widely used countermeasure for removing the statistical dependence between secret data and side-channel leaks. Although there are some techniques for verifying whether software code has been perfectly masked, they are limited in accuracy and scalability.

To bridge this gap, we propose a refinement-based method for formally verifying masking countermeasures. Our method is more accurate than prior syntactic type inference rule based approaches and more scalable than model-counting based approaches using SAT/SMT solvers.

Indeed, our method can be viewed as a gradual refinement of a set of carefully designed semantic type inference rules for reasoning about distribution types. These rules are kept abstract initially to allow fast deduction, and then made more concrete if necessary, i.e., when the abstract version is not able to completely resolve the verification problem.

We have implemented our method in a tool named SCInfer and evaluated it on cryptographic benchmarks including AES and MAC-Keccak. Our results show that SCInfer significantly outperforms state-of-the-art techniques in terms of both accuracy and scalability.