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. Our current focus is on designing and implementing the programming language F*, in collaboration with Microsoft Research. F* (pronounced F star) is a general-purpose functional programming language with effects 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 case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest (a larger collaboration with Microsoft Research). This includes verified implementations of TLS 1.2 and 1.3 and of the underlying cryptographic primitives.

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, the reverse engineering and formal test tool Tookan, and the F* verification system. 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 prover CryptoVerif, 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 symbolic and computational verification, such as computational soundness results that enable computational proofs by symbolic techniques.

Efficient formally secure compilers for tagged architectures

We aim to leverage emerging hardware capabilities for fine-grained protection to build the first, efficient secure compilation chains for realistic low-level programming languages (the C language, and Low* a safe subset of C embedded in F* for verification). These compilation chains will provide a secure semantics for all programs and will ensure that high-level abstractions cannot be violated even when interacting with untrusted low-level code. To achieve this level of security without sacrificing efficiency, our secure compilation chains target a tagged architecture, which associates a metadata tag to each word and efficiently propagates and checks tags according to software-defined rules.

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  49; it has motivated a serious research effort on the formal analysis of cryptographic protocols, starting with  45 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 protocols42. 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 40, 29, correspondences (including authentication) 41, and observational equivalences 39. 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 34, Signal 47, JFK 30, and Web Services Security 38, 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 120 research papers (references available at http://proverif.inria.fr/proverif-users.html).

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 51, 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# 37. 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. Our current focus is on designing and implementing the programming language F* 53, 33, 48, 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 50. The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest 35 (a larger collaboration with Microsoft Research). This includes a verified implementation of TLS 1.2 and 1.3 36 and of the underlying cryptographic primitives 54.

7.1.1 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) The command "use_variable x1 ... xn", which tells CryptoVerif to replace all terms equal to the value of the variable xi with xi.

  2) The command "guess i" to guess the tested session, a technique often used in cryptographic proofs.

  3) The command "assume replace", which replaces a term with another term in a game like "replace", but does not check that the replacement is correct. This is useful to experiment. (Obviously, CryptoVerif does not consider that the protocol is proved when this command is used.)

  4) The command "insert" has been extended to insert several tests, assignments as well as event_abort in a single command. For instance, inserting find ... then/else let x = ... in one step allows to test in the condition of the inserted find whether x is defined, and thus which branch of the inserted find was taken.

  5) The game indistinguishability axioms used to model the assumptions ROM (random oracle model), PRF (pseudo-random function), PRP (pseudo-random permutation), SPRP (super pseudo-random permutation), and ICM (ideal cipher model) are now generated on-demand by CryptoVerif. That allows more flexibility to optimize these axioms.

  6) We improved the probabilities for Diffie-Hellman assumptions that use random self reducibility. In particular, we introduced a probability of distinguishing a rerandomized key from an honestly generated key, so that the transformations can also be applied to Curve25519 and Curve448.

  7) When a proof of indistinguability fails, CryptoVerif explains where the two games differ. That makes it easier for the user to know what to do next in the proof, especially when the two games are large and similar.

  8) CryptoVerif can now use the total number of calls to an oracle in the probability formulas that it computes, in addition to the number of copies of each replication. That allows CryptoVerif to provide more precise probabilities in case oracles are under several replications.

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

• URL: http://cryptoverif.inria.fr/
• Publications: 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é

7.1.2 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.
• Release Contributions: New in 2020: F* continues to evolve and is actively developed on GitHub (https://github.com/FStarLang/FStar). This year, we worked on reworking the stateful core of F* using a new formal foundation called Steel (which was published at ICFP 2020) and on improving the libraries and tooling of F* to support meta-programming, which was heavily used in the EverCrypt and HACLxN projects.
• URL: https://www.fstar-lang.org/
• Contacts: Catalin Hritcu, Karthikeyan Bhargavan
• Participants: Antoine Delignat-Lavaud, Catalin Hritcu, Cedric Fournet, Chantal Keller, Karthikeyan Bhargavan, Pierre-Yves Strub

7.1.3 miTLS

• Keywords: Cryptographic protocol, Software Verification
• Functional Description: miTLS is a verified reference implementation of the TLS protocol. Our code fully supports its wire formats, ciphersuites, sessions and connections, re-handshakes and resumptions, alerts and errors, and data fragmentation, as prescribed in the RFCs, it interoperates with mainstream web browsers and servers. At the same time, our code is carefully structured to enable its modular, automated verification, from its main API down to computational assumptions on its cryptographic algorithms.
• Release Contributions: New in 2020: In 2020, we continued work on the implementation and deployment of TLS 1.3 and the QUIC protocol, which internally uses TLS 1.3. We integrated the new EverCrypt cryptographic provider to miTLS, resulting in significant performance improvements. Finally, we deployed our code within Microsoft MsQuic (https://github.com/microsoft/msquic).
• URL: https://github.com/mitls/mitls-fstar
• Contact: Karthikeyan Bhargavan
• Participants: Alfredo Pironti, Antoine Delignat-Lavaud, Cedric Fournet, Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Pierre-Yves Strub, Santiago Zanella

7.1.4 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: Vincent Cheval and Bruno Blanchet finished their work on several extensions of ProVerif: 1) support for integer counters, with incrementation and inequality tests, 2) lemmas and axioms to give intermediate results to ProVerif, which it exploits to help proving subsequent queries, by deriving additional information in the Horn clauses that it uses to perform the proofs, 3) proofs by induction on the length of the trace, by giving as lemma the property to prove, but obviously for strictly shorter traces, 4) temporal queries, which allow to order events. The soundness of these features is proved (by hand). Moreover, they optimized many algorithms used in ProVerif (generation of clauses, resolution, subsumption ...) resulting in impressive speedups on large examples. These features are included in ProVerif 2.02pl1 and a paper by Bruno Blanchet, Vincent Cheval, and Véronique Cortier is under submission.
• URL: http://proverif.inria.fr/
• Publications: hal-01947972, hal-01423742, hal-01306440, hal-01423760, hal-01102136, hal-01575920, hal-01528752, hal-01575923, hal-01527671, hal-01575861
• Authors: Bruno Blanchet, Vincent Cheval, Marc Sylvestre
• Contact: Bruno Blanchet
• Participants: Bruno Blanchet, Marc Sylvestre, Vincent Cheval

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

• Release Contributions:

  New in 2020: In 2020, we worked on two major updates to the HACL* library

  (1) EverCrypt: We built a new cryptographic provider called EverCrypt that combines verified C code from HACL* with verified Intel assembly code from the Vale projects and integrates them under a verified agile multiplexed API that seamlessly works across multiple platforms. The resulting verified code provides best-in-class performance for popular primitives like AES-GCM and X25519. This work resulted in a paper at IEEE S&P 2020 and a new HACL* release. The resulting code was deployed in the Linux kernel, Mozilla Firefox, WireGuard VPN, and Microsoft MsQuic.

  (2) HACLxN: We developed a new methodology for writing and verifying generic SIMD crypto code that can be compiled to efficient code on multiple platforms that support vector instructions, including ARM Neon and Intel AVX, AVX2, and AVX512. We used this methodology to develop high-performance verified SIMD implementations for Chacha20-Poly1305, Blake2, and SHA-2. This work resulted in a paper at ACM CCS 2020 and a new HACL* release. The resulting code is deployed in Mozilla Firefox and Tezos Blockchain.

• URL: https://github.com/mitls/hacl-star
• Contact: Karthikeyan Bhargavan

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

• Grant from Nomadic Labs - Inria
• PIs: Catalin Hritcu and 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.

10.1.1 Inria international partners

10.1.2 Participation in other international programs

10.2.1 FP7 & H2020 Projects

10.2.2 ERC Consolidator Grant: CIRCUS

• Title: CIRCUS: An end-to-end verification architecture for building Certified Implementations of Robust, Cryptographically Secure web applications
• Duration: April 2016 - March 2021
• Coordinator: Karthikeyan Bhargavan, INRIA
• Summary:

  The security of modern web applications depends on a variety of critical components including cryptographic libraries, Transport Layer Security (TLS), browser security mechanisms, and single sign-on protocols. Although these components are widely used, their security guarantees remain poorly understood, leading to subtle bugs and frequent attacks. Rather than fixing one attack at a time, we advocate the use of formal security verification to identify and eliminate entire classes of vulnerabilities in one go.

  CIRCUS proposes to take on this challenge, by verifying the end-to-end security of web applications running in mainstream software. The key idea is to identify the core security components of web browsers and servers and replace them by rigorously verified components that offer the same functionality but with robust security guarantees.

10.2.3 ERC Starting Grant: SECOMP

• Title: SECOMP: Efficient Formally Secure Compilers to a Tagged Architecture
• Duration: Jan 2017 - December 2021
• Coordinator: Catalin Hritcu, INRIA
• Summary: The SECOMP project is aimed at leveraging emerging hardware capabilities for fine-grained protection to build the first, efficient secure compilation chains for realistic low-level programming languages (the C language, and Low* a safe subset of C embedded in F* for verification). These compilation chains will provide a secure semantics for all programs and will ensure that high-level abstractions cannot be violated even when interacting with untrusted low-level code. To achieve this level of security without sacrificing efficiency, our secure compilation chains target a tagged architecture, which associates a metadata tag to each word and efficiently propagates and checks tags according to software-defined rules. We will use property-based testing and formal verification to provide high confidence that our compilers are indeed secure.

10.3.1 ANR

11.1.1 Scientific events: organisation

11.1.2 Scientific events: selection

11.1.3 Journal

11.1.4 Scientific expertise

• Bruno Blanchet is a member of the specialized temporary scientific committee of ANSM (Agence nationale de sécurité du médicament et des produits de santé), on the cybersecurity of software medical devices.
• Bruno Blanchet was a scientific consultant for Nomadic Labs, regarding the development of the blockchain Tezos.
• Karthikeyan Bhargavan was a scientific consultant for CryptoSense, Facebook, and Apple.

11.1.5 Research administration

• Bruno Blanchet was a member of the hiring scientific jury for Inria researchers (chargé de recherche and Inria Starting Faculty Positions) of the Inria Saclay center.
• Bruno Blanchet was a member of the jury for Inria Prizes.
• Bruno Blanchet was a representative of Inria Paris at the DIM RFSI (Domaine d’Intérêt Majeur, Réseau Francilien en Sciences Informatiques).

11.2.1 Teaching

• Master: Bruno Blanchet, Cryptographic protocols: formal and computational proofs, 4.5h equivalent TD, master M2 MPRI, université Paris VII
• Master: Karthikeyan Bhargavan, Cryptographic protocols: formal and computational proofs, 18h equivalent TD, master M2 MPRI, université Paris VII
• Master: Vincent Cheval, Cryptographic protocols: formal and computational proofs, 18h equivalent TD, master M2 MPRI, université Paris VII
• PhD: Bruno Blanchet and Benjamin Lipp, CryptoVerif: Mechanizing Game-Based Proofs, VeriCrypt: An Introduction to Tools for Verified Cryptography, 10-11 December 2020
• PhD: Marina Polubelova, F*, VeriCrypt: An Introduction to Tools for Verified Cryptography, 10-11 December 2020

11.2.2 Supervision

• PhD: Benjamin Beurdouche, "Formal Verification for High Assurance Security Software in F*: Application to communication protocols and cryptographic primitives", supervised by Karthikeyan Bhargavan, defended at PSL on December 18, 2020.
• PhD in progress: Benjamin Lipp, On Mechanised Cryptographic Proofs of Protocols and their Link with Verified Implementations, ENS Paris, since October 2018, supervised by Bruno Blanchet and Karthikeyan Bhargavan.
• PhD in progress: Natalia Kulatova, Formal Analysis of Security Devices, PSL, since September 2017, supervised by Karthikeyan Bhargavan and Graham Steel.
• PhD in progress: Marina Polubelova, Formal Verification of a Cryptographic Library, PSL, since September 2017, supervised by Karthikeyan Bhargavan.
• PhD in progress: Denis Merigoux, Verification framework for performance-oriented memory-safe programming languages, since September 2018, supervised by Karthikeyan Bhargavan and Jonathan Protzenko.
• PhD in progress: Son Ho, Verification tools for low-level software, since September 2020, supervised by Karthikeyan Bhargavan and Jonathan Protzenko.
• PhDs in progress: Carmine Abate, Jérémy Thibault, Guido Martínez (CIFASIS-CONICET Rosario). All three left the team with the departure of Catalin Hritcu.

11.2.3 Juries

• Bruno Blanchet was reviewer of Alexandre Debant's PhD thesis (Université de Rennes 1).
• Bruno Blanchet was member of the PhD jury of Charlie Jacomme (ENS Paris-Saclay).
• Karthikeyan Bhargavan was a reviewer of the PhD thesis of Raphael Rieu-Helft (University of Paris-Saclay)
• Karthikeyan Bhargavan was a reviewer of the PhD thesis of Darius Mercadier (Sorbonne)
• Karthikeyan Bhargavan was a reviewer of the PhD thesis of Ilya Grischenko (University of Wien)

International journals

• 11 article KenjiK. Maillard, CatalinC. Hritcu, ExequielE. Rivas and AntoineA. Van Muylder. The Next 700 Relational Program Logics Proceedings of the ACM on Programming Languages 4 POPL 2020
  HAL back to text
• 12 article RubenR. Pieters, ExequielE. Rivas and TomT. Schrijvers. Generalized monoidal effects and handlers Journal of Functional Programming 30 2020
  HAL DOI back to text
• 13 articleNikhilN. Swamy, AseemA. Rastogi, AymericA. Fromherz, DenisD. Merigoux, DanelD. Ahman and GuidoG. Martínez. SteelCore: an extensible concurrent separation logic for effectful dependently typed programsProceedings of the ACM on Programming Languages4ICFPAugust 2020, 1-30
  HALDOIback to text

International peer-reviewed conferences

• 14 inproceedings ManuelM. Barbosa, GillesG. Barthe, KarthikK. Bhargavan, BrunoB. Blanchet, CasC. Cremers, KevinK. Liao and BryanB. Parno. SoK: Computer-Aided Cryptography SP 2021 - 42nd IEEE Symposium on Security and Privacy Virtual Conference, United States May 2021
  HAL back to text
• 15 inproceedings TomásT. Díaz, FedericoF. Olmedo and ÉricÉ. Tanter. A Mechanized Formalization of GraphQL CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs New Orleans, United States https://popl20.sigplan.org/home/CPP-2020 January 2020
  HAL DOI
• 16 inproceedingsShin-yaS.-y. Katsumata, ExequielE. Rivas and TarmoT. Uustalu. Interaction Laws of Monads and ComonadsLICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceSaarbrücken / Virtual, GermanyJuly 2020, 604-618
  HALDOIback to text
• 17 inproceedingsDenisD. Merigoux, RaphaëlR. Monat and JonathanJ. Protzenko. A Modern Compiler for the French Tax CodeCC '21: 30th ACM SIGPLAN International Conference on Compiler ConstructionCC 2021: Proceedings of the 30th ACM SIGPLAN International Conference on Compiler ConstructionVirtual, South Koreahttps://conf.researchr.org/home/CC-2021March 2021, 71-82
  HALDOIback to text
• 18 inproceedings MarinaM. Polubelova, KarthikeyanK. Bhargavan, JonathanJ. Protzenko, BenjaminB. Beurdouche, AymericA. Fromherz, NataliaN. Kulatova and SantiagoS. Zanella-Béguelin. HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms) CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security Virtual Event, United States November 2020
  HAL back to text
• 19 inproceedingsJonathanJ. Protzenko, BryanB. Parno, AymericA. Fromherz, ChrisC. Hawblitzel, MarinaM. Polubelova, KarthikeyanK. Bhargavan, BenjaminB. Beurdouche, JoonwonJ. Choi, AntoineA. Delignat-Lavaud, CedricC. Fournet, NataliaN. Kulatova, TahinaT. Ramananandro, AseemA. Rastogi, NikhilN. Swamy, ChristophC. Wintersteiger and SantiagoS. Zanella-Béguelin. EverCrypt: A Fast, Verified, Cross-Platform Cryptographic ProviderSP 2020 - IEEE Symposium on Security and PrivacySan Francisco / Virtual, United StatesMay 2020, 983-1002
  HALDOIback to text

National peer-reviewed Conferences

• 20 inproceedings LianeL. Huttner and DenisD. Merigoux. Traduire la loi en code grâce au langage de programmation Catala Intelligence artificielle et finances publiques Nice, France October 2020
  HAL back to text
• 21 inproceedings DenisD. Merigoux, RaphaëlR. Monat and ChristopheC. Gaie. Étude formelle de l'implémentation du code des impôts JFLA 2020 - 31ème Journées Francophones des Langages Applicatifs Gruissan, France http://jfla.inria.fr/jfla2020.html January 2020
  HAL back to text

Conferences without proceedings

• 22 inproceedings DavidD. Baelde, StéphanieS. Delaune, CharlieC. Jacomme, AdrienA. Koutsos and SolèneS. Moreau. An Interactive Prover for Protocol Verification in the Computational Model SP 2021 - 42nd IEEE Symposium on Security and Privacy San Fransisco / Virtual, United States May 2021
  HAL

Reports & preprints

• 23 report JoëlJ. Alwen, BrunoB. Blanchet, EduardE. Hauck, EikeE. Kiltz, BenjaminB. Lipp and DoreenD. Riepel. Analysing the HPKE Standard IACR Cryptology ePrint Archive November 2020
  HAL back to text
• 24 misc BenjaminB. Beurdouche. MLS Architecture: analysis of the security, privacy and functional requirements January 2020
  HAL
• 25 report RobertoR. Blanco, MatteoM. Manighetti and DaleD. Miller. FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs Inria Saclay July 2020
  HAL
• 26 report BenjaminB. Lipp. An Analysis of Hybrid Public Key Encryption IACR Cryptology ePrint Archive February 2020
  HAL back to text
• 27 misc DenisD. Merigoux, NicolasN. Chataing and JonathanJ. Protzenko. Catala: A Programming Language for the Law March 2021
  HAL
• 28 misc DenisD. Merigoux and LianeL. Huttner. Catala: Moving Towards the Future of Legal Expert Systems September 2020
  HAL back to text