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 29.

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  56; it has motivated a serious research effort on the formal analysis of cryptographic protocols, starting with  42 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 protocols38. 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 36, 25, correspondences (including authentication) 37, and observational equivalences 35. 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 51, JFK 26, and Web Services Security 34, 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 60, 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# 33. 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, 27, 53, 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 59. The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest 31 (a larger collaboration with Microsoft Research). This includes a verified implementation of TLS 1.2 and 1.3 32 and of the underlying cryptographic primitives 10. More recently, we have built a new symbolic protocol verification framework in F* called DY* 30 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. Extension of extraction facilities, particularly for concurrency primitives. Application to StarMalloc, a verified, concurrent, hardened memory allocator.
• URL:
  https://­github.­com/­FStarLang/­steel
• Publications:
  hal-04104143, hal-02936273, hal-03466397, hal-03626859
• Contact:
  Aymeric Fromherz
• Participant:
  Aymeric Fromherz
• Partner:
  Microsoft

7.1.3 StarMalloc

• Keywords:
  Memory Allocation, Program verification, Separation Logic
• Functional Description:
  StarMalloc is a concurrent, security-oriented, formally verified memory allocator. The functional correctness and memory safety of StarMalloc have been formally established in F*, using the Steel concurrent separation logic. StarMalloc provides all APIs expected from a modern allocator, and was tested with a wide range of applications, including Firefox, Redis, or Z3.
• News of the Year:

  StarMalloc was publicly released, including an entire formally verified development using the Steel concurrent separation logic, as the extracted, executable C code packaged as a standalone, easily deployable artefact. In addition to the APIs and functionalities expected from a modern allocator, the work included the verified development of several security features, including segregated metadata, quarantine, guard pages, and canaries.

  StarMalloc was presented at OOPSLA 2024.

• URL:
  https://­github.­com/­Inria-Prosecco/­StarMalloc
• Publication:
  hal-04837244
• Contact:
  Aymeric Fromherz
• Participants:
  Aymeric Fromherz, Antonin Reitz

7.1.4 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 the previously developed streaming API to a wider range of hashes (SHA-1, other variants of SHA-2, SHA-3), which were integrated into CPython, the reference implementation of the Python language. We additionally developed a streaming version of HMAC, supporting all HACL* hashes.
• 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.5 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:
  Theophile Wallez

7.1.6 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, Université de Porto

7.1.7 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 further extended the subset of Rust supported by Aeneas, including a better support for loops and branches, as well as a support for traits. Additionally, we extended the automation of the Lean backend using metaprogramming to improve the verification experience of using Aeneas.
• URL:
  https://­github.­com/­AeneasVerif/­aeneas
• Publications:
  hal-04837250, hal-03931572
• Contact:
  Aymeric Fromherz
• Participants:
  Son Ho, Aymeric Fromherz, Guillaume Boisseau

7.1.8 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 significantly expanded the subset supported by Charon, including support for unsafe code, associated types, quantified clauses, mutually recursive traits, and many other features. We additionally developed several new static analyses on top of Charon, including a port of the Rudra analyzer, and a analyzer for constant-time programming in cryptographic implementations.
• URL:
  https://­github.­com/­AeneasVerif/­charon
• Publication:
  hal-03931572
• Contact:
  Aymeric Fromherz
• Participants:
  Son Ho, Guillaume Boisseau, Aymeric Fromherz, Yoann Prak

7.1.9 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 2024, the DGFiP completed a first milestone for the integration of Mlang into their IT sytem, as for the first time, the income tax of all French people has been computed thanks to source code compiled with Mlang instead of the legacy DGFiP compiler. Extensions of the M language to soft-code rather than hard-code domain-specific terminology are being tested for productions, 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.10 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 2024, the development of Catala is undergoing an industrialization process with three research engineers working on the project, led by Denis Merigoux as the project manager. Beyond a new C89 backend for the compiler that enables integration to legacy backends used in public administrations, the team is now focusing on a new set of front-end features focused on developper tooling as well as algorithmic explainability. Indeed, explaining algorithmic decisions in the context of public service is both useful for the end-user (to know why the decision was issued), and the administration developers that need to debug and fix the system. A design study has begun this year to investigate how to interface the technical log data produced by Catala during execution with user-facing interfaces that satisfy both needs.
• URL:
  https://­catala-lang.­org/­en
• Publications:
  hal-04391612, hal-03712130, hal-03781578, hal-03128248, hal-03159939, hal-02936606, hal-03869335
• Contact:
  Denis Merigoux
• Participants:
  Vincent Botbol, Romain Primet, Denis Merigoux, Louis Gesbert, Aymeric Fromherz, Alain Delaet-Tixeuil, Raphael Monat
• Partner:
  Université Panthéon-Sorbonne

7.1.11 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.

• 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.12 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) We improved considerably the translation from CryptoVerif to F*. In particular, it can now translate security properties proved by CryptoVerif into F* axioms. We also support ghost types, for values useful in the CryptoVerif model but not in the F* implementation (e.g. keys of random oracles, which are a modeling artifact).

  2) The library of cryptographic primitives has been adapted to support quantum adversaries. In particular, we now have model for KEMs (Key Encapsulation Mechanisms) often used in post-quantum protocols. Moreover, we have a version of the library that contains only primitives with a known post-quantum instantiation, and we have models for primitives without security assumption (useful to model broken primitives, e.g., classical schemes in the presence of a quantum adversary).

  These changes are included in CryptoVerif version 2.11 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, hal-04321656, hal-04271666, hal-04577912, tel-01112630, hal-01102382, hal-01528752, hal-01575920, hal-01575861, hal-01575923
• Contact:
  Bruno Blanchet
• Participants:
  Charlie Jacomme, Bruno Blanchet, David Cade, Benjamin Lipp, Pierre-Yves Strub, Christian Doczkal, Pierre Boutry

7.1.13 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:

  Squirrel development continued, with several new features: i) namespaces: objects can now be stored in namespaces, which allows to organize large developments, ii) basic builtin support for integer and string constants, iii) SMT support, and iv), system variables: lemmas and axioms can now be parameterized by systems, bringing a form of system parametricity where system arguments are inferred during lemma's applications, as for type variables.

  In addition, participants of the project published in the ACM SIGLOG newsletter a full presentation of the up to date theory behind the tool.

• URL:
  https://­squirrel-prover.­github.­io/
• Publications:
  hal-04577828, hal-04511718, hal-04579038, hal-03981949, hal-03620358, hal-03172119, hal-03264227
• Contact:
  Adrien Koutsos
• Participants:
  David Baelde, Stephanie Delaune, Clément Herouard, Charlie Jacomme, Adrien Koutsos, Solene Moreau, Thomas Rubiano, Justine Sauvage, Theo Vignon
• Partners:
  IRISA, ENS Rennes

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 52). We also added game transformations that guess values, a step often used in cryptographic proofs. This work is published at CSF'24 17.

We (Bruno Blanchet and Charlie Jacomme) showed that CryptoVerif is sound against quantum adversaries. We used this result to obtain the first formal security guarantees over two IETF draft proposals designing post-quantum variants of SSH and TLS. This work is published at CSF'24 18.

We (Karthikeyan Bhargavan, Bruno Blanchet , Aymeric Fromherz , 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${}^{☆}$ axioms for security properties proved by CryptoVerif (these axioms can then be used in F${}^{☆}$ proofs) and lemmas for equations used as assumptions in CryptoVerif (these lemmas are then proved in F${}^{☆}$). We (Bruno Blanchet , Pierre Boutry, Christian Dockzal, Benjamin Grégoire, and Pierre-Yves Strub) also developed a translation from the security assumptions used in CryptoVerif to EasyCrypt. 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 published at CSF'24 16. All these developments are included in CryptoVerif 2.11.

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.

Squirrel's logic operates in the asymptotic security framework, This is a standard and established framework in the cryptographic community, which allows for simpler proofs by abstracting away irrelevant details, such as the probability of asymptotically negligible events, or small changes in the running times of the involved parties. Concrete security 61 is another established framework which requires the user to prove explicit bounds on the winning probability of the adversary. Because of the increased burden it puts on the user, we did not initially target this framework. Nonetheless, it has advantages: it allows to obtain precise security bounds, and it is required for some particular cryptographic reasoning steps (e.g. to handle uniformity in hybrid arguments 43). Recently, we showed how to extend Squirrel's logic to concrete security by adding new security predicate and a corresponding proof system. Further, we designed a novel proof-transformation technique which shows that a large class of asymptotic security proofs can be automatically rewritten into concrete security proofs, while improving their security bounds. This work, which is of a theoretical nature, has been published at CSF'24 14.

The CCSA logics and its implementation in Squirrel come with cryptographic axioms whose soundness derives from the security of standard cryptographic games, e.g. PRF, EUF, IND-CCA. Unfortunately, these axioms are complex to design and implement; so far, these tasks were manual, ad hoc and error-prone. Further, adding a new axiom required to modify the Squirrel tool itself, puting this task out-of-reach of the standard users. We solved these issues by providing a formal and systematic method for deriving axioms from cryptographic games. Our method relies on synthesizing an adversary against some cryptographic game, through the notion of bi-deduction. Concretely, we defined a rich notion of bi-deduction, justified how to use it to derive cryptographic axioms, provide a proof system for bi-deduction, and an automatic proof-search method. This work has been published at CSF'24 15 and included in the main version of Squirrel.

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

10.2.1 Visits of international scientists

10.3.1 PEPR

10.3.2 ANR

11.1.1 Scientific events: organisation

11.1.2 Scientific events: selection

11.1.3 Journal

11.1.4 Invited talks

• Adrien Koutsos : invited talk “Mechanizing and Automating Cryptographic Arguments”, May 2024, ETH Zurich, ProTeCS workshop (associated to EuroCrypt’24).
• Aymeric Fromherz : invited panel member, "Research, Grad School, Community - Let's Chat", Milan, September 2024, PLMW workshop (associated to ICFP 24)
• Aymeric Fromherz : Demi-heure de Science, "Améliorer la fiabilité d'implémentations cryptographiques optimisées à l'aide de vérification formelle", December 2024, Inria Paris.

11.2.1 Teaching

• Master: Bruno Blanchet , Proofs of security protocols, 36h equivalent TD, master M2 MPRI, université Paris VII
• Master: Adrien Koutsos , Proofs of security protocols, 18h equivalent TD, master M2 MPRI, université Paris VII
• Master: Aymeric Fromherz , Proofs of security protocols, 18h equivalent TD, master M2 MPRI, université Paris VII
• Summer school: Bruno Blanchet , CryptoVerif: Mechanizing Game-Based Proofs of Security Protocols, XXIII International School on Foundations of Security Analysis and Design (FOSAD'24), 6h.

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: 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.
• PhD in progress: Pierre Goutagny , PhD student in EPC SyCoMoRES (Inria, University of Lille, and CNRS) on Automated Verification of Catala Programs, since September 2024, supervised by Patrick Baillot, Raphael Monat, and Aymeric Fromherz .
• PhD defended: Son Ho , Verification of Rust Programs, defended on December 9, 2024, supervised by Karthikeyan Bhargavan, Bruno Blanchet , and Jonathan Protzenko  21.
• M2 internship: Ryan Lahfa , Formal verification of Rust programs with Aeneas and Lean, supervised by Aymeric Fromherz .

11.2.3 Juries

• Bruno Blanchet : reviewer of Maïwenn Racouchot's PhD thesis, Université de Lorraine.

International journals

• 11 articleD.David Baelde, S.Stéphanie Delaune, C.Charlie Jacomme, A.Adrien Koutsos and J.Joseph Lallemand. The Squirrel Prover and its Logic.ACM SIGLOG News112April 2024HALDOI
• 12 articleS.Son Ho, A.Aymeric Fromherz and J.Jonathan Protzenko. Sound Borrow-Checking for Rust via Symbolic Semantics.Proceedings of the ACM on Programming Languages8ICFPAugust 2024, 426-454HALDOIback to text
• 13 articleA.Antonin Reitz, A.Aymeric Fromherz and J.Jonathan Protzenko. StarMalloc: Verifying a Modern, Hardened Memory Allocator.Proceedings of the ACM on Programming Languages8OOPSLA2October 2024, 1757 - 1786HALDOIback to text

International peer-reviewed conferences

• 14 inproceedingsD.David Baelde, C.Caroline Fontaine, A.Adrien Koutsos, G.Guillaume Scerri and T.Théo Vignon. A Probabilistic Logic for Concrete Security.2024 IEEE 37th Computer Security Foundations Symposium (CSF)CSF 2024 - 37th IEEE Computer Security Foundations SymposiumEnschede, NetherlandsIEEE Computer Society2024, 324-339HALback to text
• 15 inproceedingsD.David Baelde, A.Adrien Koutsos and J.Justine Sauvage. Foundations for Cryptographic Reductions in CCSA Logics.CCS '24: ACM SIGSAC Conference on Computer and Communications SecurityProceedings of the 2024 ACM SIGSAC Conference on Computer and Communications SecuritySalt Lake City UT, United StatesACMDecember 2024, 2814-2828HALDOIback to text
• 16 inproceedingsB.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.CSF 2024 - 37th IEEE Computer Security Foundations SymposiumEnschede, NetherlandsJuly 2024, 283-298HALDOIback to text
• 17 inproceedingsB.Bruno Blanchet. Dealing with Dynamic Key Compromise in CryptoVerif.37th IEEE Computer Security Foundations SymposiumEnschede, NetherlandsJuly 2024, 495-510HALDOIback to text
• 18 inproceedingsB.Bruno Blanchet and C.Charlie Jacomme. Post-quantum sound CryptoVerif and verification of hybrid TLS and SSH key-exchanges.CSF'24 - 37th IEEE Computer Security Foundations SymposiumEnschede, NetherlandsJuly 2024, 543-556HALDOIback to text
• 19 inproceedingsP.Pierre Goutagny, A.Aymeric Fromherz and R.Raphaël Monat. CUTECat: Concolic Execution for Computational Law.ESOP 2025 - 34th European Symposium on ProgrammingHamilton, ON, CanadaMay 2025HAL
• 20 inproceedingsBest paperR.Raphaël Monat, A.Aymeric Fromherz and D.Denis Merigoux. Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law.Lecture Notes in Computer ScienceESOP 2024 - 33rd European Symposium on Programming14577Lecture Notes in Computer ScienceLuxembourg City, LuxembourgSpringer Nature SwitzerlandApril 2024, 421-450HALDOIback to textback to text

Doctoral dissertations and habilitation theses

• 21 thesisS.Son Ho. Formal Verification of Rust Programs by Functional Translation.Université PSL (Paris Sciences & Lettres)December 2024HALback to text

Reports & preprints

• 22 miscS.Sandrine Blazy, A.Alain Delaët and D.Denis Merigoux. Scaling Up Mechanized Proof Automation for Small-step Semantics.November 2024HAL
• 23 reportD.Denis Merigoux, M.Marie Alauzen, J.Justine Banuls, L.Louis Gesbert and É.Émile Rolley. From algorithmic transparency to automatized explanainability: Understanding IT, legal and organizational challenges.RR-9535INRIA ParisJanuary 2024, 68HAL

Software

• 24 softwareD.David Baelde, A.Adrien Koutsos and J.Justine Sauvage. Artifact for "Foundations for Cryptographic Reductions in CCSA Logics".August 2024 lic: MIT License; GNU Library General Public License v2 only; cecill.HAL