Prosecco – Programming securely with cryptography (original) (raw)

Presentation

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 48 rue Barrault, 75013 Paris, France. Here are more details.

Postal address

Inria Prosecco team, Centre Inria de Paris, 48 rue Barrault, CS 61534, 75647 Paris Cedex