CRYSP: Collaborative Cryptographic Security Proofs for Programs

ERC Starting Grant 2010: 259639-CRYSP
Principal Investigator: K. Bhargavan

Objectives

The goal of the CRYSP project is to enable the security verification of large-scale collaborative software, such as cryptographic protocol libraries, and web applications built using these libraries. In previous work, we showed how to extract abstract symbolic models directly from implementation code and then verify them using specialized theorem provers [Bhargavan et al., 2008c]. We used this technique to verify implementations of widely deployed and important cryptographic protocols such as Windows Cardspace [Bhargavan et al., 2008b] and Transport Layer Security (TLS) [Bhargavan et al., 2008a]. However, a key limitation of such verification techniques is that one must verify the whole program at once. For large programs such as our TLS implementation, this leads to long and unpredictable verification times and quickly becomes infeasible.

In more recent work [Bengtson et al., 2008], we explore a new program specification technique, called refinement types, and adapt it for security verification. We find that typechecking is more compositional and modular than whole-program verification, and hence, it scales far better. We have designed and implemented a refinement type system for the functional programming language F# and used it to verify large multi-party security protocol implementations [Bhargavan et al., 2009, Bhargavan et al., 2010]. Even with the advantages of refinement typechecking, writing, maintaining, and verifying security specifications for constantly-evolving collaboratively-written large software projects remains a difficult task, suitable only for security verification experts.

The main aim of CRYSP is to design and implement new refinement typecheckers that can be directly used by software developers to build formal security proofs for the code that they write, whether in F#, C, or Java. In particular, CRSYP identifies five key research goals:

  1. Design a new collaborative security specification framework that helps programmers to incrementally develop security specifications for their code;
  2. Design and implement new incremental and modular security verification techniques that scale up to large programs;
  3. Design and implement tools to extract security-critical components from programs;
  4. Build the first verified open source cryptographic library with implementations for standard protocols such as TLS, SSH, IPSec, and Kerberos;
  5. Build the first web applications with formal proofs of security.

CRYSP Team

We are in the process of building a team to tackle these goals. The team is headed by Karthikeyan Bhargavan, and is closely linked to both the MOSCOVA project and the Microsoft Research-INRIA Joint Centre. We have several ongoing and potential collaborations on various aspects of CRYSP with C. Fournet (Microsoft Research Cambridge), C. Gunter (University of Illinois Urbana-Champaign), S. Maffeis (Imperial College), P. Naldurg (Microsoft Research, Bangalore), and G. Steel (INRIA Saclay).

Openings and Deadlines

We are offering the following positions within the CRYSP team in 2011:

We will keep the offers open until the positions are filled. The starting date for each position is flexible.

To apply, send a CV, research statement, and the names and addresses of three referees to [karthikeyan DOT bhargavan AT inria DOT fr]

References

Bengtson et al. [2008]
J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. In 21st IEEE Computer Security Foundations Symposium (CSF’08), pages 17–32, 2008. PDF.
Bhargavan et al. [2008a]
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, 2008a. PDF.
Bhargavan et al. [2008b]
K. Bhargavan, C. Fournet, A. D. Gordon, and N. Swamy. Verified implementations of the Information Card federated identity-management protocol. In ACM Symposium on Information, Computer and Communications Security (ASIACCS’08), pages 123–135. ACM, 2008b. PDF.
Bhargavan et al. [2008c]
K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse. Verified interoperable implementations of security protocols. ACM TOPLAS, 31: 5:1–5:61, December 2008c. PDF.
Bhargavan et al. [2009]
K. Bhargavan, R. Corin, P.-M. Deniélou, C. Fournet, and J. J. Leifer. Cryptographic protocol synthesis and verification for multiparty sessions. In 22nd IEEE Computer Security Foundations Symposium (CSF’09), pages 124–140. IEEE Computer Society, July 2009. 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.
This document was translated from LATEX by HEVEA.