%0 Conference Paper
%B Proceedings of the 4th International Workshop on Foundations and Techniques for Open Source Software Certification - OpenCert
%D 2010
%T A Deductive Verification Platform for Cryptographic Software
%A Manuel Bernardo Barbosa
%A Jorge Sousa Pinto
%A Jean-Christophe Filliâtre
%A Bárbara Vieira
%C Pisa, Italy
%V 33
%X <p>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.</p>
%8 September
%> https://haslab.uminho.pt/sites/default/files/mbb/files/2010_opencert_10_a.pdf