文章基本信息

标题：A Deductive Verification Platform for Cryptographic Software
本地全文：下载
作者：Manuel Barbosa ; J. Pinto ; J.-C. Filliatre 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2010
卷号：33
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：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.