This page gathers all information about this past event (last update: 03/06/2022)
The programme is composed of presentations of ongoing collaborative projects funded by Nomadic Labs, as well as a few technical presentations by Nomadic Labs.
It is coomposed of short talks (15mn = 12mn + questions) and long talks (25mn = 20mn + questions).
8h45 : Accueil
| S1 | 1h20 | Slides | Talk, Speaker |
|---|---|---|---|
| 9h00 : | Introduction | ||
| 9h10 : | L | X | Scaling up, NL, Yann-Régis Gianas |
| 9h35 : | S | X | OCamlMaintenance, Cambium, Florian Angeletti |
| 9h50 : | S | X | OCamlEvolution, Cambium, François Pottier & Gabriel Scherer |
| 10h05 : | S | X | OCamlMulticore, Cambium, Glen Mével |
10h20 : Coffee break (25mn)
| S2 | 1h20 | Slides | Talk, Speaker |
|---|---|---|---|
| 10h45 : | L | X | Zero-Knowledge proofs, NL, Marc Beurnardeau |
| 11h10 : | S | X | ZCashVerif, Pesto & Prosecco, Vincent Cheval |
| 11h25 : | S | Y | Effizk, Grace, Danny Willems |
| 11h40 : | L | X | Jasmin, Grace & Stamp, Benjamin Grégoire |
12h10 : Lunch break (2h00)
| S3 | 1h45 | Slides | Talk, Speaker |
|---|---|---|---|
| 14h10 : | S | X | NFT. Nomadic Labs, Daniel Jean |
| 14h25 : | L | W | CoqExtra, Gallinette, Nicolas Tabareau |
| 14h50 : | L | X | Cavoc, Gallinette, Guilhem Jaber |
| 15h15 : | S | X | Salto, Celtique, Benoît Montagu |
| 15h30 : | L | X | CoqDev, Picube, Théo Zimmermann |
15h55 : Tea time (25mn)
| S4 | 1h45 | Slides | Talk, Speaker |
|---|---|---|---|
| 16h20 : | L | X | OCamlRust, Gallinette, Guillaume Munch-Maccagnoni |
| 16h45 : | L | X | SMTCoq, Deducteam, Chantal Keller |
| 17h10 : | S | X | Fstar, Prosecco, Aymeric Fromherz |
| 17h25 : | S | X | SmartSpec, SIF, Georges Gonthier |
| 17h40 : | L | X | Data availability, Nomadic Labs, François Thiré |
| 17h55 : | Cloture |
18h00 : fin
Zero knowledge proof systems are often based on operations over (prime) finite fields, and are written in a specific language; but most standard cryptographic primitives are encoded as boolean circuits and use bitwise operations. This project aims to develop cryptographic primitives that can be implemented efficiently and securely in zero-knowledge languages, while remaining efficient on conventional processor architectures.
We report on a static analyzer for a higher-order functional language, that infers over-approximations of the values that any subterm may produce. The analysis is based on a recently published version of control-flow analysis (∇CFA). This is a first step towards the static analysis of OCaml programs, that would warn about unhandled exceptions, prove that some assertions cannot be violated, and warn about arithmetic overflows. This project is conducted in collaboration with Thomas Genet and Thomas Jensen.
scope is a new Coq tactic that transforms a subset of Coq goals expressed in the Calculus of Inductive Construction into First-Order Logic. It is based on the combination of small, modular and pairwise-independent certifying transformations. It currently handles polymorphism, function and fixpoint definitions, pattern matching, algebraic datatypes; inductive predicates are under progress. Combined with SMTCoq, which calls external SMT solvers, and trakt, a new tactic developed by Enzo Crance, Assia Mahboubi and Denis Cousineau to reflect bijective types, it provides an efficient automatic tactic called snipe.
We will present an erasure procedure–certified in MetaCoq–to untyped lambda-calculus accomplishing the same as the Extraction plugin of Coq. The extracted safe erasure is available in Coq through a new vernacular command:
MetaCoq Erase <term>. We will also explain the next step to improve Coq Extraction plugin based on this work.
The Jasmin language has been designed to develop low level implementations that need to be secure and efficient. I will give and overview of the latest feature introduced in the language and present a type system allowing to ensure protection against Spectre attacks based on selective speculative load hardening.
Steel is a recent framework based on Concurrent Separation Logic that extends F* with concurrency. As a framework, Steel combines a rich, expressive program logic to reason about fine-grained concurrency with a high-level of automation through a cooperation between SMT solving and F* tactics. In this talk, we report on the latest improvements to Steel and present ongoing efforts on applying Steel to the verification of a concurrent memory allocator with modern security defenses.
Since January 2020, Nomadic Labs has sponsored the evolution of the Coq ecosystem and the organization of its community by funding Théo Zimmermann’s activity. In this talk, he will present the ongoing and accomplished work since the last Nomadic Labs-Inria day in September 2020. He will present efforts toward making the Coq ecosystem more accessible (notably work on the Coq Platform, but also on documentation and discussion channels), efforts of community organization and development (including the Coq Community Survey 2022, and the management of the Coq-community organization), and efforts toward making the evolution of Coq and its ecosystem more robust (including evolution of the bot assisting the development team, and innovation in cross-project collaboration through smart continuous integration).
Since 2019, Nomadic Labs has sponsored the evolution of the OCaml language and system. In this talk, we will zoom in on two ongoing research projects. Olivier Martinot (advised by Gabriel Scherer) is scaling up Inferno, a library for constraint-based type inference and elaboration, so as to eventually make it possible to implement type inference for OCaml based on Inferno. Paulo de Vilhena (advised by François Pottier) has developed Hazel, a program logic that allows reasoning about effect handlers, and is now using Hazel as a basis to prove the soundness of a static type system that keeps track of effects and guarantees that every effect is handled.
Since 2019, Nomadic Labs has sponsored the maintenance and evolution of the OCaml compiler by funding Florian Angeletti’s activity. In this talk, we present our recent progress towards making the OCaml release process more regular and better integrated with the ecosystem. Inside the compiler, we have refactored the type-checker and prepared the advent of OCaml 5, which introduces support for shared-memory concurrency and support for delimited control effects, also known as effect handlers. Closer to the surface, there have been improvements in error messages and in the integration with Merlin. Regarding the workflow of the compiler developers, we are now able to use the compiler’s benchmarks to inform design choices in the compiler’s development.
We often want to write programs with components in several different programming languages. Interfacing two languages typically goes through low-level, unsafe interfaces. The OCamlRust project has studied safer interfaces between OCaml and Rust.
We investigated safe low-level representations of OCaml values on the Rust side, representing GC ownership, and developed a calling convention that reconciles the OCaml FFI idioms with Rust idioms. A key new software component is Boxroot, an efficient and flexible mechanism to register values with the OCaml GC, for use when interfacing with Rust (and other programming languages). This resulted in novel techniques which can benefit other pairs of languages in the future. Some of these works are now integrated in the ocaml-rs interface between OCaml and Rust.
Since 2019, Nomadic Labs has funded Glen Mével’s research on Concurrent Separation Logic (CSL). The main focus of Glen’s work has been on Cosmo, a CSL with specific support for the weak memory model of OCaml 5. In this talk, however, Glen will present recent results on a different aspect, namely the use of CSL to reason about the amortized time complexity of persistent data structures that involve thunks. Okasaki’s “banker’s queue” is one such data structure: it uses a lazy list. Glen will show how Okasaki’s complexity analysis, which relies on subtle notions of “debits” and “anticipation”, can be reconstructed (and mechanically verified) inside CSL.
This work provides a formal security analysis of the sapling version of the ZCash standard using the state-of-the-art protocol verification tool ProVerif. ZCash is a specification and an implementation of a decentralized anonymous payment scheme based on, and improving the ZeroCash protocol.
We provide a detailed formal model of ZCash that follows closely the ZCash protocol specification document for the Sapling version. A particular effort has been put into the modelling of cryptographic primitives. We propose a model for complex zero-knowledge proofs, different kind of signatures (relying on an existing model for signatures that includes potential weaknesses) and a novel model of hash functions. The specification of security properties is inspired by the ones given in the original ZeroCash paper, relying on oracles that the attacker can invoke to create new addresses, mint new notes, trigger transactions from honest participants as well as insert his own transactions. Our analysis focuses on two essential properties: the balance property and non-malleability of transactions. We discuss our modeling choices regarding those properties that turned out to be non-trivial to model.
NFTs have grown considerably in the last two years. But what are they concretely? Let’s see how this technology enables new funding levers for sustainable projects and rewards donors for their commitments.
A blockchain is a decentralized and secure computational device. As such, this software system must implement the standard fetch-execute cycle under three specific constraints. First, the next instruction must come from a consensus between the participants of the blockchain. Second, the execution of the instruction, that is, its action on the state of the blockchain must be undisputable. Third, the blockchain must be robust to adversarial participants.
The Tezos blockchain satisfies the first constraint through a (low energy) consensus algorithm based on the idea of liquid proof of stake: every token holder owns a fractional right to produce a block of operations and by delegating this right to specific participants named bakers, participants allow for a robust and efficient consensus algorithm dependent on the distribution of stakes. With the recent Tenderbake, the Tezos blockchain produces in practice a block every 30 seconds with a finality period – the time required to make sure that the block is indeed a consensus – of one minute.
The Tezos blockchain is a real-time system: the frequency of block production imposes a limit on the number of operations a block can contain. This limit depends on how fast one can satisfy the second constraint – the indisputability of operation interpretation. In Tezos, as in most blockchains, the “execute” phase is implemented by every participant of the system: everyone computes a cryptographic hash characterizing the state of the chain by applying the operations to its previous state and compares this hash to the one embedded in the block to accept this block as valid. This verification process is computationally expensive and limits the number of operations per block to several hundred.
In this talk, we present the next evolution of the Tezos blockchain: the optimistic rollups. This technique is based on off-chain executions that are optimistically trusted but refutable. Thanks to optimistic rollups, we can increase the number of operations per block to several thousand.
In this talk we will see how zero-knwoledge proofs can be used to scale the blockchain. We will recap the main properties of efficient verifier zero-knowledge proofs (SNARKs) and see how to use them to build a zk-rollup. We will also see privacy related applications of zk-rollups.
Scalability is the main priority for Tezos in 2022. Tezos’ scalability is based on rollups, a means of discharging the main chain from the execution of the operations and maintenance of the corresponding state. Rollups are already a nice improvement for scalability. However, all operations, including rollups’ ones, still go through the Tezos P2P network, making network bandwidth the limiting factor for scaling.
In this talk, we propose to overcome this limitation by ensuring that not all transactions have to pass through the P2P network. This raises several challenges, including: - How can we ensure the operations are available if they were never posted on chain? - How to modify the P2P network so that the operations are not broadcast to everyone?
We will propose a plan tailored for Tezos that is inspired by other blockchains such as Ethereum, NEAR or Polkadot.