Sciences du logiciel - Xavier Leroy

Xavier LeroyChaire Sciences du logicielAnnée 2025-2026Collège de FranceSéminaire - Pierrick Gaudry : Outils cryptographiques pour le vote électroniquePierrick GaudryCNRSLe vote par Internet est un exemple où la cryptographie avancée est requise, et déployée en pratique, afin de garantir de bonnes propriétés de sécurité. Dans cet exposé, nous présenterons ce contexte du vote électronique, ainsi que le protocole de vote Belenios (simplifié), afin d'illustrer les besoins en preuves zero-knowledge (ZKP).Ensuite, nous décrirons le fonctionnement de ces ZKP utiles au vote, en partant des plus basiques, pour aller progressivement vers des constructions complexes qui relèvent plutôt du calcul multipartite. Nous expliquerons comment ceci permet d'aller plus loin que le vote classique en termes de secret du vote, grâce à la notion de dépouillement en aveugle (tally-hiding).

Xavier LeroyChaire Sciences du logicielAnnée 2025-2026Collège de France02 - Le calcul sécurisé : calculer sur des données chiffrées ou privées : Chiffrement totalement homomorphe : calculer sur des données chiffrées (1)RésuméCe cours a commencé par des rappels sur les algorithmes de chiffrement et la manière de spécifier et de démontrer leur sécurité. Nous avons ensuite introduit la notion de chiffrement semi-homomorphe : les chiffrements qui sont homomorphes pour l'addition ou la multiplication de textes clairs mais pas pour les deux opérations. Nous en avons montré quatre exemples : les chiffrements RSA, d'ElGamal, d'ElGamal exponentiel, et de Paillier. Mais l'objectif ultime est d'obtenir un chiffrement qui soit homomorphe pour l'addition et pour la multiplication, ce qui permettrait d'évaluer de manière homomorphe des circuits booléens arbitraires, via un encodage des portes logiques par des polynômes.Comme première étape dans cette direction, nous avons introduit la notion de chiffrement faiblement homomorphe, c'est-à-dire homomorphe pour un nombre limité d'additions et de multiplications. Nous avons présenté la construction, due à van Dijk, Gentry, Halevy et Vaikuntanathan (2010), d'un tel chiffrement utilisant uniquement des nombres entiers. Ce chiffrement peut être rendu totalement homomorphe en le combinant avec la procédure de bootstrap introduite par Gentry en 2009. Cette procédure repose sur l'évaluation homomorphe d'un circuit qui réalise le déchiffrement. Elle permet de supprimer la limite sur le nombre d'additions et de multiplications successives, et donc d'évaluer des circuits arbitraires, à condition que le circuit de déchiffrement soit suffisamment simple pour être évalué par un chiffrement faiblement homomorphe, ce qui est difficile à réaliser.

Xavier LeroyChaire Sciences du logicielAnnée 2025-2026Collège de France01 Le calcul sécurisé : calculer sur des données chiffrées ou privées : Sécuriser le calcul : introduction et étude de casCe premier cours sur le calcul sécurisé a introduit deux approches pour calculer sur des données privées sans les révéler aux opérateurs du calcul : le chiffrement homomorphe, qui permet d'effectuer certains calculs sur des données chiffrées et de produire des résultats également chiffrés, sans donner les clés de déchiffrement au calculateur ; et le calcul multipartite sécurisé, dans lequel plusieurs participants coopèrent pour calculer une fonction de leurs données privées, sans jamais révéler ces données aux autres participants. Ces deux approches seront étudiées de manière plus approfondie dans la suite du cours.Pour compléter ce premier cours, nous avons étudié trois exemples d'utilisation de ces techniques. La première étude de cas est le calcul multipartite d'une moyenne, permettant par exemple à un groupe d'amis de déterminer leur salaire moyen sans que chacun révèle son salaire aux autres. La deuxième étude de cas porte sur le dépouillement d'un vote électronique simplifié, utilisant du chiffrement homomorphe pour totaliser les votes sans avoir à déchiffrer les bulletins individuellement, ainsi que des preuves à divulgation nulle de connaissance pour garantir que les votes sont bien formés sans avoir à les divulguer. La troisième étude de cas concerne le calcul bipartite de l'intersection de deux ensembles privés, un algorithme qui permet par exemple de découvrir des contacts sur un réseau social sans révéler de données personnelles.

Xavier LeroyCollège de FranceScience du logicielAnnée 2023-2024Séminaire - Daan Leijen : Design and Compilation of Efficient Effect Handlers in the Koka LanguageDaan LeijenMicrosoft Research

Xavier LeroyCollège de FranceScience du logicielAnnée 2023-202408 - Structures de contrôle : de « goto » aux effets algébriques : 08 - Structures de contrôle : de « goto » aux effets algébriques : Logiques de programmes pour le contrôle et les effets