Salut Fabrice,
Le 22/04/07, Fabrice Papirnyk<[EMAIL PROTECTED]> a écrit :
> > > preuve de code
> Voir notamment Coq (de l'INRIA) et ACL2. Il y en a d'autres
Est-ce que cela a été mis en place pour Demexp ?
Non. Serge a fait quelques preuves de l'algo Condorcet mais pour
l'instant je ne suis pas capable de les comprendre et encore mois de
les intégrer.
Est-ce que la preuve de code se fait principalement par exemple sur le
code de l'algorithme Condorcet, ou est-ce que c'est intéressant de le
faire aussi sur le reste ?
A priori tout. :-) Mais Coq n'est certainement mais l'outil le plus
adapté dans toutes les situations.
(1) > > > techniques de signature de code d'exécutable
> http://www.g10code.com/p-sfsv.html
(2) > > > technique de vérification d'exécutable
> J'ai un article papier quelque part, il faut que je le retrouve.
Si je comprends bien, il s'agit de vérifier un exécutable (1) AVANT son
exécution et (2) PENDANT son exécution ?
Oui et oui.
J'ai vu qu'il était facile de vérifier l'authenticité d'un logiciel que
l'on vient de télécharger. Qu'en est-il de le vérifier *pendant* son
utilisation ?
J'ai au moins vu un article qui proposait une telle approche (désolé,
j'ai oublié la référence). Pas sûr qu'elle soit réellement utilisable
cependant.
Amicalement,
d.
--
Liste de discussion demexp-fr.
Pour se désinscrire, cliquer sur le lien ci-après.
mailto:[EMAIL PROTECTED]
