Journée scientifique Inria - Nomadic Labs - lundi 21 septembre
Les exposés sont de trois types:
9h00 - ACCUEIL -
9h15 + 10’
9h25 + 1h10
10h35 + 20’ - PAUSE -
10h55 + 1h15
12h10 + 1h40 - REPAS -
13h40 + 1h50
15h15 + 30’ - PAUSE -
15h45 + 55’
16h40 + 10’ - PAUSE -
16h50 + 25’
17h15 + 15’
17h30 - FIN DE LA JOURNÉE -
Présentation générale de Tezos / utilisation de l’écosystème OCaml à Nomadic (Pierre Boutillier) Slides
Efforts de recherche en cryptographie à Nomadic (Marc Beunardeau) Slides
Vérification de smart contracts et de la base de code de Tezos (Raphaël Cauderlier et Zaynah Dargaye) Slides, part 1 Slides, part 2
OCaml Multicore: Cosmo: a concurrent separation logic for Multicore OCaml (Glen Mével) Slides
Separation logic has proven an effective way of reasoning about functional correctness of imperative programs. In the last decade, tools such as CFML brought its expressiveness to interactive program verification for a meaningful fragment of the OCaml language. With the advent of Multicore OCaml, there is now a call for reasoning principles for shared-memory concurrency. The weak memory setting poses specific challenges for program verification and is an active research topic. Using the Iris separation logic framework, I will derive program logic for Multicore OCaml, mechanized in Coq, and demonstrate its usage on simple examples.
OCaml Maintenance: Nurturing Ocaml day by day (Florian Angeletti) Slides
We present the ongoing work to make the OCaml release process more transparent, predictable and integrated within the ecosystem. Echoing this outward-facing effort, we also present the on-going refactoring of the type checker and its error messages, in order to better convey intents to users. Diving deeper, we conclude with the internal refactoring of the pattern matching compiler.
OCaml Evolution: Rebuilding the OCaml type system: high and low road (Gabriel Radanne, Gabriel Scherer) Slides, part 1 Slides, part 2
To introduce further ideas in the OCaml language and type system, we need to make the type-system implementation as clear and simple as possible – there is room for progress! We are following two parallel, complementary routes to this goal: the “high road”, rethinking the type system to make it more general, with clearer constraint-solving approaches in mind, and the “low road”, refactoring the current implementation to make it more maintenable, better documented, clarify its core concepts and onboard new contributors.
Fstar : Dijkstra monads and relational reasoning (Exequiel Rivas) Slides
F* is a higher-order programming language with support for ML-like effects. It was designed with program verification in mind, and used successfully for writing the verified cryptographic library HACL*. In this talk, we will see some new developments in F* which allow new effects such as non-determinism and IO to be covered in a principled way. We’ll also briefly discuss how this new approach can be extended to handle relational properties such as non-interference.
Coqdev : Génie logiciel pour l’évolution de Coq (Théo Zimmermann) Slides
Cet exposé donnera un bref aperçu des tâches en cours ou à venir ayant pour but notamment d’améliorer l’accessibilité de Coq (documentation, distribution de paquets via la création d’une “plateforme”), d’animer une communauté de contributeurs (à l’écosystème avec l’organisation coq-community, ainsi qu’au logiciel lui-même via le dépôt GitHub de Coq) et plus généralement de permettre une évolution nécessaire pour prendre en compte les besoins des utilisateurs, tout en prenant garde à la stabilité, critique pour les projets existants.
SMTCoq : Automatisation sûre et efficace pour Coq, en application à la certification de blockchains (Chantal Keller and Valentin Blot) Slides
The subject of this project is to significantly enhance automation in the Coq proof assistant, with an application to simplifying the certification of the Tezos blockchain and the development of safe libraries of smart contracts. This project is based on SMTCoq, a Coq plugin that offers a way to use automatic provers with the same degree of trust as Coq itself. We report on work in progress to extend SMTCoq with expressive, automatic tactics, by providing a framework to progressively encode Coq’s logic into first-order logic.
Votexp : Étude des évolutions possibles du système de vote de Tezos (Stéphane Glondu) Slides
Le microcosme Tezos où les élections prennent place est particulièrement atypique pour le monde du vote électronique (délégation, enjeu financier…). Cette étude a pour but de déterminer quelles propriétés, classiques ou non, sont souhaitées.
Jasmin: Jasmin-EasyCrypt, past & future (Pierre-Yves Strub) Slides
In this talk, I’ll briefly describe the Jasmin/EasyCrypt framework, describe what can be and has been achieved, and present our future plans (in terms of extension to the framework as well as future use cases that we are targeting).
Disco : Bridging synchrony and asynchrony (Stephan Merz) Slides
The asynchronous computational model is known for its performance benefits while the synchronous one for facilitating correctness proofs. In this talk we will discuss how to connect these worlds, with the goal of transferring proof arguments used in synchronous protocols to executions of asynchronous protocols.
CoqExtra : (A Formally Verified Extraction Mechanism using Precise Type Specifications)
(Nicolas Tabareau) Slides
The extraction mechanism from Coq to OCaml is very useful to be able to run and link critical pieces of code that have been certified with the rest of a software system. For instance, for Tezos, it is important to certify the Michelson language for smart contracts and then to be able to extract it to OCaml so that it interacts with the rest of the code that has been developed. Unfortunately, the current extraction mechanism of Coq suffers from two major flaws that prevent extraction from being used in complex situations—and in particular for the Michelson language. In this talk, I will present those two flaws and give some ideas on how to solve them.
SmartSpec : From Smart Contracts to Services: End-to-End Specs (Georges Gonthier) Slides
The main advantage of implementing services using smart contracts is that these ensure materially faithful execution - inasmuch as the contracts do execute as expected. Ensuring this means proving functional correctness, rather mere execution safety. We’ll present a toolset that addresses some of the many challenges such proofs present, such as modelling concurrent and probabilistic execution, belief and information flow, and economic incentives.
Cavoc : Compositional Automated Verification for OCaml (Guilhem Jaber) Slides
In this talk, I will introduce the project of designing a static analysis tool for OCaml code, that takes into account the abstraction properties enforced by the type system (parametric polymorphism, GADT). Analyzing an OCaml module, the tool would check if there exists some OCaml code that could trigger escaping exceptions in the module. Such uncaught exceptions include unsatisfied assertions in the code, allowing the programmer to check in a compositional way if given invariants holds for any possible execution of the code.
OCaml Rust : Improving the OCaml/Rust interface (Gabriel Scherer) Slides
When trying to write hybrid programs in two safe languages, OCaml and Rust, is there a better way than going through C as intermediate glue? In particular, can we hope to provide better safety guarantees than the low-level, unchecked FFI (Foreign Function Interface) that is used by OCaml/C and Rust/C programs?