Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/14219
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: | 2011 |
Editora: | Elsevier |
Revista: | Science of Computer Programming |
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 optimisations 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 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/14219 |
ISSN: | 0167-6423 |
Versão da editora: | The original publication is available at http://www.sciencedirect.com/science/article/pii/S0167642311001857 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
main.pdf | Documento principal | 307,24 kB | Adobe PDF | Ver/Abrir |