Le vote électronique, vous êtes au courant? - Page 3

Bovido (./60)>

Martial: j'attends juste qu'on me montre qqch de différent et qui tient le coup. J'ai rien du tout à prouver pour le coup, je sais qu'il existe des autres choses, mais rien de prouvé à ma connaissance pour une utilisation dans la vraie vie. et pour le liens, c'est juste pour dire que ca m'intéresse bcp et que je suis un peu informé sur ce qui se passe...

bon j'ai pas tout lu mais yavait dans charlie hebdo un arcticle pour apprendre a pirater les machines de vote et qui expliquiat less failles, et dans un bled porche ils ont eu des voixen + et en -selon les bureaux de vote

./55, ./63: je voulais signifier par là qu'une suite de tests ne permet de trouver que ce qui ne fonctionnerait pas, mais absolument pas de prouver qu'un programme est correct (ou complet, d'ailleurs)
On m'apprend en classe que vérifier la conformité à une spec en utilisant des tests, ce qui est nécessaire, mais:
* à cause notamment de l'explosion combinatoire, la suite de tests ne peut en général pas avoir une couverture de 100% du critère le plus restrictif (j'ai encore oublié son nom...);
* une spec n'a à peu près aucune chance d'être complète, ou bien elle peut contenir des âneries, etc.
Les langages formels, associés à des compilos certifiés, ont plus de chances de donner du code correct - mais encore faut-il avoir spécifié correctement. [EDIT: et puis ça coûte plus cher de faire du formel... ce qui rend encore moins populaire cette façon de faire]

> mais rien de prouvé à ma connaissance pour une utilisation dans la vraie vie
Si tu parles des machines de vote, les travaux des chercheurs de Princeton, Felten et Halderman, sont convaincants: un individu laissé tout seul avec la machine Diebold pendant 3 minutes, sans surveillance, peut l'ouvrir avec une clé type "hotel minibar" (et on pouvait, jusqu'à ce que l'affaire soit signalée, trouver un screenshot de l'empreinte de la clé sur le site de Diebold !!), mettre un chip contenant un code non signé (et potentiellement malicieux) qui prend le pas sur le code d'élection normal.
Or, les chercheurs écrivent que les "election workers" qu'ils ont interviewés ont à peu près tous été laissés 3 minutes tous seuls sans surveillance avec la machine...
C'est donc utilisable dans la vraie vie.

faudrait des codes en ROM non amovibles (genre un SoC avec sa mem embarquée) et des signatures numériques sur les codes "amovibles", surtout.

Mais tout ça n'empêcherait pas que le citoyen lambda ne comprendrait rien à ces moyens de signature/certification etc., donc que ça exigerait de lui une confiance aveugle en les gens qui maîtrisent la technologie utilisée... et donc qu'il n'y aurait pas de réelle possibilité de contrôle citoyen

(et de toute façon, ça rend impossible toute vérification ultérieure, je trouve ça extrêmement gênant :/ )

je parle de signature du code interne de la machine.

pour donner un parallèle, le citoyen lambda a t il besoin de connaitre le fonctionnement du cryptage d'une carte bleue?

Ça se voit que t'as pas lu le topic. Comme dit plus haut, le citoyen lambda peut vérifier, en regardant son relevé de compte, et en comptant l'argent que lui sort le distributeur, que le cryptage de la carte bleue fonctionne bien. Ce n'est pas du tout analogue au vote électronique.

ok, d'accord.

Lionel Debroux (./65) :
mais absolument pas de prouver qu'un programme est correct

C'est impossible: halting problem

Les langages formels, associés à des compilos certifiés, ont plus de chances de donner du code correct

Ouep, c'est pour cela que pour des applis *vraiment* critiques, l'ADA est souvent utilisé.

Si tu parles des machines de vote...

Du tout; je parlais d'une méthode de vérification. Ce qui est généralement (dans le sens où ils font des vraies vérification, pke c'est rare que tout cela soit fait) utilisé est:
- preuve formelle d'algos
- analyse statique de code source et dynamique
- test de fonctionnalités avec une plus ou moins bonne couverture

nEUrOO (./72) :

Lionel Debroux (./65) :
mais absolument pas de prouver qu'un programme est correct

C'est impossible: halting problem

C'est possible: abstract interpretation

Jamais rien vu de probant en pratique sur les méthodes formelles...
Mais je dois dire que j'aimerais bien essayer Astrée payant... mais bon... des frienchies en plus

hé hé hé.
cousot (le chef d'astrée) c'est mon directeur des études.
j'ai suivi son cours, et franchement, l'interprétation abstraite, ça tue méchamment des ours.

Oui, je ne doute pas, mais je veux voir en pratique
Je sais que mon boss avait correspondu avec cousot, je vais tenter de le relancer la dessus pour voir...

en pratique ça prouve l'airbus A380

airbus bosse aussi avec une boite en californie je crois (polyspace?) et surement bcp d'autres
mais c'est impressionnant si en pratique ca prouve tout le code

Oui c'est très impressionnant. Et le plus ouf c'est que ça le fait en quelques heures seulement, sur un PC normal.

Ouais enfin le "ça prouve l'A380" ça veut pas dire grand chose, vu qu'une grosse partie du code vient de sous traitants qui prouvent de leur côté... Et vu le nombre de calculateurs indépendant qui sont intégrés à la bestiole.

Pour être plus précis : Astrée a prouvé l'absence d'erreurs d'exécution dans le "primary flight control software" de l'Airbus A380. Et surtout, le plus impressionnant, c'est qu'en plus la preuve a signalé 0 fausses alertes (un logiciel de ce type ne laisse passer aucune erreur, mais peut parfois signaler des choses qu'il trouve bizarres mais qui en fait ne sont pas des erreurs : des fausses alertes).

Ayant vu les coulisses de l'A380, c'est pas si impressionnant que ça va, même si c'est clair que le résultat final est sympathique
Enfin bon pour en revenir à la vérification de code, l'aéronautique est en effet un bon exemple de la chose.Mais c'est pas parcequ'un code est prouvé, vérifié et certifié qu'il est sécurisé pour autant... Tout simplement parceque la preuve et la vérification se font par rapport à la spécification, qui peut comporter ses propres erreurs.

En effet, Astrée prouve l'absence d'erreurs d'exécution sur du code C, en utilisant donc le standard du C (je sais pas quelle spec). Si le compilateur C ne respecte pas la norme, effectivement la preuve n'en est pas vraiment une

Mais j'imagine qu'ils font aussi attention à leurs compilos (et à leurs processeurs aussi bien sûr, pasque si le proc respecte pas la norme IEEE sur le calcul des flottants à la lettre, par exemple, ben les preuves d'Astrée ne sont plus valide non plus en cas d'erreur d'arrondi ...).

La norme utilisée pour l'aéronautique est la DO-178B, j'imagine que le logiciel en question est de niveau A, bonne lecture
Pour la compilation, il faut de toutes façons pouvoir assurer la traçabilité jusqu'au niveau objet, et c'est fait à la main si le compilo n'est pas certifié.

Ah non mais quand je parlais de norme, je parle de la norme C, genre C89 ou C99 ou autres

[EDIT : j'ai vérifié, la norme que prend en compte Astrée est C99]

J'avais bien compris, mais c'était pour parler des normes de codage, de vérification, etc, en vigueur dans l'aéronautique, quel que soit le langage

ok

nEUrOO (./72) :

Lionel Debroux (./65) :
mais absolument pas de prouver qu'un programme est correct

C'est impossible: halting problem

euh, le problème de l'arrêt ne pose problème que dans les cas "difficiles"/ambigus : quand on a un logiciel critique on essaye justement d'être le plus clair possible et de s'en tenir à des invariants vérifiables facilement... et comme dit moumou ça marche très bien en pratique ^^

dualmoo (./77) :
en pratique ça prouve l'airbus A380

oui enfin prouver l'absence d'exceptions c'est quand même loin d'être "prouver la correction" hein c'est juste "prouver que les autres preuves de correction sur le code ont effectivement un sens, i.e. qu'on ne viole pas la type-safety et qu'on a pas d'overflow"...

certes.

cela dit l'interprétation abstraite ça ne fait pas que ça, on peut aussi prouver des propriétes de bon comportement autres. par exemple les drivers de windows vista, pour être spécifiés, doivent être analysés avec un outil d'interprétation abstraite qui prouve tout un tas de trucs bien sur le driver (genre que quand il release un lock il en avait bien acquéri un auparavant, qu'il n'y a pas de deadlocks, qu'on ne corromp pas la mémoire du noyau, etc ...)

pollux, mais c'est les vérifiations ne sont pas faites uniqumeent sur les applications critiques... mais aussi sur des appli qui sont vraiment mal codées.