Jorge Sousa Pinto

Citation:

Almeida JB, Barbosa MB, Pinto JS, Vieira B.  2013.  Formal verification of side-channel countermeasures using self-composition. Science Computer Programming. 78(7):796–812.

Abstract:

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.

Citation Key: