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

  • Almeida J
  • Barbosa M
  • Filliâtre J
 et al. 
  • 18

    Readers

    Mendeley users who have this article in their library.
  • 0

    Citations

    Citations of this article.

Abstract

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. © 2013 Elsevier B.V. All rights reserved.

Author-supplied keywords

  • Cryptographic software
  • Deductive verification
  • Formal verification
  • Program verification

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

Authors

  • José Bacelar Almeida

  • Manuel Barbosa

  • Jean Christophe Filliâtre

  • Jorge Sousa Pinto

  • Bárbara Vieira

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free