Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/31023
Título: | CAOVerif: an open-source deductive verification platform for cryptographic software implementations |
Autor(es): | Almeida, José Bacelar Barbosa, Manuel Filliâtre, Jean-Christophe Pinto, Jorge Sousa Vieira, Bárbara Isabel Sousa |
Palavras-chave: | Formal verification Program verification Cryptographic software Deductive verification |
Data: | 2014 |
Editora: | Elsevier 1 |
Revista: | Science of Computer Programming |
Citação: | Almeida, J. B., Barbosa, M., Filliâtre, J. C., Pinto, J. S., & Vieira, B. (2014). CAOVerif: An open-source deductive verification platform for cryptographic software implementations. Science of Computer Programming, 91(PART B), 216-233. |
Resumo(s): | CAO is a domain-specific imperative language for cryptography, offering a rich mathematical type system and crypto-oriented language constructions. We describe the design and implementation of a deductive verification platform for CAO and demonstrate that the development time of such a complex verification tool could be greatly reduced by building on the Jessie plug-in included in the Frama-C framework. We discuss the interesting challenges raised by the domain-specific characteristics of CAO, and describe how we tackle these problems in our design. We base our presentation on real-world examples of CAO code, extracted from the open-source code of the NaCl cryptographic library, and illustrate how various cryptography-relevant security properties can be verified. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/31023 |
DOI: | 10.1016/j.scico.2012.09.019 |
ISSN: | 0167-6423 |
Versão da editora: | The original publication is available at 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 | |
---|---|---|---|---|
opencertjournal_ack.pdf | Documento Principal | 285,04 kB | Adobe PDF | Ver/Abrir |