Les équipes organisent leurs propres séminaires thématiques
Ce séminaire rassemble des exposés généraux conçus pour être accessibles à tous (élèves/étudiants, doctorants, chercheurs).
Une participation régulière pendant la scolarité à ENS (environ 24 séminaires) peut permettre d’obtenir 3 ECTS pour le diplôme de l’ENS.
L’élève/étudiant devra veiller que ses coordonnées soient bien inscrites sur la feuille de présence lors de chaque séminaire et demander la validation de ces ECTS lors de sa dernière année de scolarité.
La personne responsable est Marc Pouzet.
Les exposés ont lieu au 45, rue d'Ulm, 75005 Paris, en général "Salle Henri Cartan", et certains sont filmés et consultables sur : savoirs.ens.fr
Salle Jacques Louis Lions, Inria Paris
Salle Dussane
Salle Emmy Noether
Algorithmic systems and data processes are being deployed to aid a wide range of high-impact decisions. These systems can have momentous consequences for the people they affect but their internal behaviors are often incompletely communicated to stakeholders, leaving them frustrated and distrusting of the outcomes of the decisions. Transparency and accountability are critical prerequisites for building trust in the results of decisions and guaranteeing fair and equitable outcomes.
In this talk, I will present my work on making these opaque processes more transparent and accountable to the public in several real-world applications. I will examine how ranking aggregation functions traditionally used in decision systems inadequately reflect the intention of the decision-makers and present work on providing transparent metrics to clarify the ranking process. In addition, ranking functions that are used in resource allocation systems often produce disparate results because of bias in the underlying data, I will show how compensatory bonus points can transparently address disparate outcomes in ranking applications. Furthermore, real-world deployments of algorithmic decision-making solutions often run into implementation constraints that impact the guarantees of the underlying algorithms, I will discuss practical challenges associated with real-world deployments of algorithms.
Organizations do not have strong incentives to explain and clarify their decision processes; however, stakeholders are not powerless and can strategically combine their efforts to push for more transparency. I will discuss the results and lessons learned from such an effort: a parent-led crowdsourcing campaign to increase transparency in the New York City school admission process. This work highlights the need for oversight and AI governance to improve the trust of stakeholders who have no choice but to interact with automated decision systems.
Amélie Marian is an Associate Professor in the Computer Science Department at Rutgers University. Her research interests are in Explainable Rankings, Accountability of Decision-making Systems, Personal Digital Traces, and Data Integration. Her recent public scholarship work on explaining the NYC School Admission lottery process to families, in collaboration with elected parent representatives, was instrumental in increasing transparency and accountability in the NYC high school application system and received an award from the NYC Citywide Council on High Schools recognizing leadership and service on behalf of New York City Public School Families in April 2024. Amélie received her Ph.D. in Computer Science from Columbia University in 2005. She is the recipient of a Microsoft Live Labs Award, three Google Research Awards, and an NSF CAREER award. Transparency and Accountability in Data and Decision Processes.
Salle W
Lustre est un langage synchrone de type flot de données. Sa structure temporelle discrète et son système d'horloges lui permettent de garantir un temps d'exécution et une consommation de mémoire bornés statiquement, favorisant ainsi son adoption dans le domaine de systèmes critiques, notamment au sein de l'outil industriel Scade. Vélus, développé à l'Inria, est un compilateur Lustre vérifié. En s'appuyant sur la définition d'une sémantique formelle pour chaque langage intermédiaire, il apporte une preuve qu'un programme Lustre et sa traduction en Clight (langage pris en charge par CompCert) exhibent des comportements identiques.
Salle W
Cette thèse vise à développer des méthodes efficientes et mathématiquement rigoureuses afin d’améliorer la fiabilité des logiciels en utilisant l’interprétation abstraite, un cadre formel pour approximer les comportements des programmes. Nous développons un cadre quantitatif pour mesurer l’influence des variables d’entrée sur le comportement des programmes, aidant ainsi à certifier les comportements corrects et à identifier les défauts. Le cadre proposé est flexible, permettant différentes mesures d’impact et garantissant des résultats rigoureux, ce qui signifie que l’impact calculé sera toujours une surestimation ou une sous-estimation. Ce cadre est appliqué à la fois aux propriétés extensionnelles, qui mesurent le comportement entrée-sortie, et aux propriétés intentionnelles, qui évaluent des détails computationnels comme les itérations de boucles. Il a été implémenté dans trois outils : Impatto, Libra et TimeSec. Ces outils ciblent respectivement la fiabilité générale des logiciels, l’équité dans les réseaux de neurones et les vulnérabilités de canaux auxiliaires. Les évaluations expérimentales ont validé ces outils, démontrant leur efficacité dans divers cas d’utilisation, tels que la détection de biais dans les réseaux de neurones et les vulnérabilités dans les bibliothèques cryptographiques. Dans l’ensemble, ce travail améliore la compréhension de l’utilisation des données d’entrée dans les logiciels, offrant à la fois des perspectives théoriques et des outils pratiques pour améliorer la fiabilité et la sécurité des systèmes.
Amphi Dussane
Salle Emmy Noether
Salle W
Sparsification refers to the process of reducing the size or the density of a combinatorial object while preserving certain properties. Within the study of graph algorithms, for instance, sparsification involves, given a large and dense graph, finding a smaller, sparse graph that approximately preserves certain properties of the original graph, such as connectivity, pairwise distances, or maximum matching size. This technique is mainly motivated by the reduction of the memory requirement and by the computational speed-up obtained using the sparsified object rather than the dense one. These advantages become crucial when it comes to large-scale problems.
In this thesis we show that some sparsification techniques for graph problems can be applied to more general settings, with a focus on the maximum matching and the maximum constrained vertex cover problems. Moreover, we provide some applications of these techniques to streaming, communication complexity, and fixed-parameter algorithms.
In the first chapters, we leverage some graph-specific ideas to extend existing techniques. The first example we give is that of a sparsifier initially developed for the maximum cardinality matching which we extend to the more general weighted b-matching. Next, we generalize a kernel construction, initially developed for the cardinality-constrained maximum vertex cover problem, to the matroid-constrained version of that problem, for some matroids that can be represented by a simple graph. The latter chapters of this thesis delve into more general matroid-related problems and are built around the concept of density in a matroid. In particular, based on density in matroids, we adapt the aforementioned maximum matching sparsifier to tackle matroid intersection, a generalization of bipartite matching. Finally, we come back to the matroid-constrained maximum coverage problem and provide a sparsification technique that works for any kind of matroid.
Salle Simone Weil
Les fournisseurs de services ont de plus en plus numérisé les biens qu'ils mettent à disposition des utilisateurs, que ce soit dans le domaine de la monétique, de l'identification ou des transports, entre autres. La conséquence directe est une forte concentration des contenus sensibles sur les appareils personnels, qu'il s'agisse de données ou d'exécutables, à la fois pour la vie privée et professionnelle.
Ces systèmes dits sur étagère sont en grande partie sous le contrôle des utilisateurs finaux. Les acteurs industriels et étatiques à la recherche d'environnements stables et de confiance rencontrent de nombreux défis lorsqu'ils cherchent à y déployer des solutions, puisqu'ils ne peuvent pas nécessairement exploiter les mécanismes de sécurité matériels, s'il y en a. Certains s'orientent alors vers des implémentations visant le modèle de sécurité en boîte blanche impliquant que toutes les opérations puissent se dérouler à la vue de tous, ou alors se reposent sur les garanties logicielles fournies par le système d'exploitation.
Dans cette thèse, nous montrons d'abord comment le cryptosystème de McEliece, un algorithme cryptographique asymétrique robuste dans un contexte post-quantique, peut-être attaqué via l'injection de fautes pour aider à outrepasser des techniques d'obfuscation. Deuxièmement, nous inspectons comment le système Android gère l'énergie des plateformes embarquées basées sur lui, et démontrons le risque d'espionnage d'entrée de code PIN grâce à l'indulgence de la politique de sécurité par défaut. Enfin nous proposons une refonte des rapports de force dans les systèmes embarqués sur étagère, en faveur de leurs utilisateurs et propriétaires.
Amphi Galois
Le but de cette thèse est la vérification d'ordonnanceurs de tâches de systèmes d'exploitation par analyse statique basée sur l'interprétation abstraite. Les systèmes d'exploitation sont des ensembles de logiciels présents sur presque tout ordinateur. Leur but est de permettre aux autres programmes de s'exécuter sans avoir à gérer des spécificités bas niveau comme la mémoire. En conséquence de ce rôle central, les systèmes sont devenus des composants critiques des infrastructures informatiques : toute erreur au niveau du système d'exploitation peut avoir des conséquences sur les autres programmes allant jusqu'au plantage de l'ordinateur.
Un des composants au cœur d'un système d'exploitation est l'ordonnanceur de tâches. Ce dernier est chargé de déterminer quelle tâche peut s'exécuter à quel moment, en suivant une politique préétablie. Les ordonnanceurs de tâches utilisent des structures de données dynamiques non bornées afin de stocker les éléments nécessaires à leur fonctionnement. Ces structures de données permettent de déplacer facilement les éléments d'une structure vers l'autre. Par conséquent, la vérification d'un ordonnanceur de tâche nécessite de concevoir une analyse capable de représenter correctement ces structures de données et leur contenu.
La première partie de cette thèse décrit un langage impératif jouet semblable au C manipulant explicitement la mémoire. On donne ensuite la sémantique concret de ce langage, puis on présente une analyse statique numérique afin de déterminer la plage de valeur des variables ainsi qu'une analyse de forme capable de raisonner sur des structures de données inductives non bornées.
La seconde partie est consacrée à la présentation d'un domaine abstrait relationnel capable de raisonner sur des séquences symboliques. Ce domaine exprime des contraintes sur le contenu de ces séquences comme leurs longueurs, leurs valeurs extrémales et leurs caractères triés.
La troisième partie présente la combinaison de l'analyse de forme présentée dans la première partie avec le domaine de séquences. Cette combinaison augmente l'expressivité de l'analyse. Cette dernière est maintenant capable de prouver la correction fonctionnelle partielle d'algorithmes complexes comme des algorithmes de tris sur les listes ou les arbres binaires, ainsi que sur des bibliothèques de listes provenant d'applications réelles.
La dernière partie de cette thèse présente le travail d'application de l'analyse sur une instance de l'ordonnanceur de tâches de FreeRTOS. La première étape de la vérification est la formalisation des propriétés que nous cherchons à établir sur les fonctions de l'ordonnanceur. Cela inclut les invariants globaux de l'ordonnanceur. La seconde étape concerne le travail de validation pour montrer que ces propriétés spécifiées sont vérifiées par les fonctions de l'instance au moyen de l'analyse.
Amphi Jaurès, 29 rue d'Ulm
This thesis examines the extraction of mathematical statements and proofs from scholarly PDF articles by approaching it as a multimodal classification challenge. It is part of the broader TheoremKB project, which seeks to convert scientific literature into a comprehensive, open-access knowledge base of mathematical statements and their proofs. The research leverages a range of techniques from traditional machine learning to advanced deep learning architectures, including LSTMs, CNNs, Object detectors, CRFs, transformers, etc.
The study utilizes a novel combination of text, font characteristics, and bitmap images from PDF pages as separate input modalities. It proposes a modular, sequential, multimodal machine learning strategy incorporating a cross-modal attention mechanism to produce multimodal paragraph embeddings. These embeddings are processed through a novel multimodal sliding window transformer architecture that captures sequential data across paragraphs. This innovative approach does not rely on Optical Character Recognition (OCR) preprocessing, LaTeX sources during inference or custom pre-training on specialized losses, making it adept at handling multi-page documents and page breaks, typically in complex scientific, mathematical texts.
The findings indicate a marked performance improvement when moving from unimodal to multimodal processing and integrating sequential paragraph modelling, underscoring the effectiveness of the proposed method for handling intricate scholarly documents.
Salles des conférences - 46 rue d'Ulm (Visio)
This presentation summarizes one part of my research, with focus on the decision and control in networks with stochastic demand and supply. Two different settings will be considered: stochastic matching systems and real-time balancing of stochastic demand and supply in power grids. The objective is similar, yet the models differ considerably and use techniques from various fields, including queueing systems and network flows from graph theory for stochastic matching, and mean-field approximations and stochastic control for real-time demand-supply balancing.
Salle des Actes - ENS - 45, rue d'Ulm
Les constructions avancées de chiffrement à clés publiques élargissent les horizons d'utilisation de primitives cryptographiques, permettant entre autres la réalisation de calculs sur des données inconnues cachées dans des chiffrés, ou d'étendre des fonctionnalités de chiffrement à des systèmes comprenant de nombreuses personnes de manière efficace. De plus, lorsque les entités prenant part à un protocole cryptographique ne sont pas systématiquement synchrones ou disponibles en même temps, l'élaboration de techniques non-interactives devient plus avantageuse ; en outre, lors d'un déploiement pour une grande communauté, l'évitement d'une solution avec une entité centrale, en plus de ne pas nécessiter sa disponibilité constante, diminue son pouvoir au sein du système.
Ces fonctionnalités de pointe amènent des problématiques spécifiques ; ainsi, si un calcul combinant des informations confidentielles issues de sources distinctes est permis, l'étendue des opérations réalisables devra être surveillée attentivement afin d'éviter que celles-ci ne provoquent de trop grosses fuites sur les données en jeu.
À l'avenant, le chiffrement au sein d'une grande communauté, sans interactions avec une entité centrale, soulève des problématiques d'efficacité, à là fois pour atteindre des sous-ensembles de personnes, ou pour leur envoyer des messages individuellement, et d'autant plus dans des cas où celles-ci généreraient leurs propres clés secrètes sans les divulguer à une autorité.
Cette thèse apportera des réponses aux questions évoquées ci-avant dans des contextes de calculs ou d'utilisations particulières. Dans une première partie, deux contributions permettront d'accéder à des modèles de sécurité plus réalistes que dans l'état de l'art précédent, pour des types de calculs restreints.
Ensuite, deux autres permettront de rendre utilisables en pratique des protocoles de chiffrement au sein de grandes structures, avec des tailles et temps de calculs effectifs efficaces, au sein de modèles de sécurité conformes aux exigences actuelles.
Advanced Public-Key Encryption schemes broaden the usability of cryptographic primitives, granting for instance primitives to obliviously perform operations on hidden data, and to scale schemes up for applications in large organizations. In contexts in which users are not necessarily synchronized nor always available, developing non-interactive schemes becomes the most attractive solution; moreover, avoiding interactions with a central server in large sets of users also brings the benefit of weakening such an entity's power.
Several challenges arise with these cutting-edge features: when allowing the combination of private data from several sources to be decrypted, the class of authorized computations should be carefully monitored, as when the scheme or security model are too lenient, the confidential information issued from a source can be uncovered.
When scaling encryption schemes for a usage among a large community, the question emerging most naturally is the one of efficiency, both in the case where messages should be issued to subsets of members, or to individual ones, while avoiding interactions with a central server, and potentially reducing its capabilities when it is necessary during a setup phase.
This thesis endeavors to overcome these obstacles, for specific types of computations or communication patterns among many participants.
First, two contributions will show constructions improving on current security models, making them suitable for realistic applications, in the case of two specific types of calculations. Then, another two will grant schemes for efficient encryption in large groups of users (without relying on a central server), with convenient effective sizes and computation times, and up-to-date security models with respect to the latest expectations in the state-of-the-art.
Amphithéâtre Dussane, ENS, 45 rue d'Ulm
This thesis is the culmination of research conducted between 2019 and 2023. It is divided into three parts. In the first part, we explore algorithms related to the Covid-19 pandemic, such as Pool Testing, a well-established technique where samples from multiple patients are pooled for collective testing, allowing for cost reduction and time savings. We propose algorithms taking into account the a priori probabilities that individual tests are positive, which can be evaluated during a prior clinical examination of the patient. We also examine Pool Test- ing in emergency situations, where certain samples need to be analyzed according to some prescribed priority order. In both cases, we propose new algorithms and analyze them in detail. This section also deals with DNA privacy preservation in Covid-19 tests. In the second part, we present our results in experimental mathematics, where we have discovered several new conjectures on continued fractions through automated exploration. All those conjectures have been numerically tested to assess their plausibility. Finally, the third part of this the- sis is devoted to various results in the field of computer security, such as a previously unknown attack on the Mathematica software, a new protection mechanism against counterfeit medication, and a new observation on zero-knowledge proofs.
Salle de conférence du Centre Sciences des Données - ENS - 45, rue d'Ulm
Cette thèse étudie la génération de séries temporelles en construisant des modèles de pro- cessus stationnaires avec des dépendances longues portés. Nous nous concentrons sur la génération de signaux audio qui contiennent des attaques, des structures harmoniques, de l’intermittence et des enveloppes asymétriques. Ce sont des propriétés typiques de réalisations de processus non gaussiens qu’il nous faut modéliser. À partir d’une observa- tion, nous définissons un processus d’entropie maximale contraint par les moments d’une représentation non-linéaire. Nous devons n’utiliser qu’un petit nombre de moments afin de les estimer avec peu de données. Nous utilisons une transformée en ondelettes qui sépare les variations du signal sur plusieurs échelles dans des canaux différents. L’enjeu principal est de définir une représentation dont les moments capturent les dépendances à travers les échelles. Des travaux antérieurs ont utilisé la covariance entre les modules de coefficients d’ondelettes. Cependant, la phase contient des informations importantes qu’il ne faut pas éliminer, nous définissons pour cela les représentations en Harmoniques de Phase. Leur covariance capture l’alignement des phases à travers les échelles. Afin de définir un modèle de basse dimension, nous identifions deux harmoniques de phases suffisantes pour décrire l’intermittence et l’asymétrie du signal. En les combinant à une quasi-diagonalisation de la matrice de corrélation des modules de coefficients d’ondelettes, nous définissons les Covariances de Scattering avec phase. Le modèle résultant de cette analyse génère des signaux audio perceptuellement semblables aux originaux, avec des impacts, des structures harmoniques et des enveloppes asymétriques. Afin d’éviter la sélection de coefficients im- pliquée dans l’approche précédente, nous considérons des caractéristiques aléatoires pour connecter les échelles. Nous prouvons qu’elles approximent un modèle d’entropie maximale avec des contraintes déterministes. Des travaux antérieurs ont défini des modèles basés sur la matrice de Graam de caractéristiques aléatoires. Nous montrons que cette contrainte peut être remplacée par les activations moyennes d’un réseau plus profond, ce qui réduit la dimension. Il en résulte une représentation calculée avec une cascade d’ondelettes et de caractéristiques aléatoires appelée la Rainbow Scattering. Enfin, nous montrons qu’il est possible d’exploiter l’invariance à l’action d’un groupe dans le cadre de la rainbow scattering.
This thesis studies time-series generation by building models for stationary processes with long-range dependencies. We concentrate on the generation of audio signals which include sharp impacts, harmonic patterns, intermittency and asymmetric envelopes. These are typical behaviours of realizations of non-Gaussian processes that we must capture. From an observed signal, we define a maximum entropy model constrained by the moments of a non-linear representation. We need to use a small number of moments to estimate them from a small number of samples. We use a wavelet transform, which separates the signal’s variations over multiple scales into different channels. The main difficulty is to design a representation whose moments efficiently capture dependencies across scales. Prior works have used the covariance of wavelet modulus coefficients. However, phase con- veys important information which should not be discarded, for this purpose we introduce Phase Harmonics representations. Their covariance captures the alignment of phases be- tween scales. To define a low-dimensional model, we identify two phase harmonics which are sufficient to describe intermittency and asymmetry in the signal. Combined with a quasi-diagonalization of the wavelet modulus correlation matrix, we define Scattering Co- variances with phase. The resulting model generates audio samples perceptually similar to the original with sharp impacts, harmonic structures and asymmetric envelopes. To avoid the coefficient selection involved in the previous approach, we consider random fea- tures to connect scales. We prove that they approximate a maximum entropy model with deterministic constraints. Previous work have defined models based on the Graam matrix of random features. We show that this constraint can be replaced by the mean of a deeper random feature network, which has a lower dimension. It results into a representation calculated with a cascade of wavelets and random features called the Rainbow Scattering. Finally, we show that invariance to group actions can be enforced within this rainbow scattering.
Salle Favard (46, rue d'Ulm) / Pot dans la cafétéria du dpt de bio.
Salle W - 45, rue d'Ulm, Paris, 75005
Dans cette thèse, nous étudions différentes méthodes permettant de faire des calculs sur de l’information cachée. Nous présentons de nouvelles constructions de protocoles, allant de l’amélioration des complexités de l’état de l’art à l’ajout de fonctionnalités. Nous analysons également la sécurité d’autres protocoles, et présentons des attaques dessus. En premier lieu, nous nous intéressons au Private Simultaneous Messages, où un groupe d’individus souhaite faire apprendre à une entité externe le résultat d’un calcul sur leurs données privées. En utilisant un nouveau cadre, nous montrons de nouvelles constructions avec un coût en communication plus bas que celles déjà existantes. Ensuite, nous étudions des protocoles d’Oblivious RAM, qui dissimulent le motif d’accès qu’un client fait lorsqu’il accède à des données privées stockées sur un serveur non fiable. Nous présentons les premières constructions permettant au client d’enregistrer des objets de tailles arbitrairement différentes. Nous montrons également comment ces constructions permettent de construire des protocoles de Chiffrement Recherchable. Enfin, nous nous intéressons à la cryptographie en boîte-blanche, qui a pour objectif de donner à un appareil non fiable un accès sans restrictions à un algorithme de chiffrement, tout en empêchant la fuite de la clé secrète. Nous présentons une cryptanalyse de la construction de Ranea et al. de CRYPTO 2022, où des cryptosystèmes en boîte blanche sont donnés à partir de chiffrements symétriques basés sur des SPN et ARX. Nous prouvons que ce système n’est pas sûr en présentant une attaque structurelle de récupération de clé.
Salle Assia DJEBAR, 29 rue d’Ulm, Paris, 75005
Les paradigmes de modélisation pour la biologie des systèmes jouent un rôle important dans l’étude de la fonction orchestrée de divers systèmes biologiques. En outre, ils permettent d’étudier un système in-silico afin d’obtenir des informations mécanistiques à partir des trajectoires résultant du modèle. Un enjeu majeur pour dériver une représentation idéale pour un processus de système est de fixer le compromis descriptif entre entre la simplicité et la précision. D’une part, les modèles trop simples ont tendance à ne reproduire que les connaissances a priori. D’autre part, les modèles trop descriptifs donnent lieu à des comportements trop difficiles à analyser, voire à calculer. Dans les deux cas, l’acquisition de nouvelles connaissances est entravée. C’est pourquoi il est sans doute important, lors de la outils de mesurer l’impact de la sélection des modèles sur la capture des phénomènes biologiques, en particulier ceux qui peuvent être vérifiés.
Dans ce manuscrit, nous présentons un cadre formel pour dériver automatiquement des modèles discrets de systèmes biologiques à partir de réseaux de réactions stochastiques. Pour ce faire, nous utilisons des techniques offertes par Abstract d’interprétation pour évaluer les comportements résultant des modèles logiques, un outil de modélisation populaire en biologie des systèmes. Malgré le succès des modèles logiques pour résumer les observations expérimentales et prédire les propriétés locales du système, leurs hypothèses de modélisation sous-jacentes restent souvent implicites. Au lieu de cela, les modèles à gros grains que nous obtenons traitent de tous les comportements de la sémantique stochastique des réseaux de réaction initiaux, qui est explicitement définie. Plus précisément, l’espace d’état du réactionnel est divisé en régions abstraites et les transitions non déterministes entre les régions abstraites sont dérivées de manière conservatrice. En outre, nous récupérons les probabilités de transitions du réseau réactionnel de référence, de sorte que les limites du réseau réactionnel non déterministe sont calculées de manière conservatrice. Il est important de souligner que nous pouvons utiliser ce cadre pour évaluer, par le biais du modèle formellement dérivé, les comportements du modèle logique qui l’accompagne. En d’autres termes, le travail établi dans cette thèse ouvre une voie pour évaluer les modèles qui sont naturellement discrets, tout en ouvrant la voie à l’établissement de techniques de réduction de modèles plus efficaces pour les systèmes de réaction.
Salle Jaurès - 29, rue d'Ulm - Paris 5e
The simplicity of strings and their impactful usage puts their processing at the heart of many applications, including Bioinformatics, Information Retrieval, and Cybersecurity. Exact pattern matching has been extensively studied as the most natural problem, however, many applications also need more complex queries. Additionally, in all those application fields, the quantity of information to process has been increasing at such a staggering rate, that obtaining scalable algorithms is difficult. In this thesis, we contribute multiple space- and time-efficient algorithms for various string problems, by relying on sketches: compressions (lossless or lossy) that only keep the essential characteristic of the input needed to answer a given query.
In the first part of this thesis, we study complex queries such as regular expressions search, gapped consecutive matching, and square detection. For regular expression search, we provide a space-efficient algorithm in the streaming model: characters of the text arrive one at a time, and we can only access past characters if we explicitly store them. Next, gapped consecutive matching is a simpler type of query where, given two patterns P1, P2 and a range [a, b], one must report all consecutive occurrences of P1 followed by P2 separated by a distance in [a, b]. We study this problem in two settings: compressed indexing and pattern matching on a compressed text. Motivated by the importance of periodicity detection, next, we investigate square detection for general alphabets (the most abstract setting where squares can be defined). We give an optimal algorithm which answers an open question asked by Main and Lorentz in 1984.
The second part of this thesis proposes several ways to use approximation toward scaling up to large amounts of data in diverse applications including Bioinformatics. We first study approximate matching, where we must report all occurrences at distance at most k for a given similarity measure. We provide efficient parametrized algorithms for computing the length of the longest common substring with approximately k mismatches and to compute all positions of a text where a pattern occurs with dynamic time warping distance at most k. Finally, we propose a compressed index for redundant collections of next-generation sequencing reads, which takes advantage of alignments to an assembled genome to improve the overall compression but can incur false positive occurrences.
Salle W
In this thesis, we propose efficient constructions of cryptographic primitives with advanced functionalities. We focus on primitives that enable privacy-preserving applications, such as encrypted search or electronic voting, with provable security in the random oracle model (ROM). In particular, we construct searchable symmetric encryption (SSE) and blind signature schemes. SSE allows a client to perform keyword queries on an encrypted database stored on a distant server. To obtain the result, the server often performs a large number of random memory accesses. In consequence, the memory throughput of an SSE scheme is often the main bottleneck. For our constructions, we first propose variants of classical hashing schemes that allow for allocation of weighted items. Based on these variants, we construct several SSE schemes with good memory efficiency on modern storage media. This includes Pluto, a static SSE scheme with optimal memory efficiency, and Hermes, a dynamic SSE scheme with sublogarithmic memory efficiency and forward security. Blind signatures serve as a foundational tool for privacy-preserving applications (e.g., electronic voting, privacy-authentication tokens, blockchains). We present two optimized frameworks to construct blind signatures in the ROM. We instantiate each framework in the pairing setting and obtain efficient round-optimal blind signatures under standard assumptions. The first construction is a highly optimized variant of the generic blind signature construction by Fischlin (CRYPTO’06). Our second construction is a semi-generic construction from a specific class of randomizable signature schemes that admits an all-but-one reduction.
Salle des Actes - ENS
Salle Favard (ENS - 46, rue d'Ulm - 75005 Paris)
Les processus multi-échelles, qui présentent des variations sur une large gamme d'échelles, sont présents en physique, finance, biologie, médecine et de nombreux autres domaines. L'objectif principal de cette thèse est de construire des modèles probabilistes de tels processus observés à partir de peu de données et pouvant être échantillonnés numériquement. Ce sujet est crucial pour aborder plusieurs problèmes, notamment la génération, la prédiction et les problèmes inverses tels que la séparation de sources.
Dans cette thèse, nous introduisons les spectres en Scattering («Scattering Spectra»), qui sont basés sur une approximation diagonale de corrélations non linéaires de coefficients d'ondelettes. Ils peuvent être utilisés pour construire des modèles non-Gaussiens de processus multi-échelles, qu'il s'agisse de processus temporels, de processus temporels multi-canaux ou de processus d'image. Nous montrons qu'ils reproduisent des propriétés statistiques importantes de séries temporelles financières, de jets turbulents et de champs physiques.
Nous démontrons que cette représentation en «Scattering Spectra» peut être utilisée pour la séparation de sources à partir de peu de données. Appliquée aux données sismiques sur Mars, ils permettent de séparer avec succès les tremblements de Mars d’événements polluants transitoires appelés «Glitches».
La prédiction sur données limitées peut être abordée en utilisant un modèle précis du processus capable de capturer les dépendances à long terme. Nous introduisons le «Path-Shadowing Monte-Carlo» qui est une méthode à noyau non-locale qui propose de moyenner les quantités futures sur des chemins générés dont l'histoire passée est «proche» de l'histoire réelle (observée). Associée à un modèle basé sur les «Scattering Spectra», cette approche permet d'obtenir des résultats à l'état de l'art pour la prédiction de volatilité en finance et fournit des smiles d'option qui surpassent le marché dans un jeu de trading.
Salle W
Afin de parer à la menace que représenterait l’essor des calculateurs quantiques sur nombre de systèmes cryptographiques — et non des moindres — en usage actuellement, d’importants efforts sont faits pour que voient le jour et se développent des systèmes dits « post-quantiques » de chiffrement, d’authentification et d’identification, analogues aux systèmes classiques mais qui résisteraient à des attaques rendues possibles par de tels calculateurs, y compris si ces derniers venaient à devenir particulièrement puissants.
C’est avec l’intention de m’associer à ces efforts que je me suis penché sur les systèmes d’accréditations anonymes. Ces systèmes permettent à un fournisseur de services de vérifier les droits d’un utilisateur à bénéficier de ces services en vertu de la garantie — donnée antérieurement par une autorité de confiance — du fait que cet utilisateur possède bien les attributs requis, cela en préservant le secret des autres attributs, tels que l’identité de l’utilisateur, dont l’autorité aurait eu à prendre connaissance, et cela en permettant la levée de l’anonymat de l’utilisateur par un autre agent, disposant d’une clef secrète spéciale. Je me suis employé à étudier les systèmes d’accréditations anonymes décrits dans la littérature et j’ai participé à l’élaboration d’un schéma théorique d’accréditations anonymes post-quantiques optimisé, fondé sur les problèmes difficiles relatifs aux réseaux euclidiens, pour ensuite contribuer au développement du premier programme informatique à sources ouvertes d’accréditations anonymes post-quantiques qui soit une démonstration directe de la compatibilité d’un tel schéma avec des cas d’usages concrets. Le protocole Signal, sur lequel se fondent de nombreux systèmes de messagerie instantanée actuels, est lui aussi appelé à connaître une adaptation post-quantique. Dans un article, nous en proposons une vérification formelle réalisée avec le prouveur Tamarin en mettant l’accent sur ses deux principales composantes, le protocole d’échange de clefs X3DH et le protocole du « double cliquet » de mise à jour des clefs de session.
Salle W
Les réseaux de neurones convolutifs profonds ont obtenu un succès considérable en vision par ordinateur, à la fois pour de l'apprentissage non-supervisé (i.e., génération d'image) et de l'apprentissage supervisé (i.e., classification d'image). Cependant, les principes fondamentaux qui expliquent ces résultats impressionnants ne sont pas bien compris. En particulier, l'apprentissage profond semble échapper à la malédiction de la dimensionalité, ce qui révèle une structure mathématique riche dans les problèmes d'apprentissage rencontrés en pratique. Cette structure est présente dans les interactions entre les données d'entraînement (sur quelles propriétés se repose-t-on implicitement ?), l'architecture (quel est le rôle fonctionnel rempli par ses composants ?) et l'algorithme d'optimisation (qu'est-ce que le réseau a appris ?). Cette thèse comporte des résultats sur ces trois questions. Premièrement, nous montrons qu'une factorisation multi-échelles des distributions d'images peut révéler des propriétés de régularité, des structures de dépendances markoviennes locales, et même de la log-concavité conditionnelle, alors que la distribution globale ne possède pas ces propriétés. Cela conduit à des algorithmes efficaces d'apprentissage et d'échantillonnage dont on peut contrôler toutes les sources d'erreurs. Deuxièmement, nous étudions le rôle de la non-linéarité en classification d'images, et montrons que sa fonction principale est de collapser la phase complexe des coefficients d'ondelettes des activations du réseau. En revanche, des modèles précédents reposant sur des seuillages et des hypothèses de parcimonie ne sont ni suffisants ni nécessaires pour expliquer la précision de classification des réseaux profonds. Troisièmement, nous introduisons un modèle probabiliste des poids appris dans les architecture profondes, en capturant les dépendances entre couches par un alignement des activations du réseau sur une représentation déterministe associée à un noyau reproduisant. Le modèle est spécifié à travers des distributions à chaque couche, dont les covariances sont de bas rang et réalisent une réduction de dimensionalité entre les plongements en haute dimension calculés par la non-linéarité. Dans certains cas, ces distributions sont approximativement gaussiennes, et les covariances capturent la performance et la dynamique d'entraînement du réseau.
Deep convolutional neural networks have achieved considerable success in computer vision tasks, both in unsupervised learning (e.g., image generation) and supervised learning (e.g., image classification). However, the fundamental principles behind these impressive results remain not well understood. In particular, deep learning seemingly escapes the curse of dimensionality in practice, which evidences a rich mathematical structure underlying real-world learning problems. This structure is revealed by the interplay between the training data (what properties are we implicitly relying on?), the architecture (what is the functional role of network computations?), and the optimization algorithm (what has the network learned?). This thesis presents results on these three questions. First, we demonstrate that a multiscale factorization of image distributions can reveal properties of smoothness, local Markov dependency structure, and even conditional log-concavity, whereas the global distribution does not enjoy these properties. It leads to efficient learning and sampling algorithms where all sources of errors can be controlled. Second, we investigate the role of non-linearity in image classification, and show that its main function is to collapse the phase of complex wavelet coefficients of network activations. In contrast, previous models based on thresholding and sparsity assumptions are neither sufficient nor necessary to explain the classification accuracy of deep networks. Third, we introduce a probabilistic model of learned weights in deep architectures, with layer dependencies that are captured by alignment of the network activations to deterministic kernel embeddings. The model is specified through weight distributions at each layer, whose covariances are low-rank and perform dimensionality reduction in-between the high-dimensional embedding computed by the non-linearity. In some cases, these weight distributions are approximately Gaussian, and the covariances capture the performance and training dynamics of the network.
Amphithéâtre Evariste Galois
Le nombre d’appareils connectés par personne a massivement augmenté lors de la dernière décennie, en particulier dans les pays occidentaux. Étant donné que la sécurité des structures connectées au réseau peut être compromise à partir de n’importe quel point d’entrée par un attaquant malveillant, la sécurisation des trousseaux de clefs cryptographiques des utilisateurs devient centrale pour construire une infrastructure sécurisée. Afin d’explorer les réponses à cette problématique, nous proposons des solutions pour que les utilisateurs puissent gérer des appareils multiples. En particulier, nous nous penchons sur les pratiques cryptographiques qui sont compatibles avec les méthodologies modernes de contrôle d’accès basées sur des attributs. Ces pratiques doivent aussi intégrer les outils qui sont au cœur de la gestion d’appareils multiples par des utilisateurs. Le premier de ces outils est la délégation, qui permet aux utilisateurs de délimiter les capacités de déchiffrement de chacun de leurs appareils en fonction de leurs besoins. La délégation doit être possible sans nécessiter d’interaction avec une quelconque autorité, afin de préserver la vie privée et l’autonomie de l’utilisateur. Le second outil est le traçage, où nous exigeons que les appareils des utilisateurs puissent être identifiés en cas d’abus ou d’utilisation illégitime, afin que tout utilisateur puisse être tenu responsable de la gestion de ses appareils.
Nous commençons par présenter une approche pratique des Dual Pairing Vector Spaces (DPVS), qui est un système de construction et de preuves qui permet d’assurer le meilleur niveau de sécurité pour la cryptographie basée sur les attributs. Le DPVS est compatible avec des caractéristiques importantes de cette cryptographie telles que la richesse de l’expression des politiques de contrôle d’accès. Ensuite, nous présentons une nouvelle contribution pour le chiffrement basé sur les attributs sous la forme d’une nouvelle primitive : le Switchable-Attribute Key-Policy Attribute-Based Encryption (SA-KP-ABE). Dans un SA-KP-ABE, les attributs des utilisateurs et des chiffrés peuvent être "activés/désactivés" d’une manière indistinguable pour les utilisateurs. Nous prouvons que cette approche permet le traçage et qu’elle est compatible avec la délégation. Nous fournissons également une construction de SA-KP-ABE avec le DPVS. Notre dernière contribution est un schéma de signature basée sur des attributs qui permet deux méthodes de délégation. La première est la délégation habituelle de clefs, et la seconde permet de déléguer des politiques d’accès pré-approuvées qui peuvent être réutilisées pour signer différents messages. L’une ou l’autre de ces deux méthodes peut être utilisée en fonction du risque liée à une mauvaise gestion ou de la compromission de l’appareil recevant les clefs déléguées, car la seconde méthode implique moins de dommages potentiels que la première. De plus, nous prouvons également que notre schéma est compatible avec le traçage de signatures, où une autorité désignée peut lever l’anonymat des signatures suspectes.
The last decade has seen a massive increase in the number of connected devices per person, especially in western countries. As the security of connected structures can be compromised from any entry point by a malicious attacker, securing sets of cryptographic keys of users becomes an important keystone to build secure infrastructure. To explore answers to this problem, we propose solutions oriented towards the management of multiple devices for each user. In particular, we consider cryptographic practices that are compatible with modern access-control methodologies based on attributes. These practices should be compatible with features that are central to management of multiple devices. The first is delegation, as a means for users to delimit the decryption capabilities of each of their devices depending on their needs. Delegation should be doable without requiring interaction with any sort of authority, in order to preserve the user’s intimacy and autonomy. The second is tracing, in the sense that we require that devices can be tracked in the case of abuse or illegitimate use so that any user can be held accountable.
We begin by presenting a practical approach to the Dual Pairing Vector Spaces (DPVS), a framework that allows for full security of attribute-based schemes, while being compatible with important features like expressive policies. Then, we present a new contribution for attribute- based encryption schemes in the form of a new primitive: Switchable-Attribute Key-Policy Attribute-Based Encryption (SA-KP-ABE). In a SA-KP-ABE, the attributes of users and cipher- texts can be "turned on/off" in a way that is indistinguishable for the users. We prove that this approach allows for tracing, and is fully compatible with delegation. We also provide a con- struction of SA-KP-ABE in the DPVS framework. Our last contribution is an attribute-based signature scheme that allows for two types of delegation. The first one is the usual delegation of keys, and the second one allows to delegate pre-approved policies that can be re-used to sign different messages. Either of these two approaches can be used depending on the risk of mismanagement or corruption of the device receiving the delegated keys, as the latter incurs less possible damage than the first one. Furthermore, we also prove our scheme to be compat- ible with tracing techniques, where a designated authority can lift the anonymity of suspicious signatures.
Salle Henri Cartan
Salle Henri Cartan
La cryptographie moderne a un ennemi de taille à l'horizon : la montée inévitable des ordinateurs quantiques. Cependant, cette même puissance de calcul permettrait également de trouver des solutions sur des tâches cryptographiques qui sont tout simplement impossibles à réaliser avec la technologie actuelle. Dans cette thèse, nous mettons les pieds dans un univers où le quantique est omniprésent en y présentant notamment deux principales contributions. Nous mettons en avant à la fois des nouveaux modèles et de nouvelles analyses de sécurité pour deux primitives cryptographiques : les chiffrements et les preuves à divulgation nulle de connaissance non interactives. Les définitions usuelles de sécurité de ces primitives requièrent intrinsèquement la capacité d'enregistrer et de comparer des chaînes classiques. Cependant, les tâches d'enregistrement et de comparaison sont extrêmement difficiles dans le monde quantique en raison du principe d'incertitude. Nous proposons deux alternatives afin de surmonter cette barrière. De plus, nos notions de sécurité sont les premières à prendre pleinement en compte les attaques quantiques dans lesquelles les attaquants peuvent interagir avec les utilisateurs finaux sur des canaux quantiques. D'autre part, nous montrons que la disponibilité des ordinateurs quantiques se révèle être également à l'avantage des cryptographes, même lorsque les utilisateurs finaux n'utilisent que des communications classiques. En particulier, nous présentons un protocole interactif entre une Alice classique et un Bob quantique. Ce dispositif permet à Alice d'envoyer un état quantique caché non clonable à Bob par des canaux classiques. En outre, cet état quantique non clonable établit une forte propriété dite de monogamie de l'intrication, qui décrit les limites de la force des corrélations multipartites quantiques. Enfin, nous appliquons notre protocole et nous donnons les premiers schémas semi-quantiques de protection contre la copie.
Modern cryptography has a major foe on the horizon: the inevitable rise of quantum computers. However, the same computing power will also unlock solutions to cryptographic tasks that are simply impossible to achieve with the current technology. This thesis sets foot in a ubiquitous quantum world, where everyone will be running quantum computers, with two main contributions. Firstly, we put forth new security models and security analyses for two cryptographic primitives: encryption and non-interactive zero-knowledge proofs. Classical security definitions of these primitives inherently require the ability to record and compare classical strings. However, the tasks of recording and comparing are highly non-trivial in the quantum setting, due to the quantum uncertainty principle. We propose two different ways to overcome this recording barrier. Our security notions are the first to fully capture quantum attacks in which the codebreakers can interact with the end-users over quantum channels. Secondly, we show that the availability of quantum computers turns out to be also the advantage of codemakers, even when the end-users only use classical communication. In particular, we exhibit an interactive protocol between a classical Alice and a quantum Bob which allows Alice to send a hidden unclonable quantum state to Bob through classical channels. Furthermore, the constructed unclonable quantum state establishes a strong monogamy-of-entanglement property, which describes the limitations on the strength of quantum multipartite correlations. We further apply our protocol to quantum copy-protection and give the first semi-quantum copy-protection schemes.
Salle CELAN
Résumé : De nos jours, la cryptographie fait partie intégrante de notre quotidien. Initialement destinée à être utilisée pour les interactions entre humains, elle est aujourd’hui employée pour les interactions avec et entre des machines. A travers cette thèse, nous présenterons nos diverses contributions couvrant une partie du spectre de la cryptographie interactive. Dans un premier temps, nous la verrons comme un outil au service de l’apprentissage automatique. Nous montrerons qu’elle peut permettre à un client et à un serveur d’interagir afin de faire évaluer les données du client par le modèle du serveur, sans qu’aucun d’eux n’apprenne d’informartion confidentielle au sujet de l’autre. Ensuite, nous étendrons la notion déjà existante de Smooth Projective Hash Functions pour la rendre plus compatible avec la cryptographie post-quantique, et notamment les réseaux euclidiens. Cette extension servira de base à la construction de Transferts Inconscients, largement déployés aujourd’hui dans le cadre de Calculs Multipartites Securisés. Finalement, nous nous intéresserons à la cryptographie à bas-coût, permettant à des appareils techniquement limités d’interagir entre eux tout en jouissant d’une sécurité suffisante. Plus précisément, nous étudierons la sécurité d’un protocole authentifié d’échange de clés optimisé pour de tels appareils, permettant d’établir une communication sécurisée entre eux.
Abstract: Nowadays, cryptography is an integral part of our daily lives. Originally intended to be used for human-to-human interactions, cryptography is now also used for with and between machines. In this thesis, we will present our contributions covering part of the spectrum of interactive cryptography. First, we will use cryptography as a tool for Machine Learning. We will show that a client and a server can securely interact such that the client gets his data evaluated by a model owned by the server, without learning any confidential information about the other party’s data. Next, we will extend the already existing primitive of Smooth Projective Hash Functions to make it more compliant with post-quantum cryptography, and in particular with lattices. This extension will be used as a basis for the construction of Oblivious Transfers, widely used in the Secure Multiparty Context. Finally, we will focus on lightweight cryptography, allowing technically limited devices to interact with each other while enjoying sufficient security. More precisely, we will perform a security analysis of an authenticated key exchange protocol optimized for such devices, allowing them to securely interact.
Salle du Centre Sciences des Données
Résumé : Les classificateurs convolutionnels profonds séparent linéairement les classes d'images avec une précision croissante à mesure que la profondeur augmente. Ces classes se concentrent progressivement autour de moyennes séparées, tandis que la variable spatiale est réduite et que le nombre de canaux augmente. Un problème fondamental de l'apprentissage profond réside dans la compréhension du rôle des non-linéarités ainsi que des filtres convolutionnels dans ces transformations. Dans cette thèse, nous abordons cette question en construisant des architectures profondes dont les modules reposent sur les principes de parcimonie et de collapse de phase. Ces principes permettent d'expliciter les mécanismes mathématiques conduisant aux phénomènes de séparation et de concentration observés dans les réseaux profonds, et de mettre en évidence le rôle des poids et des non-linéarités dans ce processus. Nous montrons que ces architectures structurées sont capables d'atteindre la précision de réseaux profonds de référence comme ResNet, mais avec moins de couches et sans biais. Une analyse comparative de réseaux qui itèrent des non-linéarités éliminant ou préservant la phase met également en évidence à la fois théoriquement et numériquement la préséance des premiers sur les seconds, offrant de nouvelles perspectives sur le rôle fonctionnel sous-jacent des ReLUs dans les réseaux profonds.
Abstract: Deep convolutional classifiers linearly separate image classes and improve accuracy as depth increases. They progressively concentrate classes around separated means, while reducing the spatial dimension and increasing the number of channels. A fundamental challenge in deep learning is to understand the role of non-linearities together with convolutional filters in those transformations. In this dissertation, we tackle this question by building deep architectures whose building blocks rely on sparsity and phase collapse principles. Those principles provide explicit mathematical mechanisms explaining the separation and concentration phenomenon observed in deep networks, while highlighting the role of weights and non-linearities in this process. We show that those principled architectures are able to reach the accuracy of most advanced deep baselines like ResNet, yet with fewer layers and no biases. A comparative analysis of networks iterating phase collapsing and phase preserving non-linearities also evidences both theoretically and numerically the precedence of the former on the latter, offering new perspectives on the underlying functional role of ReLUs in deep networks.
Salle Henri Cartan
ENS, salle Emmy Noether
Cette thèse étudie la malléabilité dans le contexte du chiffrement à clé publique et des signatures numériques, en présentant les avancées et les applications des technologies améliorant la confidentialité. La première partie aborde le problème de l'égalité générique des textes en clair et les preuves d'inégalité. Étant donné deux textes chiffrés générés par un schéma de chiffrement à clé publique, le problème de l'égalité des textes chiffrés consiste à déterminer si les textes chiffrés contiennent la même valeur. Parallèlement, le problème de l'inégalité du texte clair consiste à déterminer s'ils contiennent une valeur différente. Les travaux précédents se sont concentrés sur la construction de nouveaux schémas ou sur l'extension de schémas existants afin d'inclure le support de l'égalité/inégalité du texte en clair. Nous proposons des preuves génériques et simples à connaissance zéro pour les deux problèmes, qui peuvent être instanciées avec divers schémas de chiffrement. Pour ce faire, nous formalisons les notions liées à la malléabilité dans le contexte du chiffrement à clé publique et proposons un cadre de définition pour le chiffrement générique aléatoire, que nous utilisons pour construire nos protocoles. La partie suivante est consacrée aux signatures préservant la structure sur les classes d'équivalences, le principal élément constitutif des parties suivantes. Initialement, nous proposons des constructions nouvelles et plus efficaces sous des hypothèses standard. Ensuite, nous construisons un schéma d'accréditation établi sur les attributs sous des hypothèses standard, qui étend les travaux précédents de plusieurs façons. Nous améliorons notamment l'expressivité, les compromis d'efficacité et proposons une notion de dissimulation de l'émetteur qui permet aux détenteurs de lettres de créance de cacher l'identité de l'émetteur pendant les utilisations. La dernière partie est consacrée à la présentation de Protego, un nouveau schéma d'accréditation pour les blockchains à autorisation. Il s'appuie sur les contributions précédentes et bien qu'il soit discuté dans le contexte des blockchains à autorisation, il peut également être utilisé dans d'autres contextes. Pour démontrer l'aspect pratique de Protego, nous fournissons un prototype et des benchmarks montrant que Protego est plus de deux fois plus rapide que les approches de l'état de l'art basées sur Idemix, le schéma d'accréditation le plus largement utilisé pour les blockchains à autorisation.
This thesis studies malleability in the context of public-key encryption and digital signatures, presenting advances and applications to privacy-enhancing technologies. The first part addresses the problem of Generic Plaintext Equality and Inequality Proofs. Given two ciphertexts generated with a public-key encryption scheme, the problem of plaintext equality consists in determining whether the ciphertexts hold the same value. Similarly, the problem of plaintext inequality consists in deciding whether they hold different values. Previous work has focused on building new schemes or extending existing ones to include support for plaintext equality/inequality. We propose generic and simple zero-knowledge proofs for both problems, which can be instantiated with various encryption schemes. We do so by formalizing notions related to malleability in the context of public-key encryption and proposing a definitional framework for Generic Randomisable Encryption, which we use to build our protocols. The next part turns to Structure-Preserving Signatures on Equivalence Classes, the main building block of subsequent parts. First, we propose new and more efficient constructions under standard assumptions. Then, we build an anonymous attribute-based credential (ABC) scheme under standard assumptions, which extends previous work in several ways. We improve expressiveness, provide efficiency trade-offs and propose an issuer-hiding notion that allows credential holders to hide the issuer's identity during showings. The last part is devoted to presenting Protego, a new ABC scheme for permissioned blockchains. It builds upon the previous contributions, and although it is discussed in the context of permissioned blockchains, it can also be used in other settings. To show the practicality of Protego, we provide a prototype implementation and benchmarks showing that Protego is more than twice faster than state-of-the-art approaches based on Idemix, the most widely used ABC scheme for permissioned blockchains.
Salle Henri Cartan - ENS - Paris
Salle W – ENS Paris, 45 rue d'Ulm
Salle W – ENS Paris, 45 rue d'Ulm
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.
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.
Salle W – ENS Paris, 45 rue d'Ulm
Le Real-time Bidding (RTB) est un marché particulier de la publicité programmatique, dans lequel des créneaux publicitaires sont vendus aux enchères. Les acheteurs en RTB peuvent améliorer les performances de leurs campagnes en fixant un certain nombre de paramètres, comme l'offre qu'ils souhaitent soumettre ou le budget qu'ils souhaitent allouer à chaque subdivision de la campagne. Dans ce manuscrit, nous fournissons un cadre mathématique pour l'optimisation de tels paramètres, qui peut être considéré comme un cas particulier de bandit à bras continu. Tout d'abord, nous profitons de la structure des enchères au second prix et au premier prix pour concevoir des stratégies spécifiques pour fixer une offre dans ces deux types d'enchères, utilisées dans le RTB. Les enchères au second prix et au premier prix sont traitées séparément, car la propriété de sincérité de l'enchère au second prix permet des stratégies plus simples. Ensuite, nous nous attaquons à la tâche d'allocation du budget entre les subdivisions d'une campagne, en adaptant les algorithmes de recherche directe, courants en optimisation sans dérivée, aux problèmes d'optimisation bruités et linéairement contraints. Nous analysons tous les algorithmes proposés du point de vue du regret cumulatif, et nous commentons leur optimalité. Nous démontrons la performance de chaque algorithme en réalisant des expériences numériques.
Real-time Bidding (RTB) is a particular market for programmatic advertising, in which advertising slots are sold via auctions. Buyers in RTB can improve the performance of their campaigns by setting a number of parameters, like the bid that they wish to submit or the budget that they wish to allocate to each subdivision of the campaign. In this manuscript, we provide a mathematical framework for the optimization of such parameters, which may be seen as a special case of continuously-armed bandit models. First, we take advantage of the structure of second-price and first-price auctions to design specific strategies for setting a bid in these two types of auctions, used in RTB. Second-price and first-price auctions are treated separately, as the truthfulness property of second-price auction allows for simplified strategies. Then, we tackle the task of budget allocation across subdivisions of a campaign, by adapting direct search algorithms, common in derivative-free optimization, for noisy and linearly-constrained optimization problems. We analyze all the proposed algorithms from the perspective of cumulative regret, and comment on their optimality. We showcase the performance of each algorithm by performing numerical experiments.
Salle Henri Cartan
Salle Henri Cartan
Salle Henri Cartan
ENS
The vast majority of communication on the Internet and private networks heavily relies on Public-key infrastructure (PKI). One possible solution, to avoid complexities around PKI, is to use Password Authenticated Key-Exchange (PAKE) protocols.
PAKE protocols enable a secure communication link between the two parties who only share a low-entropy secret (password). PAKEs were introduced in the 1990s, and with the introduction of the first security models and security proofs in the early 2000s, it was clear that PAKEs have a potential for wide deployment - filling the gap where PKI falls short. PAKEs' PKI-free nature, resistance to phishing attacks and forward secrecy are just some of the properties that make them interesting and important to study. This dissertation includes three works on various aspects of PAKEs: an attack on an existing PAKE proposal, an application of PAKEs in login (for password leak detection) and authentication protocols (HoneyPAKEs), and a security analysis of J-PAKE protocol, that is used in practice, and its variants.
In our first work, we provide an empirical analysis on zkPAKE protocol proposed in 2015. Our findings show that zkPAKE is not safe against offline dictionary attacks, which is one of the basic security requirements of the PAKE protocols.
Further, we demonstrate an implementation of an efficient offline dictionary attack, which emphasizes, when proposing a new protocol, it is necessary to provide a rigorous security proof.
In our second contribution, we propose a combined security mechanism called HoneyPAKE. The HoneyPAKE construction aims to detect the loss of password files and ensures that PAKE intrinsically protects that password. This makes the PAKE part of the HoneyPAKE more resilient to server-compromise and pre-computation attacks which are a serious security threat in a client-server communication.
Our third contribution facilitates the wider adoption of PAKEs. In this work, we revisit J-PAKE and simplify it by removing a non-interactive zero knowledge proof from the last round of the protocol and derive a lighter and more efficient version called sJ-PAKE. Furthermore, we prove sJ-PAKE secure in the indistinguishability game-based model, the so-called Real-or-Random, also satisfying the notion of perfect forward secrecy.
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.
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.
Dans cette thèse, nous nous intéresserons à deux thématiques majeures : la sécurité des données dans des protocoles d'échange cryptographiques, ainsi que l'analyse et la sécurisation des structures de données. Pour cela, nous appliquons des analyses formelles, reposant autant sur des outils cryptographiques existants que des modélisations ad-hoc pour le problème envisagé. En premier lieu, nous étudierons la sécurité de détecteurs de doublons, ainsi qu'une optimisation de l'utilisation de l'espace de stockage disponible. Ensuite, nous nous tournerons sur un cas pratique de modélisation, proposant un nouveau modèle formel pour la blockchain. Enfin, nous nous pencherons sur la problématique d'externalisation de protocoles de bandit manchot. Nous verrons comment externaliser les calculs, tout en prouvant que les nœuds du réseau apprennent aussi peu d'information que possible.
In this thesis, we are interested in two major themes: data security in exchange protocols, and the analysis and securing of data structures. To do so, we apply formal analyses, based on existing cryptographic tools as well as ad-hoc modelling for the problem under consideration. Firstly, we will study the security of duplicate detectors, as well as an optimisation of the use of available storage space. Then, we will turn to a practical modelling case, proposing a new formal model for blockchain. Finally, we will study the problem of outsourcing bandit learning protocols. We will see how to outsource calculations, while proving that the network learns as little as possible.
Amphi Galois -- ENS, Paris
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.
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.
ENS, Paris
Avec l’utilisation massive du stockage dématérialisé, l’homomorphisme est devenu l’une des propriétés les plus largement employées en cryptologie. Dans cette thèse, nous allons étudier comment l’utiliser dans des protocoles multi-utilisateurs concrets qui nécessitent non seulement de la confidentialité, mais aussi de l’anonymat, de l’authentification ou encore de la vérifiabilité. Pour cela, nous utilisons des schémas homomorphes de chiffrement, de signature numérique et de preuves à divulgation nulle de connaissances, mais, à chaque fois, nous devrons limiter leurs capacités de malléabilité pour atteindre le niveau de sécurité préalablement défini. Tout d’abord, l’aspect confidentiel est abordé au travers de l’étude de calculs sur des bases de données externalisées. Être capable d’appliquer des fonctions sur des données chiffrées sans avoir à les télécharger pour les déchiffrer entièrement est permet de profiter de la puissance de calcul du serveur qui est généralement supérieure à celle du client. Cela peut être également indispensable lorsqu’une société sans droit d’accès à une base de données de clients souhaite obtenir le résultat d’un calcul. La quantité d’information apprise ne doit pas être supérieure à celle contenue dans le résultat du calcul. Nous proposons pour cela un schéma de chiffrement décentralisé qui permet d’évaluer des fonctions quadratiques sur les données externalisées tout en ayant un contrôle des opérations grâce à un groupe d’inspecteurs. Cependant, la confidentialité des données n’est pas toujours la propriété la plus recherchée pour un système car elle ne protège pas l’identité de l’expéditeur. Pour le vote électronique, chaque bulletin chiffré doit être associé à un électeur afin de vérifier que celui-ci était autorisé à voter, mais après la phase de vote, l’anonymat doit être assuré. Pour cela une solution est de mélanger plusieurs fois l’urne de sorte que, au moment du dépouillement, qui correspond au déchiffrement, aucun lien entre le vote et l’électeur ne puisse être fait. C’est le fonctionnement d’un réseau de serveurs-mélangeurs dont nous proposons une nouvelle construction basée sur des signatures linéairement homomorphes avec un coût de vérification de l’urne finale indépendant du nombre de mélanges. Ce protocole est donc d’autant plus efficace que le nombre de mélanges augmente et représente un progrès par rapport aux constructions déjà connues. Dans certains cas, avoir un anonymat parfait permettrait l’utilisation malveillante d’un système et la cryptologie doit aussi tenir compte de ces abus potentiels. La troisième contribution de cette thèse consiste en la proposition du premier protocole d’accréditation anonyme multi-autorités traçable : un utilisateur demande une accréditation auprès d’une autorité émettrice et peut l’utiliser pour accéder à un système tout en restant anonyme. En cas d’abus, une autorité juge peut lever l’anonymat et retrouver un utilisateur malveillant grâce au traçage. De plus, ce protocole, tout en étant aussi efficace que les précédents pour une seule autorité émettrice, permet d’agréger des accréditations d’autorités émettrices distinctes pour avoir une accréditation de taille optimale.
ENS, Paris
ENS, Paris
ENS, Paris
ENS, Paris
ENS, Paris
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.
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.
ENS, Paris
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.
ENS, Paris
ENS, Paris
INRIA, Paris
INRIA, Paris
ENS, Paris
ENS, Paris
ENS, Paris
ENS, Paris
ENS, Paris
ENS, Paris
ENS, Paris
Salle Henri Cartan
Salle Henri Cartan
Salle Henri Cartan
Salle Henri Cartan
Salle Henri Cartan
Salle U/V
Salle Henri-Cartan
Salle Henri Cartan
Amphithéâtre Dussane
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, 75005 Paris.
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, Paris 5ème.
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, 75005 Paris.
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, 75005 Paris.
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, Paris 5ème
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, Paris 5ème
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, Paris 5ème.
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, Paris 5ème
In 1941, Claude Shannon introduced a continuous-time analog model of computation, namely the General Purpose Analog Computer (GPAC). The GPAC is a physically feasible model in the sense that it can be implemented in practice through the use of analog electronics or mechanical devices. It can be proved that the functions computed by a GPAC are precisely the solutions of a special class of differential equations where the right-hand side is a polynomial. Analog computers have since been replaced by digital counterpart. Nevertheless, one can wonder how the GPAC could be compared to Turing machines.
A few years ago, it was shown that Turing-based paradigms and the GPAC have the same computational power. However, this result did not shed any light on what happens at a computational complexity level. In other words, analog computers do not make a difference about what can be computed; but maybe they could compute faster than a digital computer. A fundamental difficulty of continuous-time model is to define a proper notion of complexity. Indeed, a troubling problem is that many models exhibit the so-called Zeno's phenomenon, also known as space-time contraction.
In this talk, I will present results from my thesis that give several fundamental contributions to these questions. We show that the GPAC has the same computational power as the Turing machine, at the complexity level. We also provide as a side effect a purely analog, machine- independent characterization of P and Computable Analysis.
I will present some recent work on the universality of polynomial differential equations. We show that when we impose no restrictions at all on the system, it is possible to build a fixed equation that is universal in the sense it can approximate arbitrarily well any continuous curve over R, simply by changing the initial condition of the system.
If time allows, I will also mention some recent application of this work to show that chemical reaction networks are strongly Turing complete with the differential semantics.Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, Paris 5ème.
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, Paris 5ème.
The idea of Probabilistic Programming is to use the expressiveness of programming languages to build probabilistic models. To implement this idea, a common approach is to take a general purpose language and extend it with (1) a function that allows to sample a value from a distribution, (2) a function that allows to condition values of variables in a program via observations, and (3) an inference procedure that build a distribution for a program using the two previous constructs.
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.
This is a join work with Guillaume Baudart, Martin Hirzel, Kiran Kate, and Avraham Shinnar.
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, Paris 5ème.
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.
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, Paris 5ème.
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, Paris 5ème
Salle Henri Cartan, 2e sous sol, Aile Rataud, École normale supérieure, 45 rue d'Ulm, Paris 5ème
