Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/26363
Título: | Formal verification of side-channel countermeasures using self-composition |
Autor(es): | Almeida, José Bacelar Barbosa, Manuel Pinto, Jorge Sousa Vieira, Bárbara |
Palavras-chave: | Cryptographic algorithms Program verification Program equivalence Self-composition Side-channel countermeasures |
Data: | 2013 |
Editora: | Elsevier |
Revista: | Science of Computer Programming |
Citação: | José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira: Formal verification of side-channel countermeasures using self-composition. Sci. Comput. Program. 78(7): 796-812 (2013) |
Resumo(s): | 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 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 generalizations thereof. We tackle the formal verification of high-level security policies adopted in the implementation of the recently proposed NaCl cryptographic library. We formalize these policies and propose a formal verification approach based on self-composition, extending the range of security policies that could previously be handled using this technique. We demonstrate our results by addressing compliance with the NaCl security policies in real-world cryptographic code, highlighting the potential for automation of our techniques. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/26363 |
DOI: | 10.1016/j.scico.2011.10.008 |
ISSN: | 0167-6423 |
Versão da editora: | The original publication is available at http://www.sciencedirect.com/ |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
SCICO_2013.pdf | Documento principal | 467,2 kB | Adobe PDF | Ver/Abrir |