Inria project-team $\pi r^2$ (Inria)

Thematic team Analysis and conception of systems

## Analysis and conception of systems

#### Day, hour and place

Thursday at 2pm, room 1007

The calendar of events (iCal format).

In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link.

#### Contact(s)

### Next talks

Analysis and conception of systems

Thursday February 2, 2023, 2PM, salle séminaires au plateau SCAI +(Esclangon, 1er étage, campus Jussieu)

**Marine Minier** (Université de Lorraine) *Comment les outils automatiques peuvent nous aider, nous cryptographes*

Séminaire Codes Sources

Analysis and conception of systems

Thursday February 9, 2023, 2PM, salle séminaires au plateau SCAI (Esclangon, 1er étage, campus Jussieu)

**Catarina Urban** (Inria) *Interpretability-Aware Verification of Machine Learning Software*

Séminaire IRILL / GdT Programmation @ LIP6

### Previous talks

#### Year 2023

Analysis and conception of systems

Wednesday January 11, 2023, 2PM, Salle 1007

**Laurent Prosperi** (Inria) *Programming distributed systems with Varda*

Varda provides a higher level of abstraction. An Varda program describes how to compose components into a safe architecture. The programmer isolates an off-the-shelf (OTS) component behind an Varda shield, which specifies its interface, its protocol, and its pre- and post-conditions.

Components can be logically nested, providing encapsulation boundaries; the outer component orchestrates its inner components. It can intercept communication, as a general mechanism to compute over components and messages. Varda provides strong guarantees, enforcing the specification by static analysis, by run-time checks, and by sandboxing. To be useful, Varda takes a pragmatic approach. An OTS adaptor can contain non-Varda code (e.g., Java). Varda provides control over properties such as elasticity, placement, and inlining. Varda supports non-stop execution thanks to supervision mechanisms.

#### Year 2022

Analysis and conception of systems

Wednesday December 7, 2022, 2PM, Salle 1007

**Antoine Séré** (École Polytechnique) *Developments around the correction proof of Hakyber*

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.

Analysis and conception of systems

Wednesday November 23, 2022, 2PM, Salle 1007

**Charles Paperman** (Inria Links) *Vectorial execution of automata*

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.

Analysis and conception of systems

Wednesday November 2, 2022, 2PM, Salle 1007

**François Pottier** (Inria Paris) *“You Only Linearize Once”, with elegance*

Analysis and conception of systems

Tuesday October 18, 2022, 10:45AM, Salle 1007

**Juliusz Chroboczek** (IRIF) *Babel-MAC, reloaded*

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.

Analysis and conception of systems

Friday July 8, 2022, 10:30AM, Salle 1007

**Ada Vienot** (IRIF) *A reactive operational semantics for a lambda-calculus with time warps*

Analysis and conception of systems

Friday July 1, 2022, 10:30AM, Salle 3052

**Jean-Baptiste Tristan** (Boston College) *Probabilistic Programming and Molecular Optimization (Zoom link)*

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.

Analysis and conception of systems

Friday June 24, 2022, 10:30AM, Salle 3052

**Stanislas Polu** (Open AI) *Formal Mathematics Statement Curriculum Learning (Zoom link)*

Analysis and conception of systems

Wednesday June 15, 2022, 2PM, Salle 1007

**Ghiles Ziat** (IRIF) *Reading group: “Principles of Abstract Interpretation”, P. Cousot (II)*

Analysis and conception of systems

Friday June 3, 2022, 10:30AM, Salle 1007

**Yaëlle Vinçont** *Fuzzing et méthodes symboliques pour la détection de vulnérabilités à large échelle*

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.

Analysis and conception of systems

Friday April 29, 2022, 10:30AM, Salle 1007

**Ghiles Ziat** (IRIF) *Reading group: “Principles of Abstract Interpretation”, P. Cousot*

Analysis and conception of systems

Friday April 15, 2022, 10:30AM, Salle 3052

**András Kovács** (Eötvös Loránd University) *A first-principles investigation of performance of elaboration with dependent types*

Analysis and conception of systems

Friday April 1, 2022, 10:30AM, Salle 3052

**Mathieu Montin, Amélie Ledein, Catherine Dubois** (Loria - Inria Deducteam - ENSIIE, Samovar) *LibNDT: Towards a formal library on spreadable properties over linked nested 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.

(Amélie Ledein will be giving the talk)

Analysis and conception of systems

Thursday March 24, 2022, 2PM, salle 15-16 101 (campus Jussieu)

**Loïc Sylvestre** (APR/LIP6, Sorbonne Université) *Macle : un langage dédié à l'accélération de programmes OCaml sur circuits FPGA*

Séminaire IRILL / GdT Programmation @ LIP6

Analysis and conception of systems

Thursday March 17, 2022, 2PM, salle 15-16 101 (campus Jussieu)

**Bastien Guerry** (pôle logiciels libres, ETALAB, DINUM) *Présentation du pôle logiciels libres de la DINUM et du plan d'action logiciels libres et communs numériques*

Séminaire IRILL / GdT Programmation @ LIP6

Analysis and conception of systems

Friday February 11, 2022, 10:30AM, Salle 0011

**Denis Merigoux** (Inria Paris) *Hacspec: succinct, executable, verifiable specifications for high-assurance cryptography embedded in Rust*

Also virtually: https://webconf.math.cnrs.fr/b/dag-zdc-4mc

Analysis and conception of systems

Thursday February 10, 2022, 2PM, salle 15-16 101 (campus Jussieu)

**Gabriel Scherer** (Partout, Inria Saclay) *Déboîter les constructeurs*

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.

Séminaire IRILL / GdT Programmation @ LIP6

#### Year 2021

Analysis and conception of systems

Friday December 17, 2021, 10:30AM, Salle 1007

**Aliaume Lopez** (LSV) *Basic operational preorders for algebraic effects*

Analysis and conception of systems

Friday December 10, 2021, 10:30AM, Salle 1007

**Pierre-Evariste Dagand** (IRIF) *[CANCELED] Commentary on “Formal Metatheory of Second-Order Abstract Syntax”*

I propose (rather: Adrien has volunteered me) to show up with an Agda buffer and offer a live tour and commentary of the code.

Canceled: instead a PPS seminar will take place online, featuring Jérémy Ledent (University of Strathclyde) on Simplicial Models for Multi-Agent Epistemic Logic (https://www.irif.fr/seminaires/pps/index)

Analysis and conception of systems

Thursday December 2, 2021, 2PM, salle 15-16 101 (campus Jussieu)

**Raphael Monat** (APR/LIP6/Sorbonne Université) *A Modern Compiler for the French Tax Code*

Séminaire IRILL / GdT Programmation @ LIP6

Analysis and conception of systems

Friday November 26, 2021, 10:30AM, Salle 1007

**Giuseppe Castagna** (IRIF) *Type-cases, union elimination, and occurrence typing*

To apply this system in practice, we define a canonical form for the expressions of our extension, called MSC-form. We show that an expression of the extension is typable if and only if its MSC-form is, and reduce the problem of typing the latter to the one of reconstructing annotations for that term. We provide a sound algorithm that performs this reconstruction and a proof-of-concept implementation.

Analysis and conception of systems

Thursday November 18, 2021, 2PM, salle 15-16 101 (Jussieu)

**Xavier Thompson** (Nexedi) *Un système d'objets sans le GIL dans Cython*

Cython permet de joindre Python et C/C++ au sein d'un même langage. L'intérêt majeur de Cython est qu'il rend facile l'utilisation de code C/C++ comme back-end de code Python. On peut ainsi contourner le GIL de Python (le verrou global qui ne permet qu'à un seul thread à la fois d'exécuter du bytecode Python dans l'interpréteur CPython).

Avec Cython+, nous étendons les possibles de Cython sur trois aspects: 1. Tout d'abord, nous introduisons un système d'objets utilisables sans le GIL en exécution multi-thread sur plusieurs coeurs. La gestion de la mémoire est automatique comme en Python grâce à un comptage de références atomique. De plus une couche de compatibilité transparente en fait de vrais objets Python manipulables en tant que tels directement depuis l'interpréteur Python. 2. De plus, nous ajoutons à cela un modèle d'exécution asynchrone à base d'acteurs et une implémentation d'un scheduler inspiré par celui de Go. 3. Enfin, nous sommes en train d'explorer un système de types pour la thread safety inspiré par ceux de Pony et Rust.

Séminaire IRILL / GdT Programmation @ LIP6

Analysis and conception of systems

Friday November 12, 2021, 10:30AM, Salle 1007

**Ada Vienot** (IRIF) *[CANCELED] Synchronous semantics and functional reactive programming: a tentative unification*

Several lines of research have enriched this approach with strong type systems: works based on Nakano's guarded recursion use type-theoretical modalities to guarantee productivity. While this approach has its benefits, many of such domain specific functional languages fail to have a runtime suitable for resource-scarce environments. Such environments usually use the synchronous programming paradigm, which uses more specialized methods, but gives strong guarantees on the efficiency of the program.

In this presentation, we aim to present a recent synthesis between the two approaches by describing how a FRP language can be given a semantics in the synchronous style. We will then investigate the potentially deeper connections between synchronous programming and FRP.

Séance repoussée à une date ultérieure. Je [Pierre-Évariste] serai en 1007 pour accueillir et divertir les naufragés du GT.

Analysis and conception of systems

Monday November 8, 2021, 2PM, Salle 1007

**Emilio Jesus Gallego Arias** (IRIF) *Reading Group: AI meets Theorem Proving (1/?)*

Analysis and conception of systems

Friday October 22, 2021, 10:30AM, Salle 1007

**Théo Zimmermann** (IRIF) *PR of the Month: Architecture of a GitHub bot, the trigger-action model*

#### Year 2020

Analysis and conception of systems

Tuesday January 7, 2020, 11AM, Salle 3052

**Robin Piedeleu** (University College London) *Une approche graphique des systèmes concurrents*

Il s'agit de travaux en collaboration avec Filippo Bonchi, Pawel Sobocinski et Fabio Zanasi.

Conjoint avec le GdT sémantique

#### Year 2019

Analysis and conception of systems

Monday January 7, 2019, 10:30AM, Salle 3052

**Louis Mandel** (IBM Watson) *Reactive Probabilistic Programming*

Following this approach, we propose to extends a reactive programming language with probabilistic constructs. This new language enables the modeling of probabilistic reactive systems, that is, probabilistic models in constant interaction with their environment. Examples of such systems include time-series prediction, agent-based systems, or infrastructure self-tuning.

To demonstrate this approach, we started from ReactiveML, a reactive extension of OCaml that supports parallel composition of processes, communication through signals, preemption, and suspension. We extend the language with classic probabilistic constructs (sample, factor à la WebPPL) and propose an inference scheme for reactive processes, that are, non-terminating functions.

#### Year 2018

Analysis and conception of systems

Wednesday March 14, 2018, 2PM, Salle UFR

**Thomas Letan** (Agence Nationale de la Sécurité des Systèmes d’Information & INRIA Rennes) *FreeSpec : Modular Verification of Systems using Effects and Effect Handlers in Coq*

Even though system components are generally carefully designed and even verified by different groups of people, the \textit{composition} of these components is often regarded with less attention.

This paves the way for “architectural attacks”, a class of security vulnerabilities where the attacker is able to threaten the security of the system even if each of its component continues to act as expected.

In this article, we introduce FreeSpec, a Coq framework built upon the key idea that components can be modelled as programs with algebraic effects to be realized by other components.

FreeSpec allows for the modular modelling of a complex system, by defining idealized components connected together, and the modular verification of the properties of their composition.

In doing so, we propose a novel approach for the Coq proof assistant to reason about programs with effects in a modular way.

Analysis and conception of systems

Monday February 19, 2018, 11AM, Salle 3052

**Adrien Boiret** (University of Warsaw) *The “Hilbert Method” for Solving Transducer Equivalence Problems*

Consider an algebra A in the sense of universal algebra, i.e. a set equipped with some operations. A grammar over A is like a context-free grammar, except that it generates a subset of the algebra A, and the rules use operations from the algebra A. The classical context-free grammars are the special case when the algebra A is the free monoid with concatenation. Using the “Hilbert method” one can decide certain properties of grammars over algebras that are fields or rings of polynomials over a field. The “Hilbert method” extends to grammars over certain well-behaved algebras that can be “coded” into fields or rings of polynomials. Finally, for these well-behaved algebras, one can also use the “Hilbert method” to decide the equivalence problem for transducers (of a certain transducer model that uses registers) that input trees and output elements of the well-behaved algebra.

In the talk, we give examples and non-examples of well-behaved algebras, and discuss the decidability / undecidability results connected to them. In particular:

-We show that equivalence is decidable for transducers that input (possibly ordered) trees and output unranked unordered trees.

-We show that equivalence is undecidable for transducers that input words and output polynomials over the rational numbers with one variable (but are allowed to use composition of polynomials).

Joint work with Mikołaj Bojańczyk, Janusz Schmude, Radosław Piórkowski at Warsaw University.

Joint session with the Verification seminar

Analysis and conception of systems

Wednesday February 7, 2018, 2PM, Salle 3052

**Hongseok Yang** (University of Oxford) *Informal introduction to integral probability metrics and generative adversarial networks*

References: Wasserstein GAN https://arxiv.org/abs/1701.07875

Generative Models and Model Criticism via Optimized Maximum Mean Discrepancy https://arxiv.org/abs/1611.04488

Maximum Mean Discrepancy http://alex.smola.org/teaching/iconip2006/iconip_3.pdf

#### Year 2017

Analysis and conception of systems

Tuesday November 28, 2017, 1:30PM, Salle 3052

**Leon Gondelman** (Institute for Computation and Information Sciences (Radboud Univ.), Netherlands) *The Spirit of Ghost Code*

In this talk, we describe a simple ML-style programming language with mutable state and ghost code. Non-interference is ensured by a type system with effects, which allows, notably, the same data types and functions to be used in both regular and ghost code. We define the procedure of ghost code erasure and we prove its safety using bisimulation. A similar type system, with numerous extensions which we briefly discuss, is implemented in the program verification environment Why3.

Analysis and conception of systems

Wednesday October 18, 2017, 2:30PM, Salle 3052

**Nicolas Behr** (IRIF) *The stochastic mechanics of graph rewriting via the rule algebra framework - an introduction*

Analysis and conception of systems

Thursday June 8, 2017, 2PM, Salle 3052

**Eric Goubault** (LIX, École Polytechnique) *A simplicial complex model of dynamic epistemic logic for fault-tolerant distributed computing*

We choose distributed computing as a case study to work out in detail the dynamic epistemic simplicial complex theory. The reason is that distributed computability has been studied using combinatorial topology, where the set of all possible executions in a distributed system is represented by a simplicial complex. We establish a formal, categorical equivalence between Kripke models and simplicial complex epistemic models.

In one direction, the connection provides a dynamic epistemic logic semantics to distributed computability, opening the possibility of reasoning about knowledge change in distributed computing. In the other direction, the connection allows to bring in the topological invariants known in distributed computing, to dynamic epistemic logic, and in particular show that knowledge gained after an epistemic action model is intimately related to higher dimensional topological properties.

Analysis and conception of systems

Monday May 29, 2017, 2PM, Salle 3052

**Silvia Crafa** (Università di Padova) *Formal methods in action: typestate-oriented actor programming in Scala-Akka*

Analysis and conception of systems

Thursday May 18, 2017, 2:30PM, Salle 3052

**Giovanni Bernardi** (IRIF) *Full-abstraction for Must Testing Preorders*

Analysis and conception of systems

Tuesday May 2, 2017, 11AM, Salle 3052

**Joachim Breitner** (University of Pennsylvania) *Who needs theorem provers when we have compilers?*

But one powerful tool capable of doing (some of) these proofs is hidden in plain sight: GHC, the Haskell compiler! Its optimization machinery, in particular the simplifier, can prove many simple equations all by himself, simply by compiling both sides and noting that the result is the same. Furthermore, and crucially to make this approach applicable to more complicated equations, the compiler can be instructed to do almost arbitrary symbolic term rewritings by using Rewrite Rules.

In this rather hands-on talk I will show a small GHC plugin that I can use to prove the monad laws for a non-trivial functor. I am looking forward to a discussion of the merits, limits and capabilities of this approach.

#### Year 2016

Analysis and conception of systems

Thursday December 1, 2016, 10:30AM, Salle 1007

**Julien Lange** (Imperial College) *Building Graphical Choreographies From Communicating Machines: Principles and Applications*

Organisation jointe avec le séminaire de l'équipe PPS

Analysis and conception of systems

Thursday June 23, 2016, 2:30PM, Salle 1007

**Elisabeth Remy** (Institut de Mathématiques de Luminy) *Analyse qualitative des réseaux de régulation génétiques*

Analysis and conception of systems

Thursday May 26, 2016, 2:30PM, Salle 1008

**Ralf Treinen** (IRIF) *Towards the verification of file tree transformations - the Colis project*

A possible example of a program specification is absence of execution error under certain initial conditions. Automatic program verification even for this kind of specification is a challenging task. In case of Debian maintainer scripts we are faced with even more challenging properties like idempotency of scripts (required by policy), or commutation of scripts.

The project is still in the beginning, so there are no results yet to present. However, I will explain why I think that the case of Debian maintainer scripts is very interesting for program verification : some aspects of scripts (POSIX shell, manipulation of a complex data structure) make the problem very difficult, while other aspects of the Debian case are likely to make the problem easier than the task of verifying any arbitary shell script.

Analysis and conception of systems

Thursday April 7, 2016, 2:30PM, Salle UFR

**Tobias Heindel** (University of Copehagen) *Computing means and moments of occurrence counts: rule-based modeling meets adaptive uniformization and finite state projection*

` in rule-based models; computability is in the sense of Weihrauch. Roughly, established techniques, namely adaptive uniformization and finite state projection, can be reused – provided that occurrence counts (and their powers) are bounded by a polynomial in the ``size`

of the rule-based system and the ``size'' of the system does not explode. The most interesting results can be obtained for context-free systems, which can be thought of as branching processes equipped with structure; for these systems we have PTIME computability.
All results will be exemplified for the case of string rewriting, aiming for a widest possible audience of computer scientists, assuming only basic knowledge of continous time Markov chains with countable state space. Computing the time evolution of mean word counts in stochastic string rewriting is already highly non-trivial, even if it is the most basic example. The GEM OF THE TALK is the computation of mean word counts for context-free grammars!