Kyber is a key-encapsulation mechanism (KEM), whose security is based on the hardness the Module-LWE problem. It is the only KEM that has been selected by the NIST Post-Quantum Cryptography project, and will be part of NIST’s first post-quantum cryptography standard. Hakyber, a formally verified implementation of Kyber, has been developed. Hakyber is written in Jasmin, and formally verified in EasyCrypt.

EasyCrypt has already been used to prove the correction of implementations of cryptographic primitives, such as of ChaCha20-Poly1305. This proof is done by “game hopping”: the correction of a naive implementation of the primitive is proven using EasyCrypt’s probabilistic Hoare logic (pHL), and it is shown to be equivalent to gradually more optimized implementations using EasyCrypt’s probabilistic relational Hoare logic (pRHL).

Hakyber differs from the cryptographic primitives formalized in EasyCrypt by the complexity of the mathematical structures involved in it’s correctness an security proofs. In particular, it’s correction proof involves polynomials over finite fields, quotient rings and Number Theoretic Transforms (NTTs), variants of the Fourier transform used in fast polynomial multiplication algorithms.

The correction proof of Hakyber’s NTT is one of the trickiest parts of the total correction proof. We will discuss the issues we encountered in this proof, the solutions we used to overcome them, and current and planned developments of EasyCrypt that were motivated by these issues.

In particular, we will talk about the theories developed to deal with equivalence proofs of nested for loops, as well as those describing algebraic hierarchies using EasyCrypt’s clone mechanism. We will then present the planned replacement for these theories, using EasyCrypt’s annotations and type class mechanism respectively.

I will present work in progress on a research programs aiming to compile efficiently automata-model of computation using vectorial instructions and bit-level paralellism.

The compilation procedure relies on algebraic automata theory that will be gently introduced. Some complexity related consideration will also provides insight on what to expect and what is (probably) hopeless to compile efficiently.

It is usually considered that the security of network protocols is a difficult problem that should be reserved to specialists (“don't design your own crypto”). Yet, in 2018, together with Clara Dô and Weronika Kołodziejak, we set out to design a simple and provably correct security mechanism for the Babel routing protocol.

Much to our surprise, our work passed successfully the IETF's security review, and was subsequently published as RFC 8967. In the Spring of 2022, however, it was discovered that even though our protocol had been proved correct, it was failing in a small number of “real” networks, which turned out to violate one of the assumptions made in our proof.

In this talk, I will first describe the properties that are expected from a security mechanism. I will then show the proof of correctness of the security mechanism described in RFC 8967, and show the assumptions that it makes about the network. Finally, I will describe how these assumptions turned out to be incorrect, and how we managed to fix the protocol in a backwards compatible manner.

Many computer systems are reactive: they execute in continuous interaction with their environment. From the perspective of functional programming, reactive systems can be modeled and programmed as stream functions. Several lines of research have exploited this point of view. Works based on Nakano’s guarded recursion use type-theoretical modalities to guarantee productivity. Works based on synchronous programming use more specialized methods but guarantee incremental processing of stream fragments. In this paper, we contribute to a recent synthesis between the two approaches by describing how a language with a family of type-theoretical modalities can be given an incremental semantics in the synchronous style. We prove that this semantics coincides with a more usual big-step semantics.

The energy of a system of atoms is approximately a function of the position of the nuclei. This function is called the potential energy surface (PES). Knowledge of the PES is fundamental in ab-initio sciences but unfortunately, it cannot be computed in closed form. As a result, an important problem is that of exploring the PES to discover important features, such as local minima.

In this talk, I will introduce an experimental probabilistic programming language designed to facilitate the exploration of PES. In this language, the semantics of a program is a probability distribution over PES. The objective of the compiler is to generate an optimizer that combines solvers from machine learning and quantum chemistry to discover local minima of the PES. While much of this language and compiler is routine, we will see that the principle of conservation of energy brings about genuinely interesting compilation problems.

We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, we achieve state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads. See https://arxiv.org/pdf/2202.01344.pdf

Parmi les techniques de détection automatisée de tests, le fuzzing gagne chaque année en popularité.

Cette technique permet d'explorer rapidement la surface d'un programme grâce à la génération automatique rapide de cas de tests, parfois guidée par exemple par des mesures de couverture.

En revanche, dès que le programme contient des conditions spécifiques (par exemple, x = 0x42, où x a été lu depuis l'entrée utilisateur), la probabilité qu'un fuzzeur génère une solution est assez faible.

On propose d'améliorer les perfomances du fuzzeur AFL en le combinant avec une analyse symbolique, qui analysera les traces des cas de tests générés, pour identifier ces conditions (par exemple, on aurait input[0] = 0x0042). On en déduit des prédicats de chemins sous-approximés, qu'on appelle “facilement énumérable”, et dont les solutions sont directement générées par notre fuzzeur modifié.

L'outil ainsi créé, ConFuzz, est intégré à la plateforme d'analyse de code binaire Binsec, développée au CEA List, et a été testé sur LAVA-M, un banc de test standard en fuzzing.

In practice, the popular proof assistants based on type theory (Coq, Agda, Lean) all require users to navigate around performance issues and bottlenecks in sufficiently large or complex codebases. I hypothesize some common performance issues and try to address them in a minimal implementation, called “smalltt”. One goal is to have a concrete data point for what kind of performance is achievable in the presence of the basic convenience features of pattern unification and implicit arguments. Another goal is to develop general solutions which plausibly scale to production-strength systems without losing too much performance, and also allow fine-tuning based on more realistic codebases.

Nested datatypes have been widely studied in the past 25 years, both theoretically using category theory, and practically in programming languages such as Haskell. They consist of recursive polymorphic datatypes where the type parameter changes throughout the recursion. They have a variety of applications such as modelling memory or constraints over regular datatypes.

Our work focuses on a specific subset of nested datatypes which we call Linked Nested DataTypes (LNDT), and which induces the definition of some regular datatypes, such as List and Maybe, as well as some nested datatypes, such as Nest and Bush. LibNDT is a core library, developed both in Coq and Agda, which focuses on the set of constructs that can be spread directly from the parameter on which a specific LNDT is built to the LNDT itself (For instance, List is built with the identity parameter). These spreadable elements are of two kinds, functions, such as folds and map, and properties such as the congruence of map or Any and All (existential and universal satisfaction of a predicate inside a LNDT).

In this presentation, we explain the thought process behind the creation of this specific subset of nested datatypes, and we present different concrete LNDTs, as well as our set of spreadable elements over them. We conclude by an open discussion about various thoughts related to our work.

Despite significant progress in the formal verification of security-critical components like cryptographic libraries and protocols, the secure integration of these components into larger unverified applications remains an open challenge. The first problem is that any memory safety bug or side-channel leak in the unverified code can nullify the security guarantees of the verified code. A second issue is that application developers may misunderstand the specification and assumptions of the verified code and so use it incorrectly. In this presentation, we propose a novel verification framework that seeks to close these gaps for applications written in Rust. At the heart of this framework is hacspec, a new language for writing succinct, executable, formal specifications for cryptographic components. Syntactically, hacspec is a purely functional subset of Rust that aims to be readable by developers, cryptographers, and verification experts. An application developer can use hacspec to specify and prototype cryptographic components in Rust, and then replace this specification with a verified implementation before deployment. We present the hacspec language, its formal semantics and type system, and describe a translation from hacspec to F*. We evaluate the language and its toolchain on a library of popular cryptographic algorithms.

Dans le langage OCaml, les constructeurs de types algébriques sont représentés par des pointeurs vers des blocs mémoire. Cette représentation uniforme a de nombreux avantage, mais les utilisateurs aimeraient parfois des représentations plus compactes.

Dans ce travail, en collaboration avec Nicolas Chataing et Stephen Dolan, nous étudions la possibilité de “déboîter” certains constructeurs – si l'utilisateur le demande au moment de leur définition – c'est-à-dire de ne pas les représenter en mémoire du tout. Dans certains cas, effacer les constructeurs introduirait des confusions entre valeurs différentes, et il faut donc rejeter la demande. Nous avons donc conçu une analyse statique pour détecter ces confusions; la question de la terminaison de cette analyse est intéressante.