DIENS

Résumé :

L'usage sans précédent du machine learning (ML) ou \emph{apprentissage automatique}, motivé par les possibilités qu'il apporte dans un grand nombre de secteurs, interroge de plus en plus en raison du caractère sensible des données qui doivent être utilisées et du manque de transparence sur la façon dont ces données sont collectées, croisées ou partagées. Aussi, un certain nombre de méthodes se développent pour réduire son intrusivité sur notre vie privée, afin d'en rendre son usage plus acceptable notamment dans des domaines tels que la santé, où son potentiel est encore très largement sous-exploité. Cette thèse explore différentes méthodes issues de la cryptographie ou plus largement du monde de la sécurité et les applique au machine learning afin d'établir des garanties de confidentialité nouvelles pour les données utilisées et les modèles de ML. Notre première contribution est le développement d'un socle technique pour implémenter et expérimenter de nouvelles approches au travers d'une librairie open-source nommée PySyft. Nous proposons une architecture modulaire qui permet à chacun et chacune d'utiliser les briques de confidentialité nécessaires selon son contexte d'étude, ou encore de développer et d'interfacer de nouvelles briques. Ce socle sert de base à l'ensemble des implémentations proposées dans cette thèse. Notre seconde contribution consiste à mettre en lumière la vulnérabilité des modèles de ML en proposant une attaque qui exploite un modèle entraîné et permet de révéler des attributs confidentiels d'un individu. Cette attaque pourrait par exemple détourner un modèle qui reconnaît le sport fait par une personne à partir d'une image, pour détecter les origines raciales de cette personne. Nous proposons des pistes pour limiter l'impact de cette attaque. Dans un troisième temps, nous nous intéressons à certains protocoles de cryptographie qui permettent de faire des calculs sur des données chiffrées. Une première étude propose un protocole de chiffrement fonctionnel qui permet de réaliser des prédictions grâce à un petit modèle de ML à partir de données chiffrées et de ne rendre public que la prédiction. Une seconde étude porte sur l'optimisation d'un protocole de partage de secret fonctionnel, qui permet d'entraîner ou d’évaluer un modèle de ML sur des données de façon privée, c’est à dire sans révéler à quiconque ni le modèle ni les données. Ce protocole offre des performances suffisantes pour utiliser des modèles qui ont une utilité pratique dans des tâches non triviales comme la détection de pathologies dans les radiographies de poumons. Dans un dernier temps, nous intéressons à la confidentialité différentielle qui permet de limiter la vulnérabilité des modèles de ML et donc l’exposition des données qui sont utilisées lors de l’entraînement, en introduisant une perturbation contrôlée. Nous proposons un protocole et démontrons qu’il offre notamment la possibilité d'entraîner un modèle lisse et fortement convexe en garantissant un niveau de confidentialité indépendant du nombre d'accès aux données sensibles lors de l’entraînement.

Abstract:

The ever growing use of machine learning (ML), motivated by the possibilities it brings to a large number of sectors, is increasingly raising questions because of the sensitive nature of the data that must be used and the lack of transparency on the way these data are collected, combined or shared. Therefore, a number of methods are being developed to reduce its impact on our privacy and make its use more acceptable, especially in areas such as healthcare where its potential is still largely under-exploited. This thesis explores different methods from the fields of cryptography and security, and applies them to machine learning in order to establish new confidentiality guarantees for the data used and the ML models. Our first contribution is the development of a technical foundation to facilitate experimentation of new approaches, through an open-source library named PySyft. We propose a modular architecture that allows one to pick the confidentiality blocks necessary for one's study, or to develop and easily integrate new blocks. This library is reused in all the implementations proposed in this thesis. Our second contribution consists in highlighting the vulnerability of ML models by proposing an attack that exploits a trained model to reveal confidential attributes of an individual. This attack could, for example, subvert a model that recognizes a person's sport from an image, to detect the person's racial origins. We propose solutions to limit the impact of this attack. In a third step, we focus on some cryptographic protocols that allow us to perform computations on encrypted data. A first study proposes a functional encryption protocol that allows to make predictions using a small ML model over encrypted data and to only make the predictions public. A second study focuses on optimizing a functional secret sharing protocol, which allows an ML model to be trained or evaluated on data privately, i.e. without revealing either the model or the data to anyone. This protocol provides sufficient performance to use models that have practical utility in non-trivial tasks such as pathology detection in lung X-rays. Our final contribution is in differential privacy, a technique that limits the vulnerability of ML models and thus the exposure of the data used in training by introducing a controlled perturbation. We propose a new protocol and show that it offers the possibility to train a smooth and strongly convex model with a bounded privacy loss regardless of the number of calls to sensitive data during training.

Jury :

• Aurélien Bellet - INRIA Lille (Rapporteur)
• Yuval Ishai - Technion (Rapporteur)
• Renaud Sirdey - CEA (Examinateur)
• Mariya Georgieva - Inpher (Examinatrice)
• Laurent Massoulié - INRIA, ENS, PSL (Examinateur)
• Jonathan Passerat-Palmbach - Imperial College London (Examinateur)
• David Pointcheval - ENS, CNRS, PSL (Directeur de thèse)
• Francis Bach - INRIA, ENS, CNRS, PSL (Directeur de thèse)

Jury

• Frédéric Lavancier [Université de Nantes] Rapporteur
• Kai Schneider [Université Aix-Marseille] Rapporteur
• Djalil Chafaï [École Normale Supérieure] Examinateur
• Agnès Desolneux [CNRS] Examinatrice
• Brice Ménard [Johns Hopkins University] Examinateur
• Bartłomiej Błaszczyszyn [Inria] Directeur de thèse
• Stéphane Mallat [Collège de France] Co-directeur de thèse

Abstract

This dissertation presents a class of representations of spatial point processes. Inspired from the success of wavelet methods in signal processing, these descriptors rely on the convolution of a point process with a family of wavelet filters. From these convolutions are built sets of statistical descriptors of stationary point process, by applying non-linear operators, followed by a spatial averaging. Much like classical summary characteristics for point processes, these statistics are designed to extract information about the process with a relatively small number of numerical values, by describing its geometry. Their goal is to describe whether the atoms of the process tend to repel each other, or cluster together, and by doing so, form possibly complex geometric shapes. By construction, these descriptors enjoy several properties that make them suitable for statistical analysis and learning tasks. To illustrate the quality of these representations as statistica! l descriptors, we study several problems involving statistical analysis of point processes. In a first experiment, we seek to estimate an unknown function that takes as input a point pattern, and returns a marked version of this pattern, where a numerical value is associated to each atom of the pattern. We use a wavelet-based representation of point patterns to estimate the relation between their non-marked and marked version. We then study, in a second experiment, the ability of such representations to model the distribution of a point process, by defining a maximum entropy model defined by a set of wavelet-based statistics, computed on a single observation. For these two problems, we observe that our representations lead to better performance than summary statistics commonly used in the literature on point processes. Finally, to study to what extent such representations can capture geometric structures of texture images, we define a maximum entropy model relying on simil! ar wavelet statistics, yielding syntheses of similar visual quality to state-of-the-art models based on deep convolutional neural networks representations.

L'an dernier nous sommes plusieurs à avoir fait une césure pour créer un jeu vidéo. Nous vous présenterons les différentes étapes de ce projet, ainsi que le problèmes informatiques auxquels nous avons été confrontés. Du dessin avec OpenGL, à la réalisation d'un moteur physique en passant par l'intelligence artificielle des PNJ, ce projet nous aura fait mettre en pratique beaucoup de connaissances théoriques d'Informatique. Séminaire repoussé à une date ultérieure

Jury :

• Georg Fuchsbauer, TU Wien (Directeur de thèse)
• David Pointcheval, CNRS, École Normale Supérieure (Directeur de thèse)
• Marc Fischlin, TU Darmstadt (Rapporteur)
• Damien Vergnaud, Sorbonne Université (Rapporteur)
• Yannick Seurin, ANSSI (Examinateur)
• Esha Ghosh, Microsoft Research (Examinatrice)

Résumé

L’hypothèse de sécurité appelée "one more-discrete logarithm" (OMDL) est centrale dans l’analyse de sécurité des protocoles d’identification, les signatures aveugles ainsi que les récentes multi-signatures MuSig2. Malgré sa grande utilisation, il est surprenant que OMDL n’a jamais été rigoureusement analysée. Dans cette thèse, nous donnons une preuve rigoureuse de OMDL dans le Modèle du Groupe Générique (GGM) ainsi que d’autres hypothèses en lien. Les signatures de Schnorr aveugles sont un protocole qui permet d’envoyer à l’aveugle des signatures de Schnorr, qui sont parmi les signatures les plus utilisées. De même que OMDL, en dépit de leur utilité pratique, l’analyse de sécurité (basée sur OMDL) de ces signatures est insatisfaisant. Nous analysons la sécurité de ces protocoles dans le Modèle du Groupe Algébrique (AGM), qui est un modèle idéalisé plus proche du modèle standard que du GGM. Pour le renforcer, nous proposons une modification simple du protocole de signature, qui laisse les signatures inchangées.

Abstract

The one more-discrete logarithm assumption (OMDL) is central to the security analysis of identification protocols, blind signatures and multi-signature schemes, most notably blind Schnorr signatures and the recent MuSig2 multi-signatures. Despite its wide use, surprisingly, OMDL is lacking any rigorous analysis. In this work we give rigorous proofs in the Generic Group Model of OMDL and a related assumption. The Schnorr blind signing protocol allows blind issuing of Schnorr signatures, one of the most widely used signatures. As for OMDL, despite its practical relevance, its security analysis (based on OMDL) is unsatisfactory. We analyze the security of these schemes in the algebraic group model (AGM), an idealized model closer to the standard model than the GGM.

Résumé :

L'informatique se fonde sur de nombreuses couches d'abstraction, allant des couches matérielles jusqu'à l'algorithmique en passant par le cahier des charges à la base de la conception du produit. Dans le cadre de la sécurité informatique, les vulnérabilités proviennent souvent de la confusion résultant des différentes abstractions décrivant un même objet. La définition de sémantiques aide à la description formelle de ces abstractions dans l'objectif de les faire coïncider. Dans cette thèse, nous améliorons différents procédés ou programmes en corrélant les diverses représentations sémantiques sous-jacentes.

Nous introduisons brièvement les termes et concepts fondamentaux avec lesquels nous construisons le concept de langage assembleur ainsi que les différentes abstractions utilisées dans l'exploitation de programmes binaires.

Dans une première partie, nous utilisons des constructions sémantiques de haut niveau pour simplifier la conception de codes d'exploitation avancés sur des jeux d'instructions récents. Nous présentons didactiquement trois exemples répondant à des contraintes de plus en plus complexes. Spécifiquement, nous présentons une méthode pour produire des shellcodes alphanumériques sur ARMv8-A et RISC-V, ainsi que la première analyse de faisabilité d'attaques de type return-oriented programming sur RISC-V.

Dans une deuxième partie, nous étudions l'application des méthodes formelles à l'amélioration de la sécurité et de la sûreté de langages de programmation à travers trois exemples : une optimisation de primitives de synchronisation, une analyse statique compatible avec la vérification déductive limitant l'aliasing de pointeurs dans un langage impératif ou encore un formalisme permettant de représenter de façon compacte du code binaire dans le but d'analyser des problèmes de synchronisation de protocole.

Abstract:

Computer science is built on many layers of abstraction, from hardware to algorithms or statements of work. In the context of computer security, vulnerabilities often originate from the discrepancies between these different abstraction levels. Such inconsistencies may lead to cyberattacks incurring losses. As a remedy, providing semantics helps formally describe and close the gap between these layers. In this thesis, we improve methods and programs by connecting the various semantic representations involved using their relationship to each level of abstraction.

We briefly introduce the fundamental concepts and terminology to build assembly languages from scratch and various abstractions built atop and used in the context of binary exploitation.

In the first part, we leverage higher-level semantic constructs to reduce the design complexity of advanced exploits on several recent instruction set architectures. In a tutorial-like fashion, we present three examples addressing increasingly more complex constraints. Specifically, we describe a methodology to automatically turn arbitrary programs into alphanumeric shellcodes on ARMv8-A and on RISC-V. We also provide the first analysis on the feasibility of return-oriented programming attacks on RISC-V.

In the second part, we see how the use of formal methods can improve the safety and security of various languages or constructs, through three examples that respectively optimize the implementation of Hoare monitors, a well-known synchronization construct, prevent harmful aliasing in an imperative language without impeding deductive verification, or abstract binary code into a compact representation which enables further protocol desynchronization analyses.

Jury :

• David NACCACHE - Ecole normale supérieure (Directeur de thèse)
• Aymeric VINCENT - Commissariat à l'énergie atomique et aux énergies alternatives (Encadrant de thèse)
• Lorenzo CAVALLARO - University College London (Rapporteur)
• Sylvain GUILLEY - Télécom ParisTech (Rapporteur)
• Whitfield DIFFIE - Stanford University (Examinateur)
• Konstantinos MARKANTONAKIS - Royal Holloway University of London (Examinateur)
• Clémentine MAURICE - Centre national de la recherche scientifique (Examinatrice)
• Xavier RIVAL - Ecole normale supérieure (Examinateur)
• Hovav SHACHAM - University of Texas at Austin (Professeur invité)

Résumé :

The recent success of convolutional neural networks in high-dimensional learning problems motivated the development of new machine learning techniques in different fields. In particular, a lot of progress has been made in image classification and energy regression in physics in the last years. These two problems are multi-scale. Molecules' and solids' energy results from interactions at different scales, e.g., ionic and covalent bonds at the short scale, Van-der-Waals interactions at the mesoscale, Coulomb interactions at the large scale. One can classify an image using texture information at the small scale, pattern information at a larger scale, or shape information at the object scale. There is a natural analogy between local image classification techniques based on small image patches and local energy regression techniques based on small atomic neighborhood descriptions.

Abstract:

This dissertation studies the efficiency of local methods in image classification and energy regression. We observe that local methods perform surprisingly well in image classification and energy regression despite these two problems' multi-scale nature. We first study comparatively multi-scale and local energy regression techniques for molecules and solids. We notice that local methods perform very well, even for solids with long-range energy components. We present a new strategy to regress the vibrational entropy in solids. Again, we observe that a local method based on atomic neighborhood description has better predictive power than a multi-scale strategy. We introduce a structured convolutional network architecture for image classification based on patch encoding that reaches an accuracy that is competitive with standard convolutional networks on ImageNet. We present an image classifier based on image patches K-nearest-neighbors computations that achieves state-of-the-art performance as a non-learned representation. We end this dissertation with an opening on artistic creativity in the context of human-machine interactive systems.

Recently, there is growing concern that machine-learned software, which currently assists or even automates decision making, reproduces, and in the worst case reinforces, bias present in the training data. The development of tools and techniques for certifying fairness of this software or describing its biases is, therefore, critical. To meet these needs, we propose a perfectly parallel static analysis for certifying fairness of feed-forward neural networks used for classification of tabular data. When certification succeeds, our approach provides definite guarantees, otherwise, it describes and quantifies the biased input space regions. We design the analysis to be sound, in practice also exact, and configurable in terms of scalability and precision, thereby enabling pay-as-you-go certification. We implement our approach in an open-source tool called Libra and demonstrate its effectiveness on neural networks trained on popular datasets.

DNA-based storage has attracted significant attention due to recent demonstrations of the viability of storing information in macromolecules. Given the trends in cost decreases of DNA synthesis and sequencing, it is estimated that within the next decade DNA storage may become a highly competitive archiving technology. This technology introduces new challenges in finding coding solutions to address various problems associated with the implementation of DNA-based storage systems. This talk will review the main ideas of recent coding methods and techniques of advanced coding schemes that are specifically targeted for the unique structure and error behavior of DNA-based storage systems. These problems will focus on the design of codes for clustering, trace-reconstruction techniques, error-correction codes, and constrained codes. These families of codes are most suitable and applicable for long-term storage and recovery of data recorded in DNA, while overcoming the unique challenges associated with the synthesis, storage, and sequencing phases of the DNA storage channel.

Résumé:

L’accélération de la numérisation des communications mondiales s’accompagne d’une sensibilisation croissante de pans entiers de la société concernant la notion de vie privée. En particulier, la confidentialité des transactions commerciale fait débat. Dans les années 80-90, Chaum, un cryptographe, élabore, puis déploie avec son entreprise Digicash un système de paiement numérique «anonyme» dont les garanties reposent entre autres sur des preuves mathématiques inspirées par le paradigme encore balbutiant de «sécurité prouvée». Si son entreprise Digicash fait faillite au bout de quelques années, les milieux académiques continuent d’étudier les systèmes de paiements numériques anonymes en cherchant à développer de nouvelles fonctionnalités, dont la transferabilité.

L’objectif de cette thèse, financée par l’agence nationale de la recherche était de revisiter les modèles de sécurité concernant l’anonymat d’un paiement, puis de proposer un système de paiement théoriquement déployable reposant également sur le paradigme de la sécurité prouvée. Lors de la défense de cette thèse (qui se fera en anglais), je parlerais à la fois des modèles de sécurité garantissant l’anonymat, et de questions plus fondamentales concernant toutes une famille d’hypothèses cryptographiques couramment utilisées en sécurité prouvée.

Jury:

• Georg Fuchsbauer - TU Wien, Austria (Directeur de thèse)
• David Pointcheva - CNRS/ENS (Directeur de thèse)
• Eike Kiltz - Ruhr-University Bochum, Germany (Rapporteur)
• Olivier Blazy - Université Limoges (Rapporteur)
• Carla Rafols - Universitat Pompeu Fabra, Barcelona, Spain (Examinatrice)
• Olivier Sanders - Orange Labs, Rennes (Examinateur)
• Damien Vergnaud - Sorbonne Université (Examinateur)

Abstract:

As the digitization of global communications accelerates, there is a growing awareness of privacy issues among large segments of society. In particular, the confidentiality of commercial transactions is under debate. In the 1980s and 1990s, Chaum, a cryptographer, developed and then deployed with his company Digicash an "anonymous" digital payment system whose guarantees were based, among other things, on mathematical proof inspired by the still nascent paradigm of "proven security". Although his company Digicash goes bankrupt after a few years, the academic community continues to study anonymous digital payment systems, seeking to develop new functionalities, including transferability.

The aim of this thesis, funded by the French national research agency, was to revisit security models concerning the anonymity of payments, and then to propose a theoretically deployable payment system also based on the paradigm of proven security. During the defense of this thesis, I will talk about security models guaranteeing anonymity, as well as more fundamental questions concerning a family of cryptographic assumptions commonly used in proven security.

Programs are in charge of many systems whose failure may be catastrophic in many ways, from mere information leaks to deaths. Fortunately, there are methods that allows us to find all bugs, and thus, that are able to prove that programs are correct. The method we use, abstract interpretation, is based on overapproximation of the semantics. Usually, verification efforts are centered on end-user programs, but software systems are big stacks of components, from regular programs to silicon, where each step may fail. Consequently, we need to prove the correctness each component.

In this thesis, we intend to analyze a real-world embedded operating system for x86 architecture, in collaboration with an industrial partner. Such low-level code raises two kinds of difficulties. Firstly, C code includes assembly blocks. They are useful to use the processor's features, and to perform computation in a more precise way than what C allows. Such mixed code is difficult to analyze because both languages are mixed with fine-grained interactions, but works in very different ways.

The second issue is the kind of computations the OS needs to do, for instance, to use CPU's memory protection features. They make no sense for a regular program, but they can be abstracted precisely using ghost variables, that is, helping values that do not appear in the real execution, but help the analysis.

In this thesis, we treated both problems: we propose a quite extensive support of mixed C and x86 assembly (including arbitrary dynamic jumps, mixed calls, and dynamic code), and a new reduced product of abstract domains that allows dynamic management of ghost variables in a decentralized way.

Jury:

• Isabella MASTROENI (reviewer)
• David PICHARDIE (reviewer)
• Patrick COUSOT
• Peter MÜLLER
• Marc POUZET
• Sukyoung RYU
• Mihaela SIGHIREANU
• Jérôme FERET (supervisor)

The goal of this thesis is to build and train machine learning models capable of understanding the content of videos. Current video understanding approaches mainly rely on large-scale manually annotated video datasets for training. However, collecting and annotating such dataset is cumbersome, expensive and time-consuming. To address this issue, this thesis focuses on leveraging large amounts of readily-available, but noisy annotations in the form of natural language. In particular, we exploit a diverse corpus of textual metadata such as movie scripts, web video titles and descriptions or automatically transcribed speech obtained from narrated videos. Training video models on such readily-available textual data is challenging as such annotation is often imprecise or wrong. In this thesis, we introduce learning approaches to deal with weak annotation and design specialized training objectives and neural network architectures.
Lien vers PDF

Jury

• Bernard Ghanem (KAUST), Rapporteur
• Dima Damen (University of Bristol), Rapporteuse
• Vincent Lepetit (ENPC), Président de jury
• Cordelia Schmid (Inria / Google), Examinatrice
• Jean-Baptiste Alayrac (DeepMind), Examinateur
• Ivan Laptev (Inria), Directeur de thèse
• Josef Sivic (CTU / Inria), Directeur de thèse

This manuscript proposes new cryptographic protocols that are respectful of users’ privacy and which have real-world applications. In a first part, the focus is on group signatures, a primitive which allows members of a user group to anonymously sign on behalf of the group, and on message confidentiality. To remove the trust on single authorities, group signatures are here defined in a setting with multiple authorities and support both threshold issuance and threshold opening. These group signatures are then used as authentication mechanism for vehicle-to-vehicle communication, and combined with zone encryption, a new primitive whereby vehicles can efficiently encrypt their communication, they provide strong, well-defined privacy guarantees for cooperative intelligent transport systems. Thereafter, public-key encryption is studied in a more general context in which users do not have access to secure storage to protect their secret keys, but can leverage passwords and interaction with servers to obtain comparable security guarantees without renouncing their privacy. In a second part, the topic of study are general-purpose cryptographic primitives which have privacy-preserving applications. First come zero-knowledge arguments, a type of cryptographic schemes which enable a computationally bounded prover to convince a verifier of a statement without disclosing any information beyond that. More specifically, we study arguments to prove the satisfiability of Diophantine equations which have logarithmic communication and round complexity, as well as their applications to privacy-preserving cryptography. Then, we tackle the problem of proving that a user algorithm selected and correctly used a truly random seed in the generation of her cryptographic key, a problem of fundamental importance to the security of any public-key cryptographic scheme.

Jury

• Dario Fiore, IMDEA Software Insitute (Reviewer)
• Dennis Hofheinz, ETH Zürich (Reviewer)
• Benoît Libert, CNRS, École Normale Supérieure de Lyon (Examiner)
• Gregory Neven, DFINITY (Examiner)
• Duong Hieu Phan, Télécom Paris, Institut Polytechnique de Paris (Examiner)
• David Pointcheval, CNRS, École Normale Supérieure de Paris (Examiner)
• Carla Ràfols, Universitat Pompeu Fabra (Examiner)
• Damien Vergnaud, Sorbonne Université, CNRS, LIP6, Institut Universitaire de France (Advisor)

Lattice-based cryptography is considered as a quantum-safe alternative for the replacement of currently deployed schemes based on RSA and discrete logarithm on prime fields or elliptic curves. It offers strong theoretical security guarantees, a large array of achievable primitives, and a competitive level of efficiency. Nowadays, in the context of the NIST post-quantum standardization process, future standards may ultimately be chosen and several new lattice-based schemes are high-profile candidates. The cryptographic research has been encouraged to analyze lattice-based cryptosystems, with a particular focus on practical aspects. This thesis is rooted in this effort. In addition to black-box cryptanalysis with classical computing resources, we investigate the extended security of these new lattice-based cryptosystems, employing a broad spectrum of attack models, e.g. quantum, misuse, timing or physical attacks. Accounting that these models have already been applied to a large variety of pre-quantum asymmetric and symmetric schemes before, we concentrate our efforts on leveraging and addressing the new features introduced by lattice structures. Our contribution is twofold: defensive, i.e. countermeasures for implementations of lattice-based schemes and offensive, i.e. cryptanalysis. On the defensive side, in view of the numerous recent timing and physical attacks, we wear our designer's hat and investigate algorithmic protections. We introduce some new algorithmic and mathematical tools to construct provable algorithmic countermeasures in order to systematically prevent all timing and physical attacks. We thus participate in the actual provable protection of the GLP, BLISS, qTesla and Falcon lattice-based signatures schemes. On the offensive side, we estimate the applicability and complexity of novel attacks leveraging the lack of perfect correctness introduced in certain lattice-based encryption schemes to improve their performance. We show that such a compromise may enable decryption failures attacks in a misuse or quantum model. We finally introduce an algorithmic cryptanalysis tool that assesses the security of the mathematical problem underlying lattice-based schemes when partial knowledge of the secret is available. The usefulness of this new framework is demonstrated with the improvement and automation of several known classical, decryption-failure, and side-channel attacks.

Jury:

• Martin Albrecht, Royal Holloway, University of London (examinateur)
• Pierre-Alain Fouque, Université de Rennes 1 (examinateur)
• Louis Goubin, Université de Versailles-Saint-Quentin-en-Yvelines (rapporteur)
• Helena Handschuh, Rambus, San Francisco (examinatrice)
• Daniele Micciancio, University of California, San Diego (examinateur)
• Damien Stehlé, École normale supérieure de Lyon (rapporteur)
• Michel F. Abdalla, École normale supérieure de Paris (directeur de thèse)
• Henri Gilbert, ANSSI, Paris (codirecteur de thèse)
• Sonia Belaïd, CryptoExperts, Paris (coencadrante, invitée)
• Ange Martinelli, Thales, ANSSI, Paris (coencadrant, invité)
• Thomas Prest, PQShield, Oxford (coencadrant, invité)
• Guénaël Renault, École polytechnique, Palaiseau (coencadrant, invité)

Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by dataflow synchronous languages like Lustre. In this thesis we present Vélus, a Lustre compiler verified in the interactive theorem prover Coq. We develop semantic models for the various languages in the compilation chain, and build on the verified CompCert C compiler to generate executable code and give an end-to-end correctness proof. The main challenge is to show semantic preservation between the dataflow paradigm and the imperative paradigm, and to reason about byte-level representations of program states. We treat, in particular, the modular reset construct, a primitive for resetting subsystems. This necessitates the design of suitable semantic models, compilation algorithms and corresponding correctness proofs. We introduce a novel intermediate language into the usual clock-directed modular compilation scheme of Lustre. This permits the implementation of compilation passes that generate better sequential code, and facilitates reasoning about the correctness of the successive transformations of the modular reset construct.

Jury:

• Gerwin Klein (Reporter), Data61/University of NSW
• Xavier Thirioux (Reporter), ISAE-SUPAERO
• Jean-Louis Colaço, ANSYS
• Emmanuel Ledinot, THALES Research & Technology
• Xavier Leroy, Collège de France
• Pascal Raymond, Université Grenoble-Alpes, CNRS, and VERIMAG
• Timothy Bourke (Supervisor), Inria and ENS
• Marc Pouzet (Supervisor), Sorbonne Université, ENS, and Inria

How do you synthesize ranking information into a single most representative global ranking? This can be modeled as an optimization problem. There are a few possibilities for the objective. Related to the feedback arc set problem in directed graphs, its theoretical formulation is difficult to solve exactly. We will show sinple heuristics and analyze them from the viewpoint of quality of approximation.

Computers are widely used in timing-sensitive applications such as controlling vehicles, factories, and medical devices. Today, real-time behavior of programs is a property that emerges from implementations rather than a property that is specified in models. Control over timing behavior of software is difficult to achieve, and timing behavior is neither predictable nor repeatable. I will argue that this problem can be solved by making a commitment to deterministic models that embrace temporal properties as an integral part of the modeling paradigm. I will explain how such models differ from the prevailing practice of modeling low-level computer architectures and estimating worst-case execution time. I will show moreover that deterministic timing is practical today without sacrificing performance for many useful workload models. Specifically, I will describe a class of computer architectures called PRET Machines that deliver deterministic timing with no loss of performance for a family of real-time problems consisting of sporadic event streams with hard deadlines.

Future information and communication networks will certainly consist of both classical and quantum devices, some of which are expected to be dishonest, with various degrees of functionality, ranging from simple routers to servers executing quantum algorithms. Most of the technology required to achieve advanced stages of a quantum internet is still in its infancy, hence it is very hard to predict the potential use cases. Several applications, however, have already been characterized depending on the different stages of a quantum network such as secure delegated quantum computing, quantum key distribution, clock synchronization, leader election, quantum digital signatures, quantum money among others. Such applications promise to impact and transform the society on multiple levels including communication, accessing information and security. Therefore, it would be extremely useful to have a standard framework to describe the protocols that are relevant to quantum internet such that they become available to the diverse quantum information science community. We take the first step in this direction and call such an initiative: The Quantum Protocol Zoo which consists of an organised collection of protocols that could be implemented (or simulated) in the coming years. In this lecture I present an overview of the filed through this new platform of interaction with various communities contributing to it.

Fault-tolerant distributed protocols play an important role in many critical/high-availability applications. The literature distinguishes two main classes: asynchronous vs. synchronous protocols, based on the semantics of the parallel composition. Asynchronous protocols are crucial parts of many distributed systems because networks are natively asynchronous and so these algorithms have better performance when compared against the synchronous ones. However, their correctness is very hard to obtain, due to the challenges of concurrency, faults (message loss or process crash), buffered message queues, and message re-ordering at the network. In contrast, reasoning about synchronous protocols is simpler, as they are structured in rounds and one only has to consider specific global states at round boundaries. Therefore, synchronous algorithms are less error prone and formal verification becomes tractable. The question we address in this talk is how to connect these worlds, such that we can take advantage of the more-understandable and verifiable synchronous protocols when reasoning about asynchronous protocols.

Models that can be turned into physical systems are usually called programs, while those that are obtained by studying a pre-existing system are usually called abstractions. Thus, programs and abstractions are classes of models that are distinguished by their lineage to systems: programs beget systems, while abstractions are derived from them. Modelling can therefore be defined as the art of inferring “well behaved” abstractions of systems, while programming is the activity of producing systems that are “well-behaved” with respect to their original model. Proving that programs are “sound” with respect to a system is the aim of the well established discipline of program verification. Interestingly, claiming that a system’s abstraction is valid is always relative to an abstraction barrier, and often a disputable statement in the context of evolved systems, for which no specification is at hand. In Biology, good abstractions are generally those that reproduce data well. It is therefore difficult to “prove” that an abstraction is correct because an infinite amount of tests would be needed to assert this. In this presentation we advocate the idea that a biological model should be considered correct when it has been provably obtained by integration of falsifiable data. In this context, we present an “executable knowledge representation” of biological mechanisms in the form of a graph rewriting language named Kappa. After a brief introduction to molecular biology, we will discuss expressiveness and algorithmic issues of graph rewriting techniques.

pour les normaliens en L3 d informatique ou L3 info et L3 maths en 2018-2019

Récemment, le domaine de la compression a vu de nouveaux développements survenir à la suite de l'introduction des systèmes numériques asymétriques (ANS) par J.Duda. Nous nous proposons de revisiter les concepts sous-jacents dans une version simplifiée de cette publication initiale. Ce sera l'occasion d'un tour d'horizon ludique du domaine de la compression, vue principalement du coté ingénierie: information, communication, codage, etc."

Verification activities are liable for about 70% of the overall effort in the development of critical avionics software. Considering the steady increase in size and complexity of this kind of software, classical V&V processes, based on massive testing campaigns and complementary intellectual reviews and analyses, no longer scale up within reasonable costs.

On the other hand, some formal verification techniques have been shown to cope with real-world industrial software, while improving automation. Such techniques have therefore been introduced into avionics verification processes, in order to replace or complement legacy methods.

We will show which formal methods are being used, and how industrial processes are being transformed to take advantage of them, i.e. improve industrial efficiency while maintaining the safety and reliability of avionics systems.

Tor is a way to access the Internet securely and privately.
It's a way to escape the everyday surveillance that companies and governments have been imposing to people. In this talk we are going to present Tor, as a software and as an organization, as well as give an overview of new features that have been in development lately.