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

TitleA deductive verification platform for cryptographic software
Author(s)Barbosa, Manuel
Pinto, Jorge Sousa
Filliâtre, Jean-Christophe
Vieira, Bárbara Isabel Sousa
KeywordsFormal program verification
Issue date2010
PublisherEuropean Association of Software Science and Technology (EASST)
JournalElectronic Communications of the EASST
Abstract(s)In this paper we describe a deductive verification platform for the CAO language. CAO is a domain-specific language for cryptography. We show that this language presents interesting challenges for formal verification, not only in the rich mathematical type system that it introduces, but also in the cryptography-oriented language constructions that it offers. We describe how we tackle these problems, and also demonstrate that, by relying on the Jessie plug-in included in the Frama-C framework, the development time of such a complex verification tool could be greatly reduced. 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 version
AccessOpen access
Appears in Collections:HASLab - Artigos em revistas internacionais
DI/CCTC - Artigos (papers)

Files in This Item:
File Description SizeFormat 
A deductive verification platform for cryptographic software.pdfDocumento principal213,22 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