Lien iCal public : https://calendar.google.com/calendar/ical/proval%40lri.fr/public/basic.ics
Seminars
Agenda
Séminaires antérieurs
Proving cryptographic protocols: the complex relationship between symbolic and computation models
Speaker: Guillaume Scerri, Université de Versailles
Tuesday 8 March 2022, 11:00, (salle 1Z34 ENS Paris-Saclay)
Abstract: A number of different models coexist for proving cryptographic protocols. They can roughly be divided in two classes. First, the so called computational model deals with probabilistic Turing machines, precise reductions to specific cryptographic hypotheses often with explicit bounds, and provides very strong guarantees against adversaries that are close to real world. Second the symbolic models, that abstract away probabilities, and model the adversary as a specific list of capabilities. While the computational model provides stronger guarantees, proofs in this model are generally rather complex, hard to check, and not amenable to automation. On the other hand symbolic models typically allow for automated or quasi automated proofs in a much simpler framework. In this talk we will first explore why it is so hard to obtain symbolic models that soundly abstract the computation models. We will then present a fairly recent development, the computationally complete symbolic attacker, developed by Bana and Comon, that takes the opposite approach of usual symbolic models and model what the attacker cannot do rather than modelling the attacker through a list of capabilities. We will explore how this model allows for more modular proofs and proof composition results, and may even allow for efficiently deriving explicit bounds of reductions without ever dealing with the complexity of computational models.
On the strategy synthesis problem in MDPs: probabilistic CTL and rolling windows.
Speaker: Damien Busatto-Gaston, Université Libre de Bruxelles (ULB)
Tuesday 15 February 2022, 11:00, (online)
Abstract: In this talk I will present ongoing work on Markov decision processes. Given an MDP and a formula phi, the strategy synthesis problem asks if there exists a strategy for the MDP such that the resulting Markov chain satisfies phi. This challenging problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced globally. Moreover, we allow for linear expressions in the probabilistic inequalities. We show that this class of formulae is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis becomes decidable when strategies are either deterministic or memoryless, while the general problem remains undecidable. We compare with results on the entire PCTL logic and consider applications to the PCTL satisfiability problem.
WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms
Speaker: Benjamin Farinier, TU Wien, Austria
Tuesday 25 January 2022, 11:00, (online)
Abstract: The complexity of browsers has steadily increased over the years, driven by the continuous introduction and update of Web platform components, such as novel Web APIs and security mechanisms. Their specifications are manually reviewed by experts to identify potential security issues. However, this process has proved to be error-prone due to the extensiveness of modern browser specifications and the interplay between new and existing Web platform components. To tackle this problem, we developed WebSpec, the first formal security framework for the analysis of browser security mechanisms, which enables both the automatic discovery of logical flaws and the development of machine-checked security proofs. WebSpec, in particular, includes a comprehensive semantic model of the browser in the Coq proof assistant, a formalization in this model of ten Web security invariants, and a compiler turning the Coq model and the Web invariants into SMT-lib formulas.
We showcase the effectiveness of WebSpec by discovering two new logical flaws caused by the interaction of different browser mechanisms and by identifying three previously discovered logical flaws in the current Web platform, as well as five in old versions. Finally, we show how WebSpec can aid the verification of our proposed changes to amend the reported inconsistencies affecting the current Web platform.
Active learning for sound negotiations
Speaker: Anca Muscholl, LaBRI
Tuesday 18 January 2022, 11:00, (online)
Abstract: We present an active learning algorithm for sound deterministic negotiations. Sound deterministic negotiations are graph-based models of distributed systems, a kind of Petri nets or Zielonka automata with additional structure. We show that sound deterministic negotiations can be minimised. Our learning algorithm has similar complexity to Angluin’s L* algorithm, in particular, the number of queries is polynomial in the size of the negotiation, and not in the number of configurations.
Joint work with Igor Walukiewicz. Extended abstract: here
Formal methods at Thales Research & Technology
Speakers: Delphine Longuet, Nikolai Kosmatov and Romain Soulat from THALES Research & Technology
Tuesday 11 January 2022, 11:00, (online)
Abstract: Formal methods adoption in Thales teams is often led by developments and experiments at the research center. Over the years, we worked on a wide variety of formal methods techniques and benchmarked a lot of tools from the academia and industry. In this talk, we present three particular past or ongoing projects:
- the model checking of a real-time distributed algorithm
- the ongoing development of an automated test generation tool suite for Ada
- the formal verification of a JavaCard virtual machine with Frama-C.
Through those three projects, we present an illustrative selection of the job done at the research center by our team in the last few years.
E-voting protocols - how to analyse the security of these (real-world) systems?
Speaker: Alexandre Debant, Inria
Tuesday 04 January 2022, 11:00, (online)
Abstract: For many years, e-voting protocols have been designed and formal methods (computational or symbolic) have been developed to prove the main properties that such systems must satisfy, e.g. vote secrecy and verifiability. Based on these security proofs, e-voting systems are now used (or ready to be) in our daily life for association elections, company elections, or even political elections (e.g. in Switzerland, Estonia, Australia…).
In this talk I will first introduce the topic of e-voting and how symbolic models can be used to provide security proofs. Then, I will discuss the accuracy of the models in comparison to the real-world constraints that arise when these protocols are deployed in practice. To this aim, I will present new attacks we discovered. Finally, I will talk about some properties (e.g. cast-as-intended, accountability) which are at the limit of the state-of-the-art in symbolic analysis and what we are doing to overcome these limitations.
Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant
Speaker: Nicolas Magaud, IGG, Université de Strasbourg.
Thursday 14 April 2022, 11:00, (room 1Z61 ENS Paris-Saclay and online)
Abstract: We formally implement the smallest three-dimensional projective space PG(3,2) in the Coq proof assistant. This projective space features 15 points and 35 lines, related by an incidence relation. We define points and lines as two plain datatypes (one with 15 constructors for points, and one with 35 constructors for lines) and the incidence relation as a boolean function, instead of using the well-known coordinate-based approach relying on GF(2)^4. We prove that this implementation actually verifies all the usual properties of three-dimensional projective spaces. We then use an oracle to compute some characteristic subsets of objects of PG(3,2), namely spreads and packings. We formally verify that these computed objects exactly correspond to the spreads and packings of PG(3,2). For spreads, this means identifying 56 specific sets of 5 lines among 360 360 (= 15 x 14 x 13 x 12 x 11) possible ones. We then classify them, showing that the 56 spreads of PG(3,2) are all isomorphic whereas the 240 packings of PG(3,2) can be classified into two distinct classes of 120 elements. Proving these results requires partially automating the generation of some large specification files as well as some even larger proof scripts. Overall, this work can be viewed as an example of a large-scale combination of interactive and automated specifications and proofs. It is also a first step towards formalizing projective spaces of higher dimension, e.g. PG(4,2), or larger order, e.g. PG(3,3).
Hazel: a Separation Logic for effect handlers
Speaker: Paulo de Vilhena, Inria Paris.
Tuesday 19 April 2022, 11:00, (room 1Z31 ENS Paris-Saclay and online)
Abstract: A program logic is a pair of a language, for writing specifications, and a set of reasoning rules, for deriving specifications. In this talk, I present Hazel, a program logic for effect handlers. I start by laying out the motivation for such work and then I present its main ideas: how to write the specification of effectful programs in Hazel and what reasoning principles does it suggest? Finally, I apply these ideas to `invert`, a function that exploits effect handlers to produce a lazy sequence (a cascade) out of a higher-order iteration function.
Avoiding deadlocks in lock-sharing systems
Speaker: Corto Mascle, LaBRI.
Tuesday 12 April 2022, 11:00, (room 1Z71 ENS Paris-Saclay and online)
Abstract: We consider the distributed control problem for systems with locks. We introduce a model in which some processes running in parallel cannot communicate directly, but may acquire or release some shared locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable, but in this talk we will focus on systems in which each process can access at most two locks. The problem then becomes complete for the second level of the polynomial hierarchy, and even in PTIME under some additional assumptions. The dining philosophers problem satisfies these assumptions.
The relational semantics, and beyond
Speaker: Giulio Manzonetto, LIPN.
Tuesday 19 April 2022, 10:00, (room 1Z71 ENS Paris-Saclay and online)
Abstract: Since the pioneering work by Barendregt, Dezani-Ciancaglini and Coppo, some models of lambda-calculus are based on filters and can be presented as intersection type systems. The interpretation of a program in these models is just the set of its types, which is a filter. Filter models can be used to capture operational properties of programs like normalization, head normalization, or solvability, but establishing these results often requires impredicative techniques like Girard's reducibility candidates. In this talk we present a more recent class of models, called relational models and arising from a simple quantitative semantics of linear logic (LL). We show that these models can be presented as intersection type systems where the intersection operator is however non-idempotent. Due to the resource sensitive nature of LL , we are able to capture operational properties bypassing impredicative techniques. Starting for the type of a program, it is indeed possible to extract an upper bound to the amount of steps needed to reach its value. We will see that generalizing this semantics from the Boolean semiring to continuous semi-ring allows to compare programs not only with respect to "what they can do", but also "in how many steps" or "in how many different ways" (for non-deterministic PCF) or even "with what probability" (for probabilistic PCF). Finally, generalizing relations to the higher-dimension (profunctors) allows us to obtain the characterization of the theory of a model as a simple corollary of the Approximation Theorem.