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 Dussane – ENS Paris, 45 rue d'Ulm & Zoom
L'augmentation du volume de données collectées par des capteurs et générées par des interactions humaines a mené à l'utilisation des bases de données orientées graphes en tant que modèle de représentation efficace pour les données complexes. Les techniques permettant de tracer les calculs qui ont été appliqués aux données au sein d'une base de données relationnelle classique sont sur le devant de la scène, notamment grâce à leur utilité pour faire respecter les régulations sur les données privées telles que le RGPD en Union Européenne. Notre travail de recherche croise ces deux problématiques en s'intéressant à un modèle de provenance à base de semi-anneaux pour les requêtes navigationnelles. Nous commençons par présenter une étude approfondie de la théorie des semi-anneaux et de leurs applications au sein des sciences informatiques en se concentrant sur les résultats ayant un intérêt direct pour notre travail de recherche. La richesse de la littérature sur le domaine nous a notamment permis d'obtenir une borne inférieure sur la complexité de notre modèle. Dans une seconde partie, nous étudions le modèle en lui-même et introduisons un ensemble cohérent d'algorithmes permettant d'effectuer des calculs de provenance et adaptés aux propriétés des semi-anneaux utilisés. Nous introduisons notablement une nouvelle méthode basée sur la théorie des treillis permettant de calculer la provenance pour des requêtes complexes. Nous proposons une implémentation open-source de ces algorithmes et faisons une étude expérimentale sur de larges réseaux de transport issus de la vie réelle pour attester de l'efficacité pratique de notre approche. On s'intéresse finalement au positionnement de ce cadre de travail par rapport à d'autres modèles de provenance à base de semi-anneaux. Nous nous intéressons à Datalog en particulier. Nous démontrons que les méthodes que nous avons développées pour les bases de données orientées graphes peuvent se généraliser sur des requêtes Datalog. Nous montrons de plus qu'elles peuvent être vues comme des généralisations de la méthode semi-naïve. En se basant sur ce fait-là, nous étendons les capacités de Soufflé, un évaluateur Datalog appartenant à l'état de l'art, afin d'effectuer des calculs de provenance pour des requêtes Datalog. Les études expérimentales basées sur cette implémentation open-source confirment que cette approche reste compétitive avec les solutions spécifiques pour les graphes, mais tout en étant plus générale. Nous terminons par une discussion sur les améliorations possibles du modèle et énonçons les questions ouvertes qui ont été soulevées au cours de ce travail.
The growing amount of data collected by sensors or generated by human interaction has led to an increasing use of graph databases, an efficient model for representing intricate data. Techniques to keep track of the history of computations applied to the data inside classical relational database systems are also topical because of their application to enforce Data Protection Regulations (e.g., GDPR). Our research work mixes the two by considering a semiring-based provenance model for navigational queries over graph databases. We first present a comprehensive survey on semiring theory and their applications in different fields of computer sciences, geared towards their relevance for our context. From the richness of the literature, we notably obtain a lower bound for the complexity of the full provenance computation in our setting. In a second part, we focus on the model itself by introducing a toolkit of provenance-aware algorithms, each targeting specific properties of the semiring of use. We notably introduce a new method based on lattice theory permitting an efficient provenance computation for complex graph queries. We propose an open-source implementation of the above-mentioned algorithms, and we conduct an experimental study over real transportation networks of large size, witnessing the practical efficiency of our approach in practical scenarios. We finally consider how this framework is positioned compared to other provenance models such as the semiring-based Datalog provenance model. We make explicit how the methods we applied for graph databases can be extended to Datalog queries, and we show how they can be seen as an extension of the semi-naïve evaluation strategy. To leverage this fact, we extend the capabilities of Soufflé, a state-of-the-art Datalog solver, to design an efficient provenance-aware Datalog evaluator. Experimental results based on our open-source implementation entail the fact this approach stays competitive with dedicated graph solutions, despite being more general. In a final round, we discuss on some research ideas for improving the model, and state open questions raised by our work.
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
