Prosecco
Prosecco is a research team at Inria Paris that does formal and practical security research on cryptographic protocols, software security, web security, and hardware protection mechanisms. To this end, we design and implement programming languages, formal verification tools, dynamic monitors, testing frameworks, verified compilers, etc.
Software Tools
- HACL*: High-Assurance Cryptographic Library
- F*: Verification system for effectful programs
- CryptoVerif: Cryptographic protocol verifier in the computational model
- ProVerif: Cryptographic protocol verifier in the symbolic model
- hacspec: Domain-specific language for cryptographic specifications embedded in Rust
- Catala: Domain-specific language for faithfully and efficiently translating law into code
- Squirrel: Interactive prover for security protocols in the computational model.
- miTLS: Verified reference implementation of TLS
- Charon and Aeneas: Verification of Rust programs by means of translation to pure lambda calculus
Recruitment
We are always on the lookout for highly motivated students and young researchers for research internships and PhD, PostDoc, Research Engineer, or Researcher positions. We have external funding for a couple of PhD and PostDoc positions we can fill over several years with significant flexibility and can also support strong candidates for Researcher positions funded and awarded competitively by Inria. See the job offers page for an overview of current projects and how to apply.
How to reach us
We are located at 2 rue Simone Iff, 75012 Paris, France. This address is, however, so new that mapping applications might not know it; if that’s the case please use this old equivalent address: 43 Rue du Charolais, 75012 Paris, France. Here are more details.
Postal address
Inria Prosecco team, Centre de Recherche Inria de Paris, 2 rue Simone Iff, CS 42112, 75589 Paris Cedex 12
