CAOVerif: An open-source deductive verification platform for cryptographic software implementations

• Tipo: Artigo em Revista Científica Internacional
• Data: 2014

Autores

Almeida, JB (Autor) Outra; Barbosa, M (Autor) FCUP; Filliatre, JC (Autor) Outra; Pinto, JS (Autor) Outra; Vieira, B (Autor) Outra

Revista

Título: Science of Computer Programming

Vol. 91

Páginas: 216-233

ISSN: 0167-6423

Editora: Elsevier

Indexação

ISI Web of Knowledge - 1 Citação

Scopus - 1 Citação

Outras Informações

ID Authenticus: P-008-Y45

DOI: 10.1016/j.scico.2012.09.019

Abstract (EN): 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 18