Please use this identifier to cite or link to this item:

TitleCAOVerif: an open-source deductive verification platform for cryptographic software implementations
Author(s)Almeida, José Bacelar
Barbosa, Manuel
Filliâtre, Jean-Christophe
Pinto, Jorge Sousa
Vieira, Bárbara Isabel Sousa
KeywordsFormal verification
Program verification
Cryptographic software
Deductive verification
Issue date2014
JournalScience of Computer Programming
CitationAlmeida, 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.
Abstract(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.
Publisher versionThe original publication is available at
AccessOpen access
Appears in Collections:HASLab - Artigos em revistas internacionais

Files in This Item:
File Description SizeFormat 
opencertjournal_ack.pdfDocumento Principal285,04 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID