@article {BacelarAlmeida:2013:FVS:2483313.2483334,
	title = {Formal verification of side-channel countermeasures using self-composition},
	journal = {Science Computer Programming},
	volume = {78},
	number = {7},
	year = {2013},
	pages = {796{\textendash}812},
	publisher = {Elsevier North-Holland, Inc.},
	address = {Amsterdam, The Netherlands, The Netherlands},
	abstract = {<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>
},
	keywords = {Cryptographic algorithms, Program equivalence, Program verification, Self-composition, Side-channel countermeasures},
	issn = {0167-6423},
	doi = {10.1016/j.scico.2011.10.008},
	attachments = {https://haslab.uminho.pt/sites/default/files/jsp/files/11scp.pdf},
	author = {Jos{\'e} Bacelar Almeida and Manuel Bernardo Barbosa and Jorge Sousa Pinto and B{\'a}rbara Vieira}
}