Sleuth: automated verification of software power analysis countermeasures

Security analysis is a crucial concern in the design of hardware and software systems, yet there is a distinct lack of automated methodologies. In this paper, we remedy this situation for the verification of software countermeasure implementations. In this context, verifying the security of a protected implementation against side-channel attacks corresponds to assessing whether any particular leakage in any particular computational phase is statistically dependent on the secret data and statistically independent of any random information used to protect the implementation. We present a novel methodology to reduce this verification problem into a set of Boolean satisfiability problems, which can be efficiently solved by leveraging recent advances in SAT solving. To show the effectiveness of our methodology, we have implemented an automatic verification tool, named Sleuth, as an advanced analysis pass in the back-end of the LLVM compiler. Our results show that one can automatically detect several examples of classic pitfalls in the implementation of countermeasures with reasonable runtimes.