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 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 - visio
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
