Prosecco
Prosecco is a research team (équipe) at INRIA Paris-Rocquencourt that focuses on building and verifying programs that use cryptography. Our target applications include cryptographic protocol implementations (e.g., TLS), hardware-based security APIs (e.g., Smartcards), smartphone- and browser-based web applications (e.g., Facebook), and cloud-based web services (e.g. Dropbox). Our analysis techniques include dependent type systems, symbolic and computational cryptographic protocol verifiers, general-purpose theorem provers, formal testing frameworks, and run-time analysis tools.
Scientific goals
Ultimately, our goal is to help developers to program securely with cryptography and, to achieve this objective, we are actively researching the following key areas:
- Symbolic verification of cryptographic applications. We are developing verification tools for models and implementations of cryptographic protocols and security APIs using symbolic verification techniques. Our tools include: the specialized cryptographic prover ProVerif, the reverse engineering and formal test tool Tookan, and the security type systems F7 and F* for the programming language F#.
- Computational verification of crytpographic applications. In addition to the development of symbolic tools, we are also developing tools using computational verification techniques. Our tools include: the computational prover CryptoVerif and the computationally sound type system Computational F7 for applications written in F#.
- Provably secure web applications. We are developing analysis tools and verified libraries to help programmers build provably secure web applications. The tools include: static and dynamic verification tool for client-side JavaScript web applications, annotated JML libraries for verifying the security of Android smartphone applications, and the type systems F7 and F* for verifying clients and servers written in F#.
Further details about our scientific goals can be found in our project proposal.
Funding
Our group receives funding from the following projects:
- ANR project VERSO ProSe
- DGA project Analyse de sécurité des interfaces de programmation
- ERC project CRYSP (259639)
- FUI project PISCO
How to find us
We are located at 23 Avenue d'Italie, 75013 Paris, France (Google map) and our office is accessible as follows:
News
25 March 2013
We have a post-doctoral researcher position focusing on Formal Analysis for Security APIs available.
5 March 2013
We have one paper on miTLS accepted at Oakland'13.
15 January 2013
We are seeking interns
21 December 2012
Chetan Bansal and Karthikeyan Bhargavan report three bugs in Facebook's OAuth implementation.
17 December 2012
We have three papers accepted at POST'13.
26 October 2012
Antoine Delignat-Lavaud exploits Firefox security to allow the cross-origin reading of Location objects.
26 June 2012
A paper by Prosecco members and collaborators "Efficient Padding Oracle Attacks on Cryptographic Hardware", to appear at CRYPTO'12, has received some press and blog coverage. Please see the FAQ for more details on the work.
Open Positions
The following positions are currently open:
- 2x Post-doctoral researcher (1-2 year)
- 2x Ph.D. studentships (3 year)
- 3x Masters internships (6 months)
- 3x Internships for Ph.D. students, masters students, and undergraduates (2-3months)
Applicants should have a strong interest on topics in hardware and software security, cryptography, formal verification, and program analysis. One of the post-doctoral positions focuses on Formal Analysis for Security APIs and one of the intern positions focuses on Hardware-based Privilege Separation for Cryptographic Protocol Implementations; we are also seeking post-doctoral researchers and interns who propose their own projects in alignment with our research interests. Positions will be kept open until filled. To apply email any one of the group members with your CV and the name of two references.
Software and Tools
