Les builds reproductibles : prouver que le logiciel exécuté est celui que vous avez inspecté
La Suisse a publié son code source de vote afin que quiconque puisse l'inspecter — et des chercheurs ont immédiatement découvert une porte dérobée cachée qui aurait pu forger une preuve parfaitement crédible tout en modifiant silencieusement les votes.
Nous sommes en mars 2019, à Berne. Swiss Post s'apprête à faire quelque chose qui semble être le nec plus ultra de la transparence électorale. Son système de vote par Internet — développé par le fournisseur espagnol Scytl, destiné à être utilisé pour les votes fédéraux suisses contraignants — va voir son intégralité du code source publiée en ligne pour que le monde entier la lise.
C'est ce que les défenseurs de la démocratie demandaient depuis des années. Ouvrir la boîte noire. Laisser les experts regarder. Faire confiance par l'inspection.
En quelques semaines, trois cryptographes indépendants — Sarah Jamie Lewis, Olivier Pereira et Vanessa Teague — ont examiné le code. Et ce qu'ils ont trouvé n'était pas rassurant.
La trappe que personne n'a vue jusqu'à ce que quelqu'un regarde
Le cœur du système était une preuve mathématique. Après que tous les votes aient été mélangés et brassés pour préserver l'anonymat, le logiciel générait une « preuve de mélange » cryptographique — un élément mathématique qui était censé démontrer, à quiconque le vérifiait, que le mélange avait été effectué correctement et qu'aucun vote n'avait été modifié.
On appelait cela la vérifiabilité universelle. L'idée : vous n'avez pas besoin de faire confiance au serveur. Vous vérifiez vous-même la preuve.
Les chercheurs ont découvert que la preuve était construite sur ce qu'on appelle un schéma d'engagement avec trappe. En termes simples : la preuve de mélange pouvait être faite pour « vérifier » correctement même si les votes avaient été silencieusement modifiés — à condition de connaître la valeur de la trappe. Et la valeur de la trappe était détenue par les opérateurs du système.
En d'autres termes, une autorité qui connaissait cette valeur pouvait générer une preuve de mélange qui passait la vérification tout en ayant réarrangé chaque bulletin de vote. La revendication de « vérifiabilité universelle » était infalsifiable de l'extérieur.
Ils ont intitulé leur article « Ceci n'est pas une preuve ».
Swiss Post et Scytl ont reconnu la découverte. Les autorités suisses ont suspendu le système.
La leçon semble technique. Elle ne l'est pas. La faille était invisible tant que le code restait fermé. Elle est devenue détectable dès qu'il a été ouvert. Mais la trouver a quand même demandé des cryptographes de classe mondiale travaillant pendant des semaines. La question plus large — celle dont traite réellement ce billet — est : que se passe-t-il entre « quelqu'un peut lire le code » et « vous pouvez être sûr que le code lu est celui qui s'est exécuté sur la machine » ?
L'affaire suisse a ouvert le code. Mais elle a exposé une lacune plus profonde qu'open source ne comble pas automatiquement.
Lire la recette n'est pas la même chose que goûter le plat
Imaginez un restaurant qui publie ses recettes. Chaque ingrédient, chaque technique, chaque étape — tout en ligne, tout le temps.
Imaginez maintenant que la cuisine est fermée à clé. Vous pouvez lire ce qui est censé se passer. Vous ne pouvez pas regarder ce qui se passe réellement.
C'est précisément la situation de la plupart des logiciels de vote, même les logiciels de vote open source. Publier le code source est une condition nécessaire pour la vérification indépendante. Ce n'est pas une condition suffisante.
Voici pourquoi. Le logiciel que vous lisez dans un dépôt n'est pas le logiciel qui s'exécute sur la machine. Entre « code source » et « programme exécuté » se trouve une chaîne d'étapes :
- Un compilateur prend le source et le traduit en code binaire lisible par la machine.
- Ce binaire est empaqueté, installé sur le matériel de vote ou les serveurs, et scellé cryptographiquement — ou pas.
- Au moment de l'élection, une machine démarre et exécute ce qui se trouve sur elle.
Chacune de ces étapes est un endroit où le code exécuté peut diverger du source que vous avez inspecté, sans aucune preuve visible. Un compilateur peut être manipulé pour insérer du code qui n'apparaît pas dans le source. Un binaire peut être échangé après sa création. Une machine peut démarrer une version différente de celle que vous pensiez chargée.
La trappe suisse vivait dans le source. Mais une trappe différente pourrait vivre n'importe où dans cette chaîne — et ne jamais apparaître du tout dans le code.
Le problème des builds reproductibles, en langage simple
Il existe une discipline en génie logiciel appelée builds reproductibles. Son objectif est simple : étant donné le même code source, le même compilateur et les mêmes instructions de construction, quiconque exécute le processus de construction devrait obtenir un binaire identique — octet pour octet, bit pour bit — chaque fois.
Cela importe parce que cela vous donne un moyen de vérifier. Si l'autorité électorale publie un hash binaire — une empreinte numérique unique du logiciel sur la machine — et si vous pouvez indépendamment reproduire ce binaire exactement identique à partir du source publié, vous avez une garantie cryptographique que le code sur la machine est le code que vous avez lu.
Si le binaire ne correspond pas, vous savez que quelque chose a changé entre le source et la machine. Vous ne savez pas quoi a changé. Mais vous savez qu'il faut poser la question.
Sans builds reproductibles, l'écart entre « source inspecté » et « logiciel exécuté » est invisible. Vous n'avez aucun outil pour le vérifier. Vous êtes de retour à faire confiance à l'autorité qui a effectué la construction.
Le projet Reproducible Builds — un effort intersectoriel dans la communauté du génie logiciel — a documenté systématiquement à quel point c'est difficile à réaliser et de combien de façons la chaîne de construction peut produire des résultats différents à partir du même source. Les compilateurs intègrent des timestamps. Les éditeurs de liens insèrent des variables d'environnement. L'ordre des fichiers varie. Chacun est un mécanisme par lequel deux builds « identiques » peuvent produire des binaires différents sans que personne n'ait l'intention de frauder.
L'attestation : la deuxième moitié du problème
Même si votre build est reproductible, un deuxième problème persiste. La reproductibilité prouve que quelqu'un peut reconstruire le même binaire à partir du source. Elle ne prouve pas que le binaire maintenant exécuté sur votre machine de vote est ce binaire.
C'est ici que l'attestation entre en jeu.
L'attestation est le processus de signature cryptographique d'une affirmation : « Cet appareil exécute le binaire logiciel X, construit au moment T, avec le hash H. » La signature doit provenir de quelque chose dont la manipulation est évidente — idéalement du matériel qui ne peut pas être remplacé par le logiciel après le démarrage, comme un Trusted Platform Module (TPM) ou un module de sécurité matériel. La revendication signée peut alors être vérifiée par quiconque possède la clé publique.
Pensez-y comme à un sceau inviolable sur une carte mémoire — sauf qu'au lieu d'une étiquette physique qui se déchire à l'ouverture, c'est une signature mathématique que vous pouvez vérifier sans faire confiance à la personne qui vous remet la carte.
Ensemble, les builds reproductibles et l'attestation forment une chaîne : vous lisez le source → vous le compilez et obtenez le binaire H → vous vérifiez que l'appareil exécuté atteste du binaire H → vous êtes confiant que la machine exécute le code que vous avez lu.
Sans cette chaîne, vous avez deux faits non connectés : voici le code source et voici une machine exécutant quelque chose. Le fait que ces deux choses correspondent est une question de confiance, pas de vérification.
« Nous exécutons un logiciel certifié et open source » est une revendication. Les builds reproductibles et l'attestation sont ce qui la rend vérifiable.
Ce que l'affaire suisse nous dit sur le problème plus profond
Revenons à la Suisse. Les chercheurs ont trouvé la trappe parce qu'ils ont lu le source. Swiss Post a reconnu le défaut et suspendu le système. Jusqu'à présent : le système fonctionnant comme prévu.
Mais remarquez ce qui n'a pas été vérifié dans aucune version rapportée de cette histoire. Même si la trappe n'avait pas existé dans le source, aucune partie indépendante n'avait un mécanisme pour confirmer que le binaire exécuté sur les serveurs de Swiss Post avait été compilé à partir de ce source exacte — et non à partir d'une version légèrement modifiée avec un défaut qui n'apparaissait jamais dans le code public.
Ce n'est pas hypothétique. En 2003, l'informaticien Ken Thompson, dans son discours d'acceptation du prix Turing, a décrit comment un compilateur pouvait être modifié pour insérer automatiquement une porte dérobée dans un programme — et ensuite être modifié à nouveau pour insérer la porte dérobée en lui-même, de sorte que même compiler le compilateur à partir du source propre produirait un binaire compromis. Le source semble immaculé. Le compilateur semble immaculé. Le résultat est cheval de Troie.
Ce n'est pas une attaque théorique exotique. C'est une classe de menace bien comprise. Et la défense contre elle est les builds reproductibles : si le résultat est déterministe et publié, n'importe quelle partie indépendante peut reconstruire à partir du source et détecter une divergence. Si ce n'est pas le cas — si chaque build produit un binaire différent pour des raisons techniques innocentes — la comparaison ne peut jamais être faite.
L'affaire suisse a prouvé qu'open source est mieux que fermé. Elle a aussi prouvé qu'open source, seul, n'est pas suffisant.
L'écart que notre suivi des écarts regarde
Chez TrustVoting, nous suivons un écart spécifique : l'absence, dans la plupart des systèmes de vote déployés, de builds reproductibles vérifiés publiquement et d'attestation d'appareil. Vous pouvez voir à quelle fréquence cet écart apparaît, et où, partout dans le monde.
Le système suisse avait open source. C'est l'un des programmes de vote par Internet les plus orientés vers la transparence du monde démocratique. Les chercheurs ont toujours trouvé un défaut dans la cryptographie — ce qui aurait été indétectable dans un système fermé. Et même après que ce défaut ait été trouvé et corrigé, un observateur indépendant n'aurait aucun mécanisme pour confirmer que le binaire corrigé sur le serveur était dérivé du source corrigé.
C'est l'écart. Il se situe précisément à la jonction entre le code que vous pouvez lire et le logiciel qui gère réellement votre vote.
Quelques choses qui pourraient le combler :
- Des instructions de construction publiées publiquement qui produisent le hash binaire exacte que l'autorité prétend exécuter — de sorte que tout observateur suffisamment technique puisse vérifier indépendamment.
- Une attestation signée du matériel inviolable sur chaque appareil de vote, publiant le hash du binaire exécuté à côté de chaque lot de résultats.
- Une surveillance continue après le déploiement contre le hash publié — de sorte qu'un échange de logiciel qui se produirait après la certification mais avant le jour de l'élection serait détectable.
Aucune de ces choses n'est exotique. Ce sont des pratiques standard dans le déploiement de logiciels hautement sécurisés. Elles sont largement absentes des exigences de certification des systèmes de vote.
Ce que vous ne pouvez toujours pas vérifier aujourd'hui — et ce qui le réparerait
Voici la position inconfortable dans laquelle nous nous trouvons après la Suisse 2019.
Nous savons qu'open source est mieux. La trappe a été trouvée précisément parce que le code était lisible. Un système fermé aurait expédié le défaut non détecté.
Nous savons que la vérifiabilité cryptographique est mieux que les bulletins de papier seuls. Toute la philosophie de conception du système suisse — vérifiabilité universelle, preuves mathématiquement vérifiables — est une tentative de laisser les électeurs confirmer, sans faire confiance à l'autorité, que leur vote a été compté.
Et nous savons que les deux sont insuffisants s'ils n'incluent pas le pont entre le source et le binaire exécuté.
En ce moment, pour pratiquement chaque système de vote déployé dans le monde, la réponse honnête à « comment sais-je que le logiciel sur cette machine est le logiciel qui a été examiné ? » est : vous ne pouvez pas. Vous faites confiance à l'autorité qui l'a déployé.
Cette confiance peut être bien placée. Mais la confiance n'est pas la vérification. La Cour constitutionnelle fédérale allemande l'a compris lorsqu'elle a jugé en 2009 que le vote électronique n'est légitime que lorsque les citoyens ordinaires — pas seulement les experts — peuvent indépendamment vérifier chaque étape essentielle du bulletin au résultat. Le raisonnement de la cour s'applique aussi clairement au déploiement de logiciels qu'au décompte des votes : si confirmer que le bon code s'exécute exige de faire confiance aux personnes qui l'exécutent, l'étape de vérification essentielle manque.
La solution n'est pas de démonter les efforts de vote open source. C'est de les compléter. Open source plus builds reproductibles plus attestation signée plus hashes binaires publiés publiquement équivaut à un système où « le logiciel que vous avez inspecté est celui qui s'est exécuté » est vérifiable par quiconque avec un ordinateur portable et de la curiosité — pas seulement par l'autorité qui l'a déployé.
Jusqu'à ce que cette chaîne soit fermée, chaque revendication « nous utilisons un logiciel ouvert et certifié » est une invitation à faire confiance. Et un système électoral qui vous demande de lui faire confiance, au lieu de vous montrer la preuve, n'a pas fini de résoudre le problème.
Voyez comment l'écart des builds reproductibles apparaît dans les systèmes de vote que nous suivons
Lisez la version de 2 minutes de cet argument
Explorez la carte mondiale des écarts de vérification de la technologie électorale
Sources
- Lewis, Pereira, Teague — Ceci n'est pas une preuve (trapdoor commitments in the Scytl-SwissPost Internet voting system), 2019
- Bundesverfassungsgericht, Judgment of 3 March 2009, 2 BvC 3/07 and 2 BvC 4/07 (English translation)
- Springall, Finkbeiner, Durumeric, Kitcat, Hursti, MacAlpine, Halderman — Security Analysis of the Estonian Internet Voting System, ACM CCS 2014
- California Secretary of State news release (Aug. 21, 2018): certifying LA County VSAP Tally as California's first certified open-source election technology
- Halderman, Teague — The New South Wales iVote System: Security Failures and Verification Flaws in a Live Online Election, E-Vote-ID 2015 (arXiv:1504.05646)
- Curling v. Raffensperger, No. 1:17-cv-2989-AT, Opinion and Order (N.D. Ga. Oct. 11, 2020), Doc. 964 (Justia)