SCVerify: Verification of Software Implementation Against Power Side-Channel Attacks

Power side-channel attacks, have become a serious threat to embedded computing devices in cyber-physical systems because of the ability of deducing secret data using statistical analysis. A common strategy for designing countermeasures against power-analysis-based side-channel attacks uses random masking techniques to remove the statistical dependency between secret data and side-channel information. Although existing techniques can verify whether a piece of cryptographic software code is perfectly masked, they are limited in accuracy and scalability. In order to eliminate such limitations, a refinement-based method for verifying masking countermeasures is proposed. This method is more accurate than prior type-inference based approaches and more scalable than prior model-counting based approaches using satisfiability (SAT) or satisfiability modulo theories (SMT) solvers. Indeed, this method uses a set of semantic type-inference rules to reason about distribution type. These rules are kept abstract initially to allow fast deduction, and then specified when the abstract version is not able to resolve the verification problem. This method is implemented in a software tool called SCVerify and is evaluated on cryptographic benchmarks including advanced encryption standard (AES) and message authentication code Keccak (MAC-Keccak). The experimental results show that the method significantly outperforms state-of-the-art techniques in terms of accuracy and scalability