The Open UniversitySkip to content
 

Proving Cryptographic C Programs Secure with General-Purpose Verification Tools

Dupressoir, François (2013). Proving Cryptographic C Programs Secure with General-Purpose Verification Tools. PhD thesis Open University.

Full text available as:
[img]
Preview
PDF (Version of Record) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (1154Kb) | Preview
URL: http://fdupress.net/files/phd-material/Francois.Du...
Google Scholar: Look up in Google Scholar

Abstract

Security protocols, such as TLS or Kerberos, and security devices such as the Trusted Platform Module (TPM), Hardware Security Modules (HSMs) or PKCS#11 tokens, are central to many computer interactions.
Yet, such security critical components are still often found vulnerable to attack after their deployment, either because the specification is insecure, or because of implementation errors.

Techniques exist to construct machine-checked proofs of security properties for abstract specifications.
However, this may leave the final executable code, often written in lower level languages such as C, vulnerable both to logical errors, and low-level flaws.

Recent work on verifying security properties of C code is often based on soundly extracting, from C programs, protocol models on which security properties can be proved.
However, in such methods, any change in the C code, however trivial, may require one to perform a new and complex security proof.

Our goal is therefore to develop or identify a framework in which security properties of cryptographic systems can be formally proved, and that can also be used to soundly verify, using existing general-purpose tools, that a C program shares the same security properties.

We argue that the current state of general-purpose verification tools for the C language, as well as for functional languages, is sufficient to achieve this goal, and illustrate our argument by developing two verification frameworks around the VCC verifier.

In the symbolic model, we illustrate our method by proving authentication and weak secrecy for implementations of several network security protocols.
In the computational model, we illustrate our method by proving authentication and strong secrecy properties for an exemplary key management API, inspired by the TPM.

Item Type: Thesis (PhD)
Copyright Holders: 2012 François Dupressoir
Project Funding Details:
Funded Project NameProject IDFunding Body
Not SetNot SetMicrosoft Research
Keywords: computer security; data protection; C (computer program language)
Academic Unit/Department: Faculty of Science, Technology, Engineering and Mathematics (STEM) > Computing and Communications
Interdisciplinary Research Centre: Centre for Research in Computing (CRC)
Related URLs:
Item ID: 37627
Depositing User: Francois Dupressoir
Date Deposited: 13 Jun 2013 08:58
Last Modified: 05 Oct 2016 05:13
URI: http://oro.open.ac.uk/id/eprint/37627
Share this page:

Download history for this item

These details should be considered as only a guide to the number of downloads performed manually. Algorithmic methods have been applied in an attempt to remove automated downloads from the displayed statistics but no guarantee can be made as to the accuracy of the figures.

▼ Automated document suggestions from open access sources

Actions (login may be required)

Policies | Disclaimer

© The Open University   + 44 (0)870 333 4340   general-enquiries@open.ac.uk