David MENTRE wrote:
Mouais, les canaux cachés, c'est probablement le dernier truc que je
regarderais sur un système avec un OS classique et un processeur
généraliste : ça doit fuire de partout avec les caches, la gestion
mémoire, l'utilisation du processeur (cf. le thread relatif à
l'hyper-threading et les canaux cachés sur linux-kernel).
L'idée pour mon cas n'est pas vraiment de savoir comment éviter les
canaux cachés dans un OS mais avant tout de connaître la forme des
propriétés de sécurité au même niveau d'abstraction que le programme à
tester. Et dans ce cas, les problèmes de sécurités se transforment en
général en un problème d'accessibilité et on retombe sur des problèmes
classiques en model checking. Après, SELinux est un exemple de système
pour lequel on a une idée du flot d'information entre processus. Mais ça
reste un travail de recherche qui a avant tout le mérite de mettre en
avant les faiblesses des systèmes classiques et donc indirectement de
rester méfiant sur l'utilisation à grande échelle des systèmes de vote.
Si il y a des gens intéressé, je suis bien sûr partant pour faire une
démo à Gulliver sur SELinux et Mach (merci pour les pistes) quand je
serai plus avancé sur le sujet.
J'ai cru comprendre que vous avez déjà commencé à regarder l'utilisation
de méthodes formelles pour prouver certaines fonctionnalités de demexp.
Je n'ai pas encore eu le temps de regarder ça mais j'imagine qu'il
existe des outils pour faire des analyses à partir de bytecode Ocaml. En
tout cas il en existe pas mal pour le Java et Ocaml me semble encore
plus adapté pour faire ce genre de chose.
Amicalement,
d.
PS : on devrait faire une réunion cette semaine, mais on ne sait pas
encore quand. :) Si tu as des contraintes, fait le nous savoir.
Malheureusement, je suis pas mal pris cette semaine mais je suis tout à
fait libre pour une réunion mercredi soir ou ce week end.
Jérémy
--
Liste de discussion demexp-fr.
Pour se désinscrire, cliquer sur le lien ci-après.
mailto:[EMAIL PROTECTED]
