David MENTRE wrote:
Très intéressant, même si en ce qui concerne demexp on est encore très
loin de ne serait-ce que spécifier les parties sécurité. Et nos
contraintes de sécurité seront probablement *très* spécifiques.
Elle sont les mêmes pour tout les systèmes de vote, sur lesquels il y a
pas mal de travaux
En rapport lointain avec votre projet POLITESS, nous avons un contact
avec l'ENST Bretagne, à Rennes (Ahmed Bouabdallah, Nora et Frédéric
Cuypens). Le projet demexp à participé à l'encadrement de deux
étudiantes en master sur le vote électronique (cf. notre wiki pour le
rapport). Nous (et en particulier je) sommes preneurs de toute info
permettant d'implémenter un système sécurisé proprement (de la
conception du code à la mise en place des serveurs).
J'ai lu le rapport de projet de l'ENST Bretagne qui donne des idées pour
formaliser les politiques de sécurité d'un système de vote. Le vote
électronique est souvent pris comme exemple et le modèle Or-BAC de
Cuppens & Co est tout à fait adapté pour formaliser les contraintes d'un
tel système. Seulement, la problématique est de passer d'une
description macroscopique des contraintes à une idée de preuve des
algos ou du programme (en COQ ou par model checking par exemple) qui
partent d'une desription des contraintes de sécurité sous forme
d'automate ou de logique temporelle. Dans une certaine mesure s'assurer
qu'un vote est bien pris en compte ne fait pas intervenir
l'environnement, OS, réseaux ..., qui sont supposé marcher et dont on
peut avoir un modèle très abstrait. Seulement, pour un système Linux
actuel, on ne peut pas faire l'hypothèse qu'un cheval de troie ou même
Skype est incapable d'inférer des informations, même partielles, sur les
actions du votant. On a même assez peu d'idée de ce que qu'un programme
espion peut inférer d'un autre programme.
En dehors de l'idée d'un CD Live qui ne fait tourner que Demexp, il
existe des solutions pour "envelopper" les processus par domaine de
confiance. Par ex : domaine Interface Utilisateur, domaine skype qui ne
communique avec le domaine Utilisateur que de manière explicite (et avec
contenu crypté et enveloppe XML pour D-BUS, Bonobo ou DCOP par exemple).
Ceci est fait afin d'éviter la création de canaux cachés non
souhaitables entre les différents programmes. La solution la plus avancé
est SELinux initié par la NSA qui permet de mettre tout ça en oeuvre.
J'ai pas encore compris les détails (en 1 mois de travail) puisque qu'il
faut que je commence déjà par bien comprendre comment fonctionnent de la
gestion des processus en théorie des OS pour comprendre dans quelle
mesure ils peuvent interférer de l'information l'un sur l'autre pour
avoir une idée de comment et ou mettre en place un cloisonnement, i.e.
ce que fait SELinux. Après on peut avoir une idée de preuve qu'il n'y a
pas de fuite d'information quand au nom du vote et du vote ...
A bientôt
Jérémy
--
Liste de discussion demexp-fr.
Pour se désinscrire, cliquer sur le lien ci-après.
mailto:[EMAIL PROTECTED]
