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

• Type: Article in International Scientific Journal
• Date: 2014

Authors

Almeida, JB (Author) Other; Barbosa, M (Author) FCUP; Filliatre, JC (Author) Other; Pinto, JS (Author) Other; Vieira, B (Author) Other

Journal

Title: Science of Computer Programming

Vol. 91

Pages: 216-233

ISSN: 0167-6423

Publisher: Elsevier

Indexing

ISI Web of Knowledge - 1 Citation

Scopus - 1 Citation

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 18