Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/13451
Título: | Deductive verification of cryptographic software |
Autor(es): | Almeida, José Bacelar Barbosa, Manuel Pinto, Jorge Sousa Vieira, Bárbara |
Palavras-chave: | Cryptographic algorithms Program verification Program equivalence Self-composition |
Data: | 2010 |
Editora: | Springer |
Revista: | Innovations in systems and software engineering |
Resumo(s): | We apply state-of-the art deductive verification tools to check security-relevant properties of cryptographic software, including safety, absence of error propagation, and correctness with respect to reference implementations. We also develop techniques to help us in our task, focusing on methods oriented towards increased levels of automation, in scenarios where there are clear obvious limits to such automation. These techniques allow us to integrate automatic proof tools with an interactive proof assistant, where the latter is used off-line to prove once-and-for-all fundamental lemmas about properties of programs. The techniques developed have independent interest for practical deductive verification in general. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/13451 |
DOI: | 10.1007/s11334-010-0127-y |
ISSN: | 1614-5046 |
Versão da editora: | The original publication is available at http://www.springerlink.com |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
main.pdf | Documento principal | 166,55 kB | Adobe PDF | Ver/Abrir |