Formal verification of cryptographic software implementations
Bárbara Isabel Sousa Vieira · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT) · 2012
Security is notoriously difficult to sell as a feature in software products. In addition to meeting a set of security requirements, cryptographic software has to be cheap, fast, and use little resources. The development of cryptographic software is an area with specific needs in terms of software development processes and tools. In this thesis we explore how formal techniques, namely deductive verification techniques, can be used to increase the guarantees that cryptographic software implementations indeed work as prescribed. This thesis is organized in two parts. The first part is focused on the identification of relevant security policies that may be at play in cryptographic systems, as well as the language-based mechanisms that can be used to enforce such policies in those systems. We propose methodologies based on deductive verification to formalise and verify relevant security policies in cryptographic software. We also show the applicability of those methodologies by presenting some case studies using a deductive verification tool integrated in the Frama-c framework. In the second part we propose a deductive verification tool (CAOVerif) for a domainspecific language for cryptographic implementations (CAO). Our aim is to apply the methodologies proposed in the first part of this thesis work to verify the cryptographic implementations written in CAO. The design of CAOVerif follows the same approach used in other scenarios for general-propose languages and it is build on top of a plug-in from the Frama-c framework. At the very end, we conclude the work of this thesis by reasoning about the soundness of our verification tool.