A Deductive Verification Platform for Cryptographic Software
In this paper, the authors describe a deductive verification platform for the CAO language. CAO is a domain-specific language for cryptography. They 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. They describe how they 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.