Hardware-based Privilege Separation for Cryptographic Protocol Implementations

K. Bhargavan and G. Steel

The security of web applications relies on cryptographic protocols such as TLS, SSH, Kerberos, and IPSec. Still, leading implementations of these protocols have been found to have serious bugs years after their release. Our goal is to develop and verify reference implementations of cryptographic protocols.

In previous work, cryptographic provers such as ProVerif and CryptoVerif have been used to verify reference implementations of TLS in ML [Bhargavan et al., 2008]. More recently refinement typechecking (e.g. F7) has been used to verify protocol implementations in both the symbolic model [Bhargavan et al., 2010] and the computational model [Fournet et al., 2011].

Can the guarantees provided by these methods be extended to implementations that use a mixture of hardware-based security APIs Focardi et al. [2011] and software cryptography? Can we obtain even stronger security guarantees by carefully separating the code across the hardware/software boundary? This internship aims to address these questions.

Internship.

In this internship, we start from an existing implementation of TLS that has been written in F# and verified using the refinement typechecker F7. We propose to refactor this implementation to use a PKCS#11 hardware security token for some operations. Subsequently, we seek to verify the new implementation for stronger security guarantees, again using using the refinement typechecker F7.

During the course of the internship, the student will learn to do the following:

Some prior knowledge of cryptography, verification tools, functional programming, and type systems will be an advantage, but is not mandatory. We expect the research carried out during the internship will form the major part of a Masters-level thesis and lead to a conference publication. All interns are funded under the ERC grant CRYSP and successful internships are expected to lead to funded Ph.D. studentships.

Application Details.

The internship will be located at INRIA in Paris, at place d’Italie. To apply, send an email describing your research interests, and including your CV and the names and email addresses of one or two referees (professors or prior employers), to karthikeyan DOT bhargavan AT inria DOT fr. The deadline for applications is January 5, 2012. Positions will be kept open until filled.

The intern will have the opportunity to work closely with a team of researchers from INRIA, and potentially from MSR-INRIA, including B. Blanchet, A. Pironti, and C. Fournet.

References

Bhargavan et al. [2008]
K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu. Cryptographically verified implementations for TLS. In 15th ACM conference on Computer and Communications Security (CCS’08), pages 459–468. ACM, 2008. PDF.
Bhargavan et al. [2010]
K. Bhargavan, C. Fournet, and A. D. Gordon. Modular verification of security protocol code by typing. In ACM Symposium on Principles of Programming Languages (POPL’10), pages 445–456, 2010. PDF.
Focardi et al. [2011]
R. Focardi, F. L. Luccio, and G. Steel. An introduction to security api analysis. In A. Aldini and R. Gorrieri, editors, FOSAD, volume 6858 of Lecture Notes in Computer Science, pages 35–65. Springer, 2011. ISBN 978-3-642-23081-3.
Fournet et al. [2011]
C. Fournet, M. Kohlweiss, and P.-Y. Strub. Modular code-based cryptographic verification. In Proceedings of the 18th ACM conference on Computer and communications security, CCS ’11, pages 341–350, New York, NY, USA, 2011. ACM. ISBN 978-1-4503-0948-6. .

This document was translated from LATEX by HEVEA.