2013 | OriginalPaper | Buchkapitel
Sleuth: Automated Verification of Software Power Analysis Countermeasures
verfasst von : Ali Galip Bayrak, Francesco Regazzoni, David Novo, Paolo Ienne
Erschienen in: Cryptographic Hardware and Embedded Systems - CHES 2013
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.