2023Activity reportProject-TeamPROSECCO

New programming languages for verified software

Building realistic verified applications requires new programming languages that enable the systematic development of efficient software hand-in-hand with their proofs of correctness. We design and implement the programming language F*, in collaboration with Microsoft Research. F* (pronounced F star) is a general-purpose functional programming language with a state-of-the-art type-and-effect system aimed at program verification. Its type system includes polymorphism, dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and interactive proofs. Programs written in F* can be translated to efficient OCaml, F#, or C for execution. The main ongoing use cases of F* in our group are HACL*, a verified cryptographic library, and DY*, a framework for verifying protocol implementations. Nevertheless, we also consider non-cryptographic security software, for which we also use F* and its extensions, for instance security-enhanced memory allocators, who are often the last line of defense against memory vulnerabilities in critical C and C++ software  42.

We also design two frameworks for the analysis of Rust programs (hacspec and Aeneas), by translation to various theorem provers including F*.

Recently, we extended our work on programming languages to a domain-specific language for implementing law, for instance tax computation, which is also critical as it impacts every citizen. We indeed noticed that much of the infrastructure and methodologies we developed for cryptographic security software can be transferred to other domains in need of high-assurance software. The combination of software engineering and formal methods that we employ at the Prosecco team may thus have a more general field of application beyond cryptographic software.

Symbolic verification of cryptographic applications

We aim to develop our own security verification tools for models and implementations of cryptographic protocols and security APIs using symbolic cryptography. Our starting point is the tools we have previously developed: the specialized cryptographic prover ProVerif and the F* verification system via the DY* framework. These tools are already used to verify industrial-strength cryptographic protocol implementations and commercial cryptographic hardware. We plan to extend and combine these approaches to capture more sophisticated attacks on applications consisting of protocols, software, and hardware, as well as to prove symbolic security properties for such composite systems.

Computational verification of cryptographic applications

We aim to develop our own cryptographic application verification tools that use the computational model of cryptography. The tools include the computational provers CryptoVerif and Squirrel, and the F* verification system. Working together, we plan to extend these tools to analyze, for the first time, cryptographic protocols, security APIs, and their implementations under fully precise cryptographic assumptions. We also plan to pursue links between tools, in order to use each tool where it is the strongest.

Building provably secure web applications

We aim to develop analysis tools and verified libraries to help programmers build provably secure web applications. The tools will include static and dynamic verification tools for client- and server-side JavaScript web applications, their verified deployment within HTML5 websites and browser extensions, as well as type-preserving compilers from high-level applications written in F* to JavaScript. In addition, we plan to model new security APIs in browsers and smartphones and develop the first formal semantics for various HTML5 web standards. We plan to combine these tools and models to analyze the security of multi-party web applications, consisting of clients on browsers and smartphones, and servers in the cloud.

Verifying cryptographic protocols with ProVerif

Given a model of a cryptographic protocol, the problem is to verify that an active attacker, possibly with access to some cryptographic keys but unable to guess other secrets, cannot thwart security goals such as authentication and secrecy  68; it has motivated a serious research effort on the formal analysis of cryptographic protocols, starting with  59 and eventually leading to effective verification tools, such as our tool ProVerif.

To use ProVerif, one encodes a protocol model in a formal language, called the applied pi-calculus, and ProVerif abstracts it to a set of generalized Horn clauses. This abstraction is a small approximation: it just ignores the number of repetitions of each action, so ProVerif is still very precise, more precise than, say, tree automata-based techniques. The price to pay for this precision is that ProVerif does not always terminate; however, it terminates in most cases in practice, and it always terminates on the interesting class of tagged protocols52. ProVerif can handle a wide variety of cryptographic primitives, defined by rewrite rules or by some equations, and prove a wide variety of security properties: secrecy 50, 37, correspondences (including authentication) 51, and observational equivalences 49. Observational equivalence means that an adversary cannot distinguish two processes (protocols); equivalences can be used to formalize a wide range of properties, but they are particularly difficult to prove. Even if the class of equivalences that ProVerif can prove is limited to equivalences between processes that differ only by the terms they contain, these equivalences are useful in practice and ProVerif has long been the only tool that proves equivalences for an unbounded number of sessions. (Maude-NPA in 2014 and Tamarin in 2015 adopted ProVerif's approach to proving equivalences.)

Using ProVerif, it is now possible to verify large parts of industrial-strength protocols, such as TLS 3, Signal 65, JFK 38, and Web Services Security 48, against powerful adversaries that can run an unlimited number of protocol sessions, for strong security properties expressed as correspondence queries or equivalence assertions. ProVerif is used by many teams at the international level, and has been used in more than 140 research papers (references).

Verifying cryptographic applications using F*

Verifying the implementation of a protocol has traditionally been considered much harder than verifying its model. This is mainly because implementations have to consider real-world details of the protocol, such as message formats 72, that models typically ignore. So even if a protocol has been proved secure in theory, its implementation may be buggy and insecure. However, with recent advances in both program verification and symbolic protocol verification tools, it has become possible to verify fully functional protocol implementations in the symbolic model. One approach is to extract a symbolic protocol model from an implementation and then verify the model, say, using ProVerif. This approach has been quite successful, yielding a verified implementation of TLS in F# 47. However, the generated models are typically quite large and whole-program symbolic verification does not scale very well.

An alternate approach is to develop a verification method directly for implementation code, using well-known program verification techniques. We design and implement the programming language F* 9, 39, 67, in collaboration with Microsoft Research. F* is an ML-like functional programming language aimed at program verification. Its type system includes polymorphism, dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and interactive proofs. Programs written in F* can be translated to efficient OCaml, F#, or C for execution 71. The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest 45 (a larger collaboration with Microsoft Research). This includes a verified implementation of TLS 1.2 and 1.3 46 and of the underlying cryptographic primitives 10. More recently, we have built a new symbolic protocol verification framework in F* called DY*  44 and used it to verify real-world cryptographic protocols like Signal, ACME and Noise.

7.1.1 F*

• Name:
  FStar
• Keywords:
  Programming language, Software Verification
• Functional Description:
  F* is a new higher order, effectful programming language (like ML) designed with program verification in mind. Its type system is based on a core that resembles System Fw (hence the name), but is extended with dependent types, refined monadic effects, refinement types, and higher kinds. Together, these features allow expressing precise and compact specifications for programs, including functional correctness properties. The F* type-checker aims to prove that programs meet their specifications using an automated theorem prover (usually Z3) behind the scenes to discharge proof obligations. Programs written in F* can be translated to OCaml, F#, or JavaScript for execution.
• URL:
  https://­www.­fstar-lang.­org/
• Contact:
  Aymeric Fromherz
• Participants:
  Antoine Delignat-Lavaud, Catalin Hritcu, Cedric Fournet, Chantal Keller, Karthikeyan Bhargavan, Pierre-Yves Strub, Aymeric Fromherz

7.1.2 Steel

• Name:
  Steel
• Keywords:
  Program verification, Separation Logic
• Functional Description:
  Steel is a framework for the verification of low-level, concurrent software, and is implemented in the F* dependently-typed programming language. Steel combines a strong, expressive concurrent separation logic to reason about complex concurrency patterns with a high level of automation, mixing custom separation logic decision procedures implemented as F* tactics with generic SMT solving to provide safety and functional correctness guarantees about Steel programs. Steel programs can be translated to executable C code to be integrated in unverified projects.
• News of the Year:
  Development of additional core libraries for Steel. Development of a verified key-value store, FastVer2, using the framework.
• Publications:
  hal-04104143, hal-02936273, hal-03466397, hal-03626859
• Contact:
  Aymeric Fromherz
• Participant:
  Aymeric Fromherz

7.1.3 HACL*

• Name:
  High Assurance Cryptography Library
• Keywords:
  Cryptography, Software Verification
• Functional Description:

  HACL* is a formally verified cryptographic library in F*, developed by the Prosecco team at INRIA Paris in collaboration with Microsoft Research, as part of Project Everest.

  HACL stands for High-Assurance Cryptographic Library and its design is inspired by discussions at the HACS series of workshops. The goal of this library is to develop verified C reference implementations for popular cryptographic primitives and to verify them for memory safety, functional correctness, and secret independence.

• News of the Year:
  We extended support for SIMD vectorization, and implemented and verified a generic streaming API for block-based algorithms. The instantiation of this streaming API for hashes (SHA-2, Blake2) was integrated into CPython.
• URL:
  https://­github.­com/­hacl-star/­hacl-star
• Publications:
  hal-04301439, hal-03154278, hal-03154275, hal-02294935, hal-01588421
• Contact:
  Aymeric Fromherz
• Participants:
  Karthikeyan Bhargavan, Aymeric Fromherz

7.1.4 DY*

• Name:
  DY*
• Keywords:
  Software Verification, Cryptographic protocol
• Functional Description:
  DY* is a recently proposed formal verification framework for the symbolic security analysis of cryptographic protocol code written in the F* programming language. Unlike automated symbolic provers, DY* accounts for advanced protocol features like unbounded loops and mutable recursive data structures as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Protocols modeled in DY* can be executed, and hence, tested, and they can even interoperate with real-world counterparts. DY* extends a long line of research on using dependent type systems but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. With this, one can uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security. DY* has been applied to the formal analysis of advanced cryptographic protocols such as Signal, ACME, Noise and MLS.
• News of the Year:

  We developed the tooling around DY* to tackle more complex protocols, and did case studies using this new tooling.

  In the past, message formats were written by hand in protocol analysis done with DY*, a process that is both tedious and error-prone. We developed Comparse, a tool to automatically generate messages formats in F*. The generated message formats are usable in DY*, and correspond to the ones defined in protocol specifications.

  Cryptographic protocols are often analyzed in isolation. However, they are typically deployed within a stack of protocols, where each layer relies on the security guarantees provided by the protocol layer below it, and in turn provides its own security functionality to the layer above. We extended DY* with a new methodology that allows analysts to modularly analyze each layer in a way that compose to provide security for a protocol stack.

  We used DY* to study MLS, a novel secure group messaging protocol. Most cryptographic protocols within the reach of formal analysis are between a fixed number of participants (often two) that exchange a fixed number of messages. MLS gives new challenges for analysts, because it supports group members joining and leaving the group over time, and group members can exchange an unbounded number of messages. We used DY* to study TreeSync, a sub-protocol of MLS that specifies the shared group state, defines group management operations, and ensures consistency, integrity, and authentication for the group state across all members.

• URL:
  https://­reprosec.­org/
• Publications:
  hal-03178425, hal-03540403, hal-03540824, hal-04255953, hal-04310972
• Contact:
  Karthikeyan Bhargavan

7.1.5 Hacspec

• Keywords:
  Specification language, Rust
• Functional Description:
  Hacspec is a domain specific language embedded inside Rust geared towards cryptographic specifications. It allows easier communication between formal methods experts and cryptographers that write their implementations in Rust. Hacspec compiles to various proof backends including F* and Coq.
• News of the Year:

  Hacspec was re-implemented entirely and renamed as Hax (https://­github.­com/­hacspec/­hax).

  Hacspec was aiming at being a specification language for crypto primitives in a DSL embedded in Rust. Hax extends the scope of the project, targeting a large subset of Rust, and translating it to various formal backends (such as Coq, F*, EasyCrypt or ProVerif).

  We now call Hacspec the functional subset of Rust that can be used, together with a Hacspec standard library, to write succinct, executable, and verifiable specifications in Rust. These specifications can be translated into formal languages with hax.

• URL:
  https://­hacspec.­github.­io/
• Publication:
  hal-03176482
• Contact:
  Karthikeyan Bhargavan
• Partners:
  Concordium Blockchain Research Center, Aarhus University, Denmark, Université de Porto

7.1.6 Aeneas

• Keywords:
  Rust, Compilers, Program verification
• Functional Description:
  Aeneas is a compilation pipeline for safe Rust programs. Aeneas leverages the Rust type system to compile Rust programs to pure, executable models (i.e., pure, functional versions of the original Rust programs). The key idea behind Aeneas' compilation is that, under the proper restrictions, a Rust function is fully characterized by a forward function, which computes its return value at call site, and a set of backward functions (one per lifetime), which propagate changes back into the environment upon ending lifetimes, thus accounting for side effects. Such forward and backward functions behave similarly to lenses. Relying on theorem provers to state and prove lemmas about those models, it is then possible to enforce guarantees about the original programs. For instance, one can prove panic freedom and functional correctness, but also security guarantees like authentication and confidentiality in the case of cryptographic protocols, and potentially more.
• News of the Year:
  We expanded the subset of Rust supported by Aeneas in many directions, for instance by adding better support for arrays, slices, binary operations and, more importantly, loops. We also added support for several backends: in addition to the original F* backend, it is now possible to generate Coq, Lean and HOL4 code. For the particular cases of HOL4 and Lean, we implemented an encoding which allows to define partial functions, and we provide basic proof automation for the proofs.
• URL:
  https://­github.­com/­AeneasVerif/­aeneas
• Publication:
  hal-03931572
• Contact:
  Son Ho

7.1.7 Charon

• Keywords:
  Rust, Compilers
• Functional Description:
  Charon is a driver which retrieves the Rust compiler output (more precisely, the generated MIR) and translates it to an intermediate language called LLBC (Low Level Borrow Calculus - an “easy-to-use” version of MIR in practice). Charon is meant as a user-friendly, stable interface with the Rust compiler, for the purpose of analyzing Rust programs.
• News of the Year:
  We expanded the subset supported by Charon by adding better support for arrays and slices, const generics, and function pointers and closures. We also performed minor improvements, for instance in the control flow graph reconstruction to generate more idiomatic code. Charon now also prints nice debugging messages in case of errors, in particular when it encounters unsupported features, which pinpoint the location and the cause of the error to the user, so that they can update their code or file an issue.
• URL:
  https://­github.­com/­AeneasVerif/­charon
• Publication:
  hal-03931572
• Contact:
  Son Ho

7.1.8 mlang

• Name:
  Mlang
• Keywords:
  Compilers, Legality
• Functional Description:
  In France, income tax is computed from taxpayers' individual returns, using an algorithm that is authored, designed and maintained by the French Public Finances Directorate (DGFiP). This algorithm relies on a legacy custom language and compiler originally designed in 1990, which unlike French wine, did not age well with time. Owing to the shortcomings of the input language and the technical limitations of the compiler, the algorithm is proving harder and harder to maintain, relying on ad-hoc behaviors and workarounds to implement the most recent changes in tax law. Competence loss and aging code also mean that the system does not benefit from any modern compiler techniques that would increase confidence in the implementation. We overhaul this infrastructure and present Mlang, an open-source compiler toolchain whose goal is to replace the existing infrastructure. Mlang is based on a reverse-engineered formalization of the DGFiP's system, and has been thoroughly validated against the private DGFiP test suite. As such, Mlang has a formal semantics, eliminates previous handwritten workarounds in C, compiles to modern languages (Python), and enables a variety of instrumentations, providing deep insights about the essence of French income tax computation. The DGFiP is now officially transitioning to Mlang for their production system.
• News of the Year:
  In 2023, Mlang is still being developed at DGFiP and tested for use in production. The income tax computation software compiled with Mlang now reproduces 100% of the behavior of the old tax computation software compiled with the legacy compiler. Extensions of the M language to soft-code rather than hard-code domain-specific terminology have been developed, and plans to add function calls are underway to finally get rid of the legacy C codebase.
• Publications:
  hal-02320347, hal-03002266
• Contact:
  Denis Merigoux
• Participant:
  Denis Merigoux
• Partner:
  Direction Générale des Finances Publiques (DGFiP)

7.1.9 Catala

• Keywords:
  Domain specific, Programming language, Law
• Functional Description:
  Catala is a domain-specific programming language designed for deriving correct-by-construction implementations from legislative texts. Its specificity is that it allows direct translation from the text of the law using a literate programming style, that aims to foster interdisciplinary dialogue between lawyers and software developers. By enjoying a formal specification and a proof-oriented design, Catala also opens the way for formal verification of programs implementing legislative specifications.
• News of the Year:
  In 2023, the development of Catala has sped up through the work of research engineer Louis Gesbert. The most notable addition is a module system that allows for real code modularization and separate compilation. The language has also gained its first industrial user, the DGFiP, with the start of a project to rewrite the income tax computation algorithm : https://­gitlab.­adullact.­net/­dgfip/­ir-catala.
• URL:
  https://­catala-lang.­org/­en
• Publications:
  hal-03712130, hal-03781578, hal-03128248, hal-03159939, hal-02936606, hal-03869335
• Contact:
  Denis Merigoux
• Participants:
  Denis Merigoux, Louis Gesbert, Aymeric Fromherz, Alain Delaet-tixeuil, Raphael Monat
• Partner:
  Université Panthéon-Sorbonne

7.1.10 ProVerif

• Keywords:
  Security, Verification, Cryptographic protocol
• Functional Description:

  ProVerif is an automatic security protocol verifier in the symbolic model (so called Dolev-Yao model). In this model, cryptographic primitives are considered as black boxes. This protocol verifier is based on an abstract representation of the protocol by Horn clauses. Its main features are:

  It can verify various security properties (secrecy, authentication, process equivalences).

  It can handle many different cryptographic primitives, specified as rewrite rules or as equations.

  It can handle an unbounded number of sessions of the protocol (even in parallel) and an unbounded message space.

• News of the Year:
  We released ProVerif version 2.05. The main novelties are that constraints are allowed in assumptions of queries, lemmas, axioms, and restrictions, and that attacker, table, mess, and user-defined predicates are allowed in conclusion of lemmas, axioms, and restrictions. We are working on many extensions (liveness properties, hash consing to save memory, more equational theories, ...). Stay tuned!
• URL:
  http://­proverif.­inria.­fr/
• Publications:
  hal-03366962, hal-01947972, hal-01423742, hal-01306440, hal-01423760, hal-01102136, hal-01575920, hal-01528752, hal-01575923, hal-01527671, hal-01575861
• Contact:
  Bruno Blanchet
• Participants:
  Bruno Blanchet, Marc Sylvestre, Vincent Cheval

7.1.11 CryptoVerif

• Name:
  Cryptographic protocol verifier in the computational model
• Keywords:
  Security, Verification, Cryptographic protocol
• Functional Description:
  CryptoVerif is an automatic protocol prover sound in the computational model. In this model, messages are bitstrings and the adversary is a polynomial-time probabilistic Turing machine. CryptoVerif can prove secrecy and correspondences, which include in particular authentication. It provides a generic mechanism for specifying the security assumptions on cryptographic primitives, which can handle in particular symmetric encryption, message authentication codes, public-key encryption, signatures, hash functions, and Diffie-Hellman key agreements. It also provides an explicit formula that gives the probability of breaking the protocol as a function of the probability of breaking each primitives, this is the exact security framework.
• News of the Year:

  The main new features of the year are:

  1) CryptoVerif can now translate its assumptions into EasyCrypt, so that these assumptions can be proved in EasyCrypt from lower-level or more standard assumptions (by Christian Doczkal, Pierre-Yves Strub, Pierre Boutry, Bruno Blanchet).

  2) CryptoVerif can generate implementations of protocols in F*. It also generates F* lemmas for equational properties assumed in CryptoVerif (by Benjamin Lipp and Bruno Blanchet).

  3) The oracle front-end is now the main front-end. Processes input in the channel front-end are translated into the oracle front-end (by Charlie Jacomme and Bruno Blanchet).

  4) We added notions of secrecy as reachability and secrecy for a bit.

  5) We added the diff[.,.] construct, already present in ProVerif, which allows to prove indistinguishability between two similar protocols.

  6) We extended the "move" command so that it can move random number generations and assignments upwards in the game.

  These changes are included in CryptoVerif version 2.08 available at https://­cryptoverif.­inria.­fr.

• URL:
  http://­cryptoverif.­inria.­fr/
• Publications:
  hal-03113251, hal-03471218, hal-04246199, hal-04253820, hal-01947959, hal-01764527, hal-02396640, hal-02100345, tel-01112630, hal-01102382, hal-01528752, hal-01575920, hal-01575861, hal-01575923
• Contact:
  Bruno Blanchet
• Participants:
  Bruno Blanchet, David Cadé, Benjamin Lipp, Pierre-Yves Strub, Christian Doczkal, Pierre Boutry

7.1.12 Squirrel

• Name:
  Squirrel Prover
• Keywords:
  Proof assistant, Cryptographic protocol
• Functional Description:

  Squirrel is an interactive proof assistant dedicated to the formal verification of cryptographic protocols in the computational model. It is based on a higher-order probabilistic logic which supports generic mathematical reasoning as well as cryptographic-specific reasoning.

  Concretely, Squirrel allows to specify security protocols in a variant of the applied pi-calculus, and properties of those protocols using its probabilistic logic. Then, these properties are to be proved by the users through tactics. Squirrel supports protocols with unbounded replication and persistent state, and can express both correspondence (e.g. authentication) and indistinguishability properties (e.g. strong secrecy, unlinkability).

• News of the Year:
  Support for higher-order functions and reasoning. Extension of Squirrel cryptographic rules to handle key corruption. New user documentation at: https://­squirrel-prover.­github.­io/­documentation/
• URL:
  https://­squirrel-prover.­github.­io/
• Publications:
  hal-03981949, hal-03620358, hal-03172119, hal-03264227
• Contact:
  Adrien Koutsos
• Participants:
  David Baelde, Stephanie Delaune, Charlie Jacomme, Solene Moreau, Adrien Koutsos, Justine Sauvage, Thomas Rubiano, Clément Herouard
• Partners:
  IRISA, ENS Rennes

7.1.13 Easycrypt

• Keywords:
  Proof assistant, Cryptography
• Functional Description:
  EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs. EasyCrypt can also be used for reasoning about differential privacy.
• Release Contributions:
  This versions introduces a new logic (ehoare) allowing to bound the expectation of a function in a probabilistic program.
• URL:
  https://­github.­com/­EasyCrypt/­easycrypt
• Publications:
  hal-03352062, hal-03469015
• Contact:
  Gilles Barthe
• Participants:
  Benjamin Grégoire, Gilles Barthe, Pierre-Yves Strub, Adrien Koutsos

7.1.14 IPDL

• Name:
  Interactive Probabilistic Dependency Logic
• Keywords:
  Verification, Cryptographic protocol
• Functional Description:
  A process calculus for computationally sound approximate reasoning about distributed cryptographic protocols in a manner both close to the Universal Composability-style simulation paradigm and amenable for formal verification.
• Contact:
  Kristina Sojakova

Session equivalence

Tamarin and ProVerif are both able to verify equivalence properties but are intuitively limited to the fine-grained diff-equivalence, that is often not well suited for privacy-type properties such as anonymity and unlinkability. This limitation has always been a hard hurdle to overcome as the technique did not evolve in more than 15 years. In a paper at CSF'23 21, we (Vincent Cheval , with Itsaka Rakotonirina) finally introduced in ProVerif a new proof technique for verifying equivalence in a general framework. Our technique is based on the notion of session decomposition, inspired from the symmetry reductions in  56. We applied our results on several protocols such as LAK, PACE, a simplified TLS, ...

Advanced primitive modelings

Real life implementations of cryptographic primitives have many behaviors and weaknesses that are not captured by classical symbolic modelings. To bridge this gap, we extensively studied the concretely used hash functions and Authenticated Encryptions with Additional Data (AEADs) and proposed for each of those primitives novel and more faithful models leading to two publications at USENIX Security'23, 19 by Vincent Cheval , Cas Cremers, Alexander Dax, Lucca Hirschi, Charlie Jacomme , and Steve Kremer and 22 by Cas Cremers, Alexander Dax, Charlie Jacomme , and Mang Zhao. Those new models were notably deployed in ProVerif and Tamarin, and were used to analyze several new protocols for which new subtle weaknesses were discovered.

Applications

We performed several major case studies using the new features introduced in ProVerif. In EuroS&P'23 20, we (Vincent Cheval , with José Moreira and Mark Ryan) provided the first formal verification of two transparency protocols with a precise model of the Merkle tree data structure: transparent decryption (sometimes called accountable decryption), and certificate transparency. In CSF'23 18, we (Vincent Cheval , with Véronique Cortier and Alexandre Debant) proved the end-to-end verifiability of multiple electronic voting systems: Helios, Belenios, CHVote and SwissPost. All these proofs relied on a new complete characterization of end-to-end verifiability, a new generic election framework in which voting protocols can be expressed, and a library of lemmas for the automatic proof of end-to-end verifiability.

In USENIX Security'23 25, we (Charlie Jacomme , with Elise Klein, Steve Kremer, and Maïwenn Racouchot) verified an IETF draft for LAKE EDHOC using our platform Sapic+  55. This platform allows us to leverage the complementary strengths of ProVerif, Tamarin, and DeepSec from a single model, by translating that model to inputs of the various tools. The analysis was carried out with a fine-grained modeling of possible threat models and compromise, and lead to the discovery of multiple weaknesses, with the proposal of fixes that were integrated into new versions of the draft.

In USENIX Security'23 23, we (Charlie Jacomme , with Cas Cremers and Aurora Naska) verified the session management layer of the Signal application, Sesame, using Tamarin. This lead to the discovery that guarantees formally proved on the lower layers protocol are not preserved when considering the full application. We were able to experimentally demonstrate the identified weaknesses, and we proposed and verified simple fixes to the protocol.

Protocols with probabilistic choice

In general, symbolic models are purely non-deterministic (or possibilistic). For instance, random numbers are abstracted and are assumed to be impossible to guess by the attacker. While this is generally sensible, it is not always possible to eliminate probabilities altogether as some protocols specifically rely on non-negligible choices in their specification. In  54, we (Vincent Cheval , with Raphaëlle Crubillé and Steve Kremer) considered a framework for symbolic protocol analysis with probabilistic choice. We showed the relations between possibilistic and probabilistic equivalences and designed a decision procedure for probabilistic trace equivalence. This procedure has been implemented in DeepSec. In 2023, we published a long version of this paper in the Journal of Computer Security 12.

CryptoVerif

We (Bruno Blanchet ) continued the development of CryptoVerif, adding new game transformations in order to deal with the dynamic compromise of keys, which allowed us to complete missing proofs of forward secrecy in major previous case studies (TLS 1.3 3 and WireGuard  66). We also added game transformations that guess values, a step often used in cryptographic proofs 32, 31. This work is accepted at CSF'24.

We (Bruno Blanchet and Charlie Jacomme ) showed that CryptoVerif is sound against quantum adversaries 33.

We (Karthikeyan Bhargavan , Bruno Blanchet , with Benjamin Lipp) developed a translation from CryptoVerif to F${}^{☆}$, which allows us to generate running implementations of protocols verified in CryptoVerif. An important addition with respect to a previous translation to OCaml is that we generate F${}^{☆}$ lemmas for equations used as assumptions in CryptoVerif; these lemmas are then proved in F${}^{☆}$. We (Bruno Blanchet , with Pierre Boutry, Christian Dockzal, Benjamin Grégoire, and Pierre-Yves Strub) also developed a translation from the security assumptions used in CryptoVerif to EasyCrypt 30. Indeed, the security assumptions in CryptoVerif are often stated in a way that differs from the usual cryptographic assumptions. This translation allows us to prove the CryptoVerif assumptions from more standard or lower-level assumptions in EasyCrypt. This work is accepted at CSF'24. All these developments are included in CryptoVerif 2.08.

Squirrel

Squirrel is an interactive theorem prover dedicated to the verification of cryptographic protocols in the computational model. The Squirrel prover, first introduced in 2, encodes cryptographic protocols and their properties into a pure probabilistic logic, and supports generic as well as cryptographic-specific reasoning.

At LICS'23 17, we (Adrien Koutsos , with David Baelde and Joseph Lallemand) proposed a complete re-design of Squirrel theoretical foundations, which is less ad hoc, simpler, more general, and supports higher-order reasoning. Additionally, this new logical presentation was used to allow Squirrel cryptographic rules to support key corruption.

We also have work in progress on techniques to allow users to easily add new cryptographic primitives and assumptions to Squirrel without modifying the tool itself (PhD thesis of Justine Sauvage ).

Currently, Squirrel only supports the verification of cryptographic protocols in the asymptotic security model, which limits Squirrel reasoning capabilities (some cryptographic arguments are out-of-scope, e.g. polynomial hybrid arguments) and expressivity (Squirrel cannot give a precise bound on the probability of breaking protocol security). We are working on overcoming these limitations by adapting Squirrel to a concrete security setting (PhD thesis of Théo Vignon ).

EasyCrypt

EasyCrypt is a theorem prover designed for reasoning about properties of probabilistic computations with adversarial code, using imperative program logics implemented on top of a higher-order ambient logic. Its main application is the construction and verification of game-based cryptographic primitives.

While EasyCrypt is mainly developed outside of Prosecco at PQShield and the SPLiTS Inria team at Sophia-Antipolis, we (Adrien Koutsos , with Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, and Pierre-Yves Strub) have presented in CCS'21  41 an extension of EasyCrypt with a new program logic allowing us to reason about the computational worst-case complexity of adversarial programs. This logic can be used to prove precise relationships between the complexity of cryptographic adversaries and their success probability, allowing us to obtain fully mechanized cryptographic reductions. We showcased our approach through a new formalization of the Universal Composability framework. In 2023, we published a journal version this work at ACM ToPS 11).

IPDL

In 24, we (Kristina Sojakova , with Joshua Gancher, Xiong Fan, Elaine Shi, and Greg Morrisett) present a novel technique for proving UC-security of a class of cryptographic protocols, based on a equational calculus at the protocol level, named IPDL.

Evolution, Semantics, and Engineering of the F* Verification System

Participants: Aymeric Fromherz, Karthikeyan Bhargavan, Théo Laurent.

• Grant from Nomadic Labs - Inria
• PIs: Aymeric Fromherz (earlier, Catalin Hritcu, Exequiel Rivas)
• Duration: March 2019 - April 2023

• Abstract: While the F* verification system shows great promise in practice, many challenging conceptual problems remain to be solved, many of which can directly inform the further evolution and design of the language. Moreover, many engineering challenges remain in order to build a truly usable verification system. This proposal promises to help address this by focusing on the following 5 main topics:

  (1) Generalizing Dijkstra monads, i.e., a program verification technique for arbitrary monadic effects; (2) Relational reasoning in F*: devising scalable verification techniques for properties of multiple program executions (e.g., confidentiality, noninterference) or of multiple programs (e.g., program equivalence); (3) Making F*'s effect system more flexible, by supporting tractable forms of effect polymorphism and allowing some of the effects of a computation to be hidden if they do not impact the observable behavior; (4) Working out more of the F* semantics and metatheory; (5) Solving the engineering challenges of building a usable verification system.

Cybercampus CIRCUS funding

Participants: Aymeric Fromherz.

Creating Innovative and Robust Cryptographic Solutions.

• Partners: Inria Paris/EPI Prosecco, Cryspen.
• Prosecco PI: Aymeric Fromherz
• Abstract: This project aims to build a new integrated development and verification environment (IDVE) called Circus that is targeted at software developers and security architects. The main partner for this technical transfer is Cryspen, a new company spun off from Prosecco that aims to create innovative cryptographic solutions. The Circus IDVE targets the Rust language, and consists of several tools developed at Prosecco, such as hacspec and Aeneas, while relying on well-established verification tools for the verification of safety, correctness, and security properties about critical software.

10.1.1 Inria associate team not involved in an IIL or an international program

10.2.1 Horizon Europe

10.3.1 PEPR

11.1.1 Scientific events: organisation

11.1.2 Scientific events: selection

11.1.3 Journal

11.1.4 Invited talks

• Denis Merigoux : Invited talk at CRCL'23

11.2.1 Teaching

• Master: Bruno Blanchet , Cryptographic protocols: formal and computational proofs, 27h equivalent TD, master M2 MPRI, université Paris VII
• Master: Adrien Koutsos , Cryptographic protocols: formal and computational proofs, 27h equivalent TD, master M2 MPRI, université Paris VII

11.2.2 Supervision

• PhD in progress: Théo Vignon , Exploring the limits of the CCSA approach to computational security, since September 2023, supervised by Caroline Fontaine, Guillaume Scerri, and Adrien Koutsos .
• PhD in progress: Alain Delaët-Tixeuil , Interactive verification for programs deriving from legal specifications, since September 2022, supervised by Sandrine Blazy and Denis Merigoux .
• PhD in progress: Antonin Reitz , A Methodology for Programming and Verifying Secure Systems, since November 2022, supervised by Bruno Blanchet and Aymeric Fromherz .
• PhD in progress: Justine Sauvage , Games and Logic for the Verification of Cryptographic Protocols, since September 2022, supervised by Bruno Blanchet , David Baelde, and Adrien Koutsos .
• PhD in progress: Son Ho , Verification of Rust Programs, since September 2020, supervised by Karthikeyan Bhargavan , Bruno Blanchet , and Jonathan Protzenko .
• PhD in progress: Théophile Wallez , Verification of Cryptographic Protocols, since September 2021, supervised by Karthikeyan Bhargavan , Bruno Blanchet , and Jonathan Protzenko .
• PhD in progress: Théo Laurent , Dependent types and subtyping, since July 2020, supervised by David Delahaye, Bruno Blanchet , and Kenji Maillard.
• M2 internship: Rémy Citerin , Coinduction in F* and application to interaction trees, supervised by Aymeric Fromherz and Théo Laurent .

International journals

• 11 articleM.Manuel Barbosa, G.Gilles Barthe, B.Benjamin Grégoire, A.Adrien Koutsos and P.-Y.Pierre-Yves Strub. Mechanized Proofs of Adversarial Complexity and Application to Universal Composability: Journal pre-print: full version.ACM Transactions on Privacy and Security263August 2023, 1-34HALDOIback to text
• 12 articleV.Vincent Cheval, R.Raphaëlle Crubillé and S.Steve Kremer. Symbolic protocol verification with dice: Process equivalences in the presence of probabilities.Journal of Computer SecurityJune 2023, 1-38HALDOIback to text
• 13 articleS.Son Ho, A.Aymeric Fromherz and J.Jonathan Protzenko. Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification.Proceedings of the ACM on Programming Languages7ICFPAugust 2023, 385-416HALDOIback to text
• 14 articleD.Denis Merigoux, M.Marie Alauzen and L.Lilya Slimani. Rules, Computation and Politics: Scrutinizing Unnoticed Programming Choices in French Housing Benefits.Journal of Cross-disciplinary Research in Computational Law142023HALback to textback to text

International peer-reviewed conferences

• 15 inproceedingsD.Daniel de Almeida Braga, N.Natalia Kulatova, M.Mohamed Sabt, P.-A.Pierre-Alain Fouque and K.Karthikeyan Bhargavan. From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake.EuroS&P 2023 - IEEE 8th European Symposium on Security and PrivacyDelft, NetherlandsIEEEJuly 2023, 707-723HALDOIback to text
• 16 inproceedingsA.Arvind Arasu, T.Tahina Ramananandro, A.Aseem Rastogi, N.Nikhil Swamy, A.Aymeric Fromherz, K.Kesha Hietala, B.Bryan Parno and R.Ravi Ramamurthy. FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores.CPP '23 - 12th ACM SIGPLAN International Conference on Certified Programs and ProofsBoston (MA), United StatesACMJanuary 2023, 30-46HALDOIback to text
• 17 inproceedingsD.David Baelde, A.Adrien Koutsos and J.Joseph Lallemand. A Higher-Order Indistinguishability Logic for Cryptographic Reasoning.LICSBoston, United StatesIEEEJune 2023, 1-13HALDOIback to text
• 18 inproceedingsV.Vincent Cheval, V.Véronique Cortier and A.Alexandre Debant. Election Verifiability with ProVerif.CSF 2023 - 36th IEEE Computer Security Foundations SymposiumDubrovnik, CroatiaJuly 2023HALback to text
• 19 inproceedingsBest paperV.Vincent Cheval, C.Cas Cremers, A.Alexander Dax, L.Lucca Hirschi, C.Charlie Jacomme and S.Steve Kremer. Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses.32nd USENIX Security SymposiumAnaheim, United States2023HALback to textback to text
• 20 inproceedingsV.Vincent Cheval, J.José Moreira and M.Mark Ryan. Automatic verification of transparency protocols.2023 IEEE 8th European Symposium on Security and Privacy (EuroS&P)2023 IEEE 8th European Symposium on Security and Privacy (EuroS&P)Delft, NetherlandsIEEEJuly 2023HALDOIback to text
• 21 inproceedingsBest paperV.Vincent Cheval and I.Itsaka Rakotonirina. Indistinguishability Beyond Diff-Equivalence in ProVerif.2023 IEEE 36th Computer Security Foundations Symposium (CSF)2023 IEEE 36th Computer Security Foundations Symposium (CSF)Dubrovnik, CroatiaIEEEJuly 2023, 184-199HALDOIback to textback to text
• 22 inproceedingsBest paperC.Cas Cremers, A.Alexander Dax, C.Charlie Jacomme and M.Mang Zhao. Automated Analysis of Protocols that use Authenticated Encryption:How Subtle AEAD Differences can impact Protocol Security.32nd USENIX Security Symposium 2023Anaheim, United StatesAugust 2023HALback to textback to text
• 23 inproceedingsC.Cas Cremers, C.Charlie Jacomme and A.Aurora Naska. Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations.USENIX Security 2023 - 32nd USENIX Security SymposiumAnaheim, United States2023HALback to text
• 24 inproceedingsJ.Joshua Gancher, K.Kristina Sojakova, X.Xiong Fan, E.Elaine Shi and G.Greg Morrisett. A Core Calculus for Equational Proofs of Cryptographic Protocols.POPL 2023 - 50th ACM SIGPLAN Symposium on Principles of Programming LanguagesBoston, United StatesJanuary 2023HALDOIback to text
• 25 inproceedingsC.Charlie Jacomme, E.Elise Klein, S.Steve Kremer and M.Maïwenn Racouchot. A comprehensive, formal and automated analysis of the EDHOC protocol.USENIX Security '23 - 32nd USENIX Security SymposiumAnaheim, CA, United StatesAugust 2023HALback to text
• 26 inproceedingsBest paperT.Théophile Wallez, J.Jonathan Protzenko, B.Benjamin Beurdouche and K.Karthikeyan Bhargavan. TreeSync: Authenticated Group Management for Messaging Layer Security.USENIX Security '23Anaheim, United StatesAugust 2023HALback to textback to textback to text
• 27 inproceedingsT.Théophile Wallez, J.Jonathan Protzenko and K.Karthikeyan Bhargavan. Comparse: Provably Secure Formats for Cryptographic Protocols.CCS '23: ACM SIGSAC Conference on Computer and Communications SecurityCopenhagen, DenmarkACMNovember 2023, 564-578HALDOIback to text

National peer-reviewed Conferences

• 28 inproceedingsT.Théophile Wallez. Vérification symbolique de protocoles cryptographiques en F*: application au sous-protocole TreeSync de MLS.Journées Francophones des Langages ApplicatifsJFLA 2023 - 34èmes Journées Francophones des Langages ApplicatifsPraz-sur-Arly, FranceJanuary 2023, 243-263HAL

Conferences without proceedings

• 29 inproceedingsD.Denis Merigoux. Experience report: implementing a real-world, medium-sized program derived from a legislative specification.Programming Languages and the Law 2023 (affiliated with POPL)Boston (MA), United StatesJanuary 2023HALback to textback to text

Reports & preprints

• 30 miscB.Bruno Blanchet, P.Pierre Boutry, C.Christian Doczkal, B.Benjamin Grégoire and P.-Y.Pierre-Yves Strub. CV2EC: Getting the Best of Both Worlds.December 2023HALback to text
• 31 reportB.Bruno Blanchet. CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels).RR-9525Inria ParisOctober 2023, 166HALback to text
• 32 miscB.Bruno Blanchet. Dealing with Dynamic Key Compromise in CryptoVerif.November 2023HALback to text
• 33 reportB.Bruno Blanchet and C.Charlie Jacomme. CryptoVerif: a Computationally-Sound Security Protocol Verifier.RR-9526InriaOctober 2023, 194HALback to text
• 34 miscV.Vincent Cheval, R.Raphaëlle Crubillé and S.Steve Kremer. Symbolic protocol verification with dice: process equivalences in the presence of probabilities (extended version).May 2023HAL
• 35 reportS.Son Ho, J.Jonathan Protzenko and A.Aymeric Fromherz. Aeneas: Rust Verification by Functional Translation.Inria ParisApril 2023HALback to text
• 36 miscT.Théo Laurent, M.Meven Lennon-Bertrand and K.Kenji Maillard. Definitional Functoriality for Dependent (Sub)Types.October 2023HAL