%0 Journal Article
%J Science Computer Programming
%D 2013
%T Formal verification of side-channel countermeasures using self-composition
%A José Bacelar Almeida
%A Manuel Bernardo Barbosa
%A Jorge Sousa Pinto
%A Bárbara Vieira
%C Amsterdam, The Netherlands, The Netherlands
%I Elsevier North-Holland, Inc.
%K Cryptographic algorithms
%K Program equivalence
%K Program verification
%K Self-composition
%K Side-channel countermeasures
%N 7
%P 796–812
%R 10.1016/j.scico.2011.10.008
%V 78
%X <p>Formal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive low-level optimizations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. In this paper we extend previous results supporting the practicality of self-composition proofs of non-interference and generalisations thereof. We tackle the formal verification of high-level security policies adopted in the implementation of the recently proposed NaCl cryptographic library. We propose a formal verification framework to address these policies, extending the range of attacks that could previously be han- dled using self-composition. We demonstrate our techniques by addressing functional correctness and compliance with security policies for a practical use case.</p>
%> https://haslab.uminho.pt/sites/default/files/jsp/files/11scp.pdf