[Fsfe-france] Quelques elements supplementaires sur le vote electronique verifie

[David MENTRE]

Bonjour,

Un ami a récemment attiré mon attention sur un email de Benoît Sibaud à
propos du vote électronique[1] sur la liste fsfe-france.

Benoit, secondé par Xavier Roche, posent un certains nombres de
questions habituelles sur le vote électronique, mais il me semble que
les éléments de réponses apportés dans ce débat sont approximatifs et
inexacts.

Dans la suite de cet email, je ne parlerais que du vote électronique en
remplacement du vote traditionnel papier (« urne électronique ») et pas
du vote sur Internet (beaucoup plus difficile notamment en raison des
problèmes d'authentification).

Pour répondre aux questions de Benoît :

> Pourquoi le code de l'urne n'est-il pas publique ?

Il faut évidemment qu'un tel code soit public.

> Et s'il était public, serait-il pour autant fiable/sans bogue ?

Il y a moyen de *prouver mathématiquement* qu'un code est sans bogue,
oui, avec du logiciel libre.

Pour l'instant, trois axes me semblent possibles :

 - vérifier un code C avec Caduceus et Why (http://why.lri.fr/), puis
   Coq (http://coq.inria.fr/) ;

 - vérifier un code common-lisp avec ACL2
   (http://www.cs.utexas.edu/users/moore/acl2/) ;

 - dériver un programme OCaml prouvé correct à partir de preuves
   formelles, soit directement dans Coq, soit en utilisant Focal
   (http://caml.inria.fr/archives/200410/msg00182.html).

J'ai commencé à défricher la piste ACL2 mais je suis encore loin du
compte. Mais j'ai déjà prouvé un théorème du style « l'enregistrement
d'une vote incrémente bien le compteur correspondant au vote choisit
». Je peux filer le code ACL2 si nécessaire, mais le travail n'est pas
fini.

> Et s'il était sans bogue, pourrait-on avoir confiance ?
> (Reflections on Trusting Trust, ou comment insérer une porte dérobée
> discrète dans un logiciel http://www.acm.org/classics/sep95/)

Question classique : est-ce que je peux avoir confiance dans un
compilateur, un assistant de preuve, un OS ?

Dans l'objectif d'une urne électronique, il me semble réalisable de
prouver un support exécutif minimum (filesystem, drivers entrée/sortie
de base) et logiciel de vote.

En ce qui concerne les assistants de preuve, ils sont généralement
construits par étapes, le coeur étant ultra simple pour être vérifiable
manuellement (ACL2, Coq). Bien entendu, l'_ensemble_ d'un tel système
n'est pas pour l'instant pas vérifié. On peut également envisager
d'utiliser plusieurs assistants, écrits par des équipes différentes. 

En ce qui concerne l'environnement de compilation, la communauté
scientifique commence à considérer la vérification de vrais compilateurs
(http://www-sop.inria.fr/lemme/concert/). Je pense qu'on peut prouver
pas mal de chose en partant sur un compilo minimal et encore simplifié
pour l'objectif, comme TCC.

Quand au point Trusting Trust, on peut poser que l'environnement de
création du logiciel de référence est un logiciel bien connu et répandu,
comme une distribution Debian officielle.

De toute façon, cette notion de confiance est toujours relative. Un ami
magicien m'assure qu'il pourrait échanger les enveloppes contenant les
bulletins papier avant décomptage des votes. Bien évidemment,
l'informatique permet de réaliser cette opération à grand échelle plus
facilement.

> Et même si le logiciel était fiable et de confiance, pourrait-on avoir
> confiance dans le matériel ? Pas de bogue (bogues fdiv, hlt, f00f, coma sur
> les Pentium par exemple) ? De confiance (tout le monde est confiant dans
> TCPA/Palladium/NGSCB/TCG ?)

Depuis le bug du pentium justement, les unités arithmétiques et
flottantes des processeurs Intel et AMD sont prouvées formellement (avec
ACL2 dans le cas d'AMD). Donc oui on peut avoir un matériel très fiable.

Quand à la confiance, on peut envisager de vérifier un processeur simple
et sur mesure, comme le Léon ou sur un FPGA. (ok, ça rajoute un niveau
d'incertitude avec les compilateurs vers ASIC ou FPGA) Ou demander à
Intel ou AMD l'accès aux informations de vérification.

Il y a également eu des tentatives pour prouver formellement toute la
chaine, du processeur à l'OS en passant par le compilateur et
l'assembleur (processeur FM9001 avec un ancêtre d'ACL2).

> Et si le logiciel et le matériel étaient fiables et sans bogue,
> seraient-ils sécurisés, protégés contre les attaques ? (pensez aux machines
> de vote sous Windows NT avec du WiFi disponibles dans le commerce...)
> Faut-il permettre une concentration des risques en connectant en réseau les
> urnes électroniques ? En laissant une entreprise les produire ? En laissant
> quelques personnes les contrôler ?

La aussi, il faudra des procédures et règles (pas d'OS sur la machine,
sécurisation physique des machines de vote, traces papier, absence de
connexion réseau, ...). Mais ce n'est pas pour rien qu'on a un code
électoral.


> Et comment on résoud les problèmes de simplicité (n'importe qui comprend
> _tout_ le mécanisme du vote papier), de transparence (on fait bien ce qui
> est prévu), de vérification (on peut recompter), d'anonymat (comment savoir
> si le vote est anonyme ?), d'intégrité (comment savoir si le vote est
> modifié ?), etc.

Tout ces points peuvent être abordés techniquement. Je reconnais que la
simplicité va en prendre un coup. :)

Pour être plus précis :

 - transparence, vérification : vérification formelle, publication et
   certification par tous (principes du logiciel libre) ;

 - anonymat : preuves algorithmiques et matérielles ;

 - intégrité : sécurités physiques, preuves.


Le but de cet email a pour but de donner quelques arguments
scientifiques au débat. Je ne dirais jamais que le vote électronique est
sans risque. Mais s'il doit arriver, autant le faire avec le maximum de
garantie et des constructions scientifiques solides.

La communauté du logiciel libre a certainement son rôle à jouer. Ce
n'est pas une entreprise commerciale classique qui le fera (coûts de
développement trop élevés).

<pub>
Pour info et puisuque ça me semble pertinent pour le débat, j'ai
 commencé une liste des outils de vérification formelle libres :
 http://gulliver.eu.org/ateliers/fv-tools/index.html
</pub>


Amicalement,
d. mentré

[1] http://lists.gnu.org/archive/html/fsfe-france/2004-11/msg00007.html
-- 
David Mentré -- Projet d'expérience démocratique
 http://www.demexp.org -- http://savannah.nongnu.org/projects/demexp

pgpzogSTHyY9g.pgp
Description: PGP signature