Excusez moi pour mon insistance
Comme vous le voyez je ne suis pas un informaticien, mais quelqu'un qui
s'intéressent à l'informatique depuis 10 ans. J'ai commencé avec le DOS 3.2
à l'époque jusqu'au 6.22 et ensuite connu toute les versions de windows.
Honnêtement pour un autodidacte je me débrouille un peu (j'ai monté un petit
réseau avec 10 PC sous Win 2000 Pro, configuré les cartes et tous le reste),
en étant patient et surtout logique j'y suis arrivé, mais bon, il a fallu
gratter.
Sérieusement, est ce qu'une personne de mon niveau peux espérer utiliser
linux pour faire des serveurs (mails, intra, etc)
OoO Lors de la soirée naissante du mardi 27 janvier 2004, vers 18:55, (Michel Talon) disait:
Ça donne le 802.11b, le GSM, SSLv2, les Microsofteries et tout un tas d'autres vastes blagues au niveau de la sécu parce qu'ils n'y connaissaient rien en vérification.
Theo de Raadt il a utilisé la vérification pour faire son business?
Non et on trouve des failles dans OpenSSH. SSLv3 a été vérifié formellement et à ce jour, aucune faille n'a été trouvée en dehors des erreurs d'implémentation. Des efforts sont faits pour la vérification formelle de ssh, mais à ma connaissance, personne ne s'est encore intéressé aux problèmes d'implantations.
Mais encore une fois, la vérification n'a pas prétention aujourd'hui de vérifier l'existant en C, mais de vérifier les systèmes à concevoir et les protocoles à un certain niveau d'abstraction. Certains croient pouvoir s'en passer et se sont plantés magistralement (cf ci-dessus), d'autres ont fait des recherche et cela tient.
Quand on veut mettre au point un système d'apparence particulièrement simple (un protocole) destiné à être utilisé par des milliers de personnes, on a le bon goût de s'assurer formellement que ce système est sûr jusqu'à un certain niveau.
Avant 95, la très grande majorité des protocoles cryptos, même très simples, se sont avérés _faux_. Bizarrement, cela coïncide avec le début de la vérification dans ce domaine.
Tu crois pas que tu pousses le bouchon un peu loin sur les vertus de ta recherche? Si je connais rien en informatique, pour te faire plaisir, il y a une chose que je connais, c'est comment on fait pour justifier des choses qui ne servent à rien en disant qu'elles sont d'une utilité fondamentale, dans le domaine de la recherche.
Tes seuls arguments est que la vérification de programme arbitraire en C est imparfaite. Je vais t'économiser beaucoup de salive, c'est un problème totalement indécidable. Tu n'auras jamais aucun programme capable d'une telle prouesse. Je ne vois toujours pas en quoi ce seul et unique argument est une preuve de quoi que ce soit puisque c'est une partie infime de la vérification.
Quant au fait que tu sois béotien complet et que cela justifie donc que la vérification n'est que foutaises, c'est un lien logique qui m'échappe, d'autant que j'ai patiemment argumenté sur chacun des posts en te donnant de _nombreux_ exemples où la vérification est utilisée dans des domaines que tu croises tous les jours, mais comme tu es particulièrement borné, tu reviens toujours à ton programme en C sans te rendre compte que ce n'est pas le domaine principal de la vérification tout simplement parce que tu n'y connais absolument rien (et en plus ne possède a priori pas les facultés d'ouverture nécessaire à comprendre qu'un programme en C n'est pas la seule modélisation d'un système possible) mais que tu fais partie de la masse des prétentieux qui croient tout connaître et tout pouvoir juger parce qu'ils ont un ordinateur à eux. -- #ifdef STUPIDLY_TRUST_BROKEN_PCMD_ENA_BIT 2.4.0-test2 /usr/src/linux/drivers/ide/cmd640.c
OoO Lors de la soirée naissante du mardi 27 janvier 2004, vers 18:55,
talon@lpthe.jussieu.fr (Michel Talon) disait:
Ça donne le 802.11b, le GSM, SSLv2, les Microsofteries et tout un
tas d'autres vastes blagues au niveau de la sécu parce qu'ils n'y
connaissaient rien en vérification.
Theo de Raadt il a utilisé la vérification pour faire son business?
Non et on trouve des failles dans OpenSSH. SSLv3 a été vérifié
formellement et à ce jour, aucune faille n'a été trouvée en dehors des
erreurs d'implémentation. Des efforts sont faits pour la vérification
formelle de ssh, mais à ma connaissance, personne ne s'est encore
intéressé aux problèmes d'implantations.
Mais encore une fois, la vérification n'a pas prétention aujourd'hui
de vérifier l'existant en C, mais de vérifier les systèmes à concevoir
et les protocoles à un certain niveau d'abstraction. Certains croient
pouvoir s'en passer et se sont plantés magistralement (cf ci-dessus),
d'autres ont fait des recherche et cela tient.
Quand on veut mettre au point un système d'apparence particulièrement
simple (un protocole) destiné à être utilisé par des milliers de
personnes, on a le bon goût de s'assurer formellement que ce système
est sûr jusqu'à un certain niveau.
Avant 95, la très grande majorité des protocoles cryptos, même très
simples, se sont avérés _faux_. Bizarrement, cela coïncide avec le
début de la vérification dans ce domaine.
Tu crois pas que tu pousses le bouchon un peu loin sur les vertus de
ta recherche? Si je connais rien en informatique, pour te faire
plaisir, il y a une chose que je connais, c'est comment on fait pour
justifier des choses qui ne servent à rien en disant qu'elles sont
d'une utilité fondamentale, dans le domaine de la recherche.
Tes seuls arguments est que la vérification de programme arbitraire en
C est imparfaite. Je vais t'économiser beaucoup de salive, c'est un
problème totalement indécidable. Tu n'auras jamais aucun programme
capable d'une telle prouesse. Je ne vois toujours pas en quoi ce seul
et unique argument est une preuve de quoi que ce soit puisque c'est
une partie infime de la vérification.
Quant au fait que tu sois béotien complet et que cela justifie donc
que la vérification n'est que foutaises, c'est un lien logique qui
m'échappe, d'autant que j'ai patiemment argumenté sur chacun des posts
en te donnant de _nombreux_ exemples où la vérification est utilisée
dans des domaines que tu croises tous les jours, mais comme tu es
particulièrement borné, tu reviens toujours à ton programme en C sans
te rendre compte que ce n'est pas le domaine principal de la
vérification tout simplement parce que tu n'y connais absolument rien
(et en plus ne possède a priori pas les facultés d'ouverture
nécessaire à comprendre qu'un programme en C n'est pas la seule
modélisation d'un système possible) mais que tu fais partie de la
masse des prétentieux qui croient tout connaître et tout pouvoir juger
parce qu'ils ont un ordinateur à eux.
--
#ifdef STUPIDLY_TRUST_BROKEN_PCMD_ENA_BIT
2.4.0-test2 /usr/src/linux/drivers/ide/cmd640.c
OoO Lors de la soirée naissante du mardi 27 janvier 2004, vers 18:55, (Michel Talon) disait:
Ça donne le 802.11b, le GSM, SSLv2, les Microsofteries et tout un tas d'autres vastes blagues au niveau de la sécu parce qu'ils n'y connaissaient rien en vérification.
Theo de Raadt il a utilisé la vérification pour faire son business?
Non et on trouve des failles dans OpenSSH. SSLv3 a été vérifié formellement et à ce jour, aucune faille n'a été trouvée en dehors des erreurs d'implémentation. Des efforts sont faits pour la vérification formelle de ssh, mais à ma connaissance, personne ne s'est encore intéressé aux problèmes d'implantations.
Mais encore une fois, la vérification n'a pas prétention aujourd'hui de vérifier l'existant en C, mais de vérifier les systèmes à concevoir et les protocoles à un certain niveau d'abstraction. Certains croient pouvoir s'en passer et se sont plantés magistralement (cf ci-dessus), d'autres ont fait des recherche et cela tient.
Quand on veut mettre au point un système d'apparence particulièrement simple (un protocole) destiné à être utilisé par des milliers de personnes, on a le bon goût de s'assurer formellement que ce système est sûr jusqu'à un certain niveau.
Avant 95, la très grande majorité des protocoles cryptos, même très simples, se sont avérés _faux_. Bizarrement, cela coïncide avec le début de la vérification dans ce domaine.
Tu crois pas que tu pousses le bouchon un peu loin sur les vertus de ta recherche? Si je connais rien en informatique, pour te faire plaisir, il y a une chose que je connais, c'est comment on fait pour justifier des choses qui ne servent à rien en disant qu'elles sont d'une utilité fondamentale, dans le domaine de la recherche.
Tes seuls arguments est que la vérification de programme arbitraire en C est imparfaite. Je vais t'économiser beaucoup de salive, c'est un problème totalement indécidable. Tu n'auras jamais aucun programme capable d'une telle prouesse. Je ne vois toujours pas en quoi ce seul et unique argument est une preuve de quoi que ce soit puisque c'est une partie infime de la vérification.
Quant au fait que tu sois béotien complet et que cela justifie donc que la vérification n'est que foutaises, c'est un lien logique qui m'échappe, d'autant que j'ai patiemment argumenté sur chacun des posts en te donnant de _nombreux_ exemples où la vérification est utilisée dans des domaines que tu croises tous les jours, mais comme tu es particulièrement borné, tu reviens toujours à ton programme en C sans te rendre compte que ce n'est pas le domaine principal de la vérification tout simplement parce que tu n'y connais absolument rien (et en plus ne possède a priori pas les facultés d'ouverture nécessaire à comprendre qu'un programme en C n'est pas la seule modélisation d'un système possible) mais que tu fais partie de la masse des prétentieux qui croient tout connaître et tout pouvoir juger parce qu'ils ont un ordinateur à eux. -- #ifdef STUPIDLY_TRUST_BROKEN_PCMD_ENA_BIT 2.4.0-test2 /usr/src/linux/drivers/ide/cmd640.c
Vincent Bernat
OoO Pendant le journal télévisé du mardi 27 janvier 2004, vers 20:19, Azathoth disait:
Je t'ai donné des exemples bien plus convaincants puisque la vérification est utilisée par de gros industriels. Seulement, ils ne se font pas d'illusion, cela reste un domaine spécifique.
Justement, ce qui peut interresser le lecteur lambda comme moi c'est de savoir quand ce truc fonctionne à un niveau acceptable aujourd'hui, puisqu'une verification dont on est pas sur, c'est nettement moins interressant.
La vérification, c'est une preuve. Je ne connais à ce jour rien de plus sûr qu'une preuve : tu peux la vérifier toi même ou demander à quelqu'un qui s'y connaît mieux de la vérifier. Maintenant, tu peux coller les mêmes arguments que pour la présence du code source.
Maintenant, comme je l'ai dit au moins 4 fois, la vérification n'est ni pour l'utilisateur lambda, ni pour le responsable informatique, elle est destinée aux concepteurs de systèmes dont certains aspects (ceux que l'on va vérifier) sont critiques. Cf les nombreux exemples éparpillés à travers ce thread. -- I WILL NOT DO MATH IN CLASS I WILL NOT DO MATH IN CLASS I WILL NOT DO MATH IN CLASS -+- Lisa Simpson on chalkboard in episode BABF07
OoO Pendant le journal télévisé du mardi 27 janvier 2004, vers 20:19,
Azathoth <azathoth@alussinan.org> disait:
Je t'ai donné des exemples bien plus convaincants puisque la
vérification est utilisée par de gros industriels. Seulement, ils
ne se font pas d'illusion, cela reste un domaine spécifique.
Justement, ce qui peut interresser le lecteur lambda comme moi c'est
de savoir quand ce truc fonctionne à un niveau acceptable
aujourd'hui, puisqu'une verification dont on est pas sur, c'est
nettement moins interressant.
La vérification, c'est une preuve. Je ne connais à ce jour rien de
plus sûr qu'une preuve : tu peux la vérifier toi même ou demander à
quelqu'un qui s'y connaît mieux de la vérifier. Maintenant, tu peux
coller les mêmes arguments que pour la présence du code source.
Maintenant, comme je l'ai dit au moins 4 fois, la vérification n'est
ni pour l'utilisateur lambda, ni pour le responsable informatique,
elle est destinée aux concepteurs de systèmes dont certains aspects
(ceux que l'on va vérifier) sont critiques. Cf les nombreux exemples
éparpillés à travers ce thread.
--
I WILL NOT DO MATH IN CLASS
I WILL NOT DO MATH IN CLASS
I WILL NOT DO MATH IN CLASS
-+- Lisa Simpson on chalkboard in episode BABF07
OoO Pendant le journal télévisé du mardi 27 janvier 2004, vers 20:19, Azathoth disait:
Je t'ai donné des exemples bien plus convaincants puisque la vérification est utilisée par de gros industriels. Seulement, ils ne se font pas d'illusion, cela reste un domaine spécifique.
Justement, ce qui peut interresser le lecteur lambda comme moi c'est de savoir quand ce truc fonctionne à un niveau acceptable aujourd'hui, puisqu'une verification dont on est pas sur, c'est nettement moins interressant.
La vérification, c'est une preuve. Je ne connais à ce jour rien de plus sûr qu'une preuve : tu peux la vérifier toi même ou demander à quelqu'un qui s'y connaît mieux de la vérifier. Maintenant, tu peux coller les mêmes arguments que pour la présence du code source.
Maintenant, comme je l'ai dit au moins 4 fois, la vérification n'est ni pour l'utilisateur lambda, ni pour le responsable informatique, elle est destinée aux concepteurs de systèmes dont certains aspects (ceux que l'on va vérifier) sont critiques. Cf les nombreux exemples éparpillés à travers ce thread. -- I WILL NOT DO MATH IN CLASS I WILL NOT DO MATH IN CLASS I WILL NOT DO MATH IN CLASS -+- Lisa Simpson on chalkboard in episode BABF07
Alexis Guillaume
Alexis Guillaume , dans le message , a écrit :
Ce n'est pas précisé dans cette [###CENSURE###] de page info non plus. :-/
Si, dans Choosing, Wildcards.
C'est vrai que je suis un boulet, je me sers des pages infos comme si c'était des pages man : recherche puis lecture diagonale des trois lignes qui suivent la première occurence, sans lire le roman qui suit sur les subtilités de l'option. J'ai une dent contre info parce que ce n'est qu'une vile fourberie de Stallman pour accoutumer les gens à emacs tellement ça y ressemble. J'ai essayé de passer à pinfo mais trop tard : le traumatisme s'est installé. Je suis infophobe. ;-)
-- Alexis Guillaume <http://cowsoft.free.fr> : ressources universitaires en vrac
"Il est minuit. La pluie fouette les vitres."
Alexis Guillaume , dans le message
<slrnc1dp01.g1a.alek@volfoni-brothers.org>, a écrit :
Ce n'est
pas précisé dans cette [###CENSURE###] de page info non plus. :-/
Si, dans Choosing, Wildcards.
C'est vrai que je suis un boulet, je me sers des pages infos comme si
c'était des pages man : recherche puis lecture diagonale des trois
lignes qui suivent la première occurence, sans lire le roman qui suit
sur les subtilités de l'option.
J'ai une dent contre info parce que ce n'est qu'une vile fourberie de
Stallman pour accoutumer les gens à emacs tellement ça y ressemble. J'ai
essayé de passer à pinfo mais trop tard : le traumatisme s'est installé.
Je suis infophobe. ;-)
--
Alexis Guillaume
<http://cowsoft.free.fr> : ressources universitaires en vrac
Ce n'est pas précisé dans cette [###CENSURE###] de page info non plus. :-/
Si, dans Choosing, Wildcards.
C'est vrai que je suis un boulet, je me sers des pages infos comme si c'était des pages man : recherche puis lecture diagonale des trois lignes qui suivent la première occurence, sans lire le roman qui suit sur les subtilités de l'option. J'ai une dent contre info parce que ce n'est qu'une vile fourberie de Stallman pour accoutumer les gens à emacs tellement ça y ressemble. J'ai essayé de passer à pinfo mais trop tard : le traumatisme s'est installé. Je suis infophobe. ;-)
-- Alexis Guillaume <http://cowsoft.free.fr> : ressources universitaires en vrac
"Il est minuit. La pluie fouette les vitres."
Alexis Guillaume
Chez moi j'ai : --exclude PATTERN exclude files matching PATTERN
Moi c'est sur Debian stable.
Je suis en unstable. Comme quoi les pages man sont bien mises à jour parfois. ;-)
-- Alexis Guillaume <http://cowsoft.free.fr> : ressources universitaires en vrac
"Il est minuit. La pluie fouette les vitres."
Chez moi j'ai :
--exclude PATTERN
exclude files matching PATTERN
Moi c'est sur Debian stable.
Je suis en unstable. Comme quoi les pages man sont bien mises à jour
parfois. ;-)
--
Alexis Guillaume
<http://cowsoft.free.fr> : ressources universitaires en vrac
Chez moi j'ai : --exclude PATTERN exclude files matching PATTERN
Moi c'est sur Debian stable.
Je suis en unstable. Comme quoi les pages man sont bien mises à jour parfois. ;-)
-- Alexis Guillaume <http://cowsoft.free.fr> : ressources universitaires en vrac
"Il est minuit. La pluie fouette les vitres."
Azathoth
Vincent Bernat wrote in news::
La vérification, c'est une preuve. Je ne connais à ce jour rien de plus sûr qu'une preuve : tu peux la vérifier toi même ou demander à quelqu'un qui s'y connaît mieux de la vérifier. Maintenant, tu peux coller les mêmes arguments que pour la présence du code source.
Oui mais justement : il semble que la vérification ne soit pas au point dans tous les domaines à lire le thread. Donc ma question : dans quels domaines la vérification est elle valide ?
Maintenant, comme je l'ai dit au moins 4 fois, la vérification n'est ni pour l'utilisateur lambda, ni pour le responsable informatique, elle est destinée aux concepteurs de systèmes dont certains aspects (ceux que l'on va vérifier) sont critiques.
Tu sais des systèmes que l'on qualifie de "critique" je peux t'en trouver plein.Ce qui m'interresse c'est de savoir à partir de quels critères je peux dire "oui je peux utiliser la vérification pour concevoir ce système de façon sure" et avec lesquels je dois dire "non la verification dans ce domaine n'en est qu'a ses débuts, je devrais plutot essayer autre chose pour l'instant".
Vincent Bernat <vince@khabale.org> wrote in
news:m3znc97ym0.fsf@neo.loria:
La vérification, c'est une preuve. Je ne connais à ce jour rien de
plus sûr qu'une preuve : tu peux la vérifier toi même ou demander à
quelqu'un qui s'y connaît mieux de la vérifier. Maintenant, tu peux
coller les mêmes arguments que pour la présence du code source.
Oui mais justement : il semble que la vérification ne soit pas au point
dans tous les domaines à lire le thread. Donc ma question : dans quels
domaines la vérification est elle valide ?
Maintenant, comme je l'ai dit au moins 4 fois, la vérification n'est
ni pour l'utilisateur lambda, ni pour le responsable informatique,
elle est destinée aux concepteurs de systèmes dont certains aspects
(ceux que l'on va vérifier) sont critiques.
Tu sais des systèmes que l'on qualifie de "critique" je peux t'en
trouver plein.Ce qui m'interresse c'est de savoir à partir de quels
critères je peux dire "oui je peux utiliser la vérification pour
concevoir ce système de façon sure" et avec lesquels je dois dire "non
la verification dans ce domaine n'en est qu'a ses débuts, je devrais
plutot essayer autre chose pour l'instant".
La vérification, c'est une preuve. Je ne connais à ce jour rien de plus sûr qu'une preuve : tu peux la vérifier toi même ou demander à quelqu'un qui s'y connaît mieux de la vérifier. Maintenant, tu peux coller les mêmes arguments que pour la présence du code source.
Oui mais justement : il semble que la vérification ne soit pas au point dans tous les domaines à lire le thread. Donc ma question : dans quels domaines la vérification est elle valide ?
Maintenant, comme je l'ai dit au moins 4 fois, la vérification n'est ni pour l'utilisateur lambda, ni pour le responsable informatique, elle est destinée aux concepteurs de systèmes dont certains aspects (ceux que l'on va vérifier) sont critiques.
Tu sais des systèmes que l'on qualifie de "critique" je peux t'en trouver plein.Ce qui m'interresse c'est de savoir à partir de quels critères je peux dire "oui je peux utiliser la vérification pour concevoir ce système de façon sure" et avec lesquels je dois dire "non la verification dans ce domaine n'en est qu'a ses débuts, je devrais plutot essayer autre chose pour l'instant".
Vincent Bernat
OoO En cette aube naissante du mercredi 28 janvier 2004, vers 07:32, Azathoth disait:
La vérification, c'est une preuve. Je ne connais à ce jour rien de plus sûr qu'une preuve : tu peux la vérifier toi même ou demander à quelqu'un qui s'y connaît mieux de la vérifier. Maintenant, tu peux coller les mêmes arguments que pour la présence du code source.
Oui mais justement : il semble que la vérification ne soit pas au point dans tous les domaines à lire le thread. Donc ma question : dans quels domaines la vérification est elle valide ?
Dans les domaines où tu peux construire ton système à partir d'un quelconque (presque) modèle formel. Ça inclut les exemples que j'ai donnés auparavant, ça inclut les logiciels si l'auteur veut se casser la tête à les vérifier, cela inclut les protocoles existants déjà, mais cela exclut les programmes déjà faits et trop complexes (à moins de vouloir les réécrire de 0), à moins de les réécrire de 0 en passant par un modèle formel. C'est extrêmement large, mais cela nécessite de passer par une modélisation qui est coûteuse si on doit la faire depuis l'existant.
Dans les protocoles, on vérifie aussi bien ceux qui assurent un secret, ceux qui assurent certaines formes d'authentification, ceux qui permettent de voter, ceux qui permettent de signer un contrat et on se rapproche le plus possible de la réalité en incluant éventuellement certaines propriétés algébriques des algorithmes de chiffrement sous-jacents (considérés sinon comme parfaits).
Ensuite, tu peux vérifier des systèmes modélisés par des automates ou des automates d'arbre ou encore des systèmes de transitions symboliques. Il y a beaucoup d'exemples basiques dans ce domaine, mais les exemples réels existent et forment des automates à plusieurs millions d'états vérifiés ensuite automatiquement. On se rapproche de la programmation conventionnelle en utilisant des algèbres de processus sur lesquels on dispose également d'outils automatiques pour vérifier (mais comme le problème est la plupart du temps indécidable, cela peut ne pas terminer).
Tiens, j'ai un autre exemple qui me vient sous la main : la vérification de la cohérence des caches dans un système distribué (par exemple une machine SMP). On y a trouvé des bugs mais aussi des systèmes justes du premier coup.
Et un autre exemple qui va bien dans ce groupe : la vérification des smart cards programmées en Java.
Mais la vérification est invisible du grand public, il s'agit d'un test de qualité comme un autre. -- BOFH excuse #249: Unfortunately we have run out of bits/bytes/whatever. Don't worry, the next supply will be coming next week.
OoO En cette aube naissante du mercredi 28 janvier 2004, vers 07:32,
Azathoth <azathoth@alussinan.org> disait:
La vérification, c'est une preuve. Je ne connais à ce jour rien de
plus sûr qu'une preuve : tu peux la vérifier toi même ou demander à
quelqu'un qui s'y connaît mieux de la vérifier. Maintenant, tu peux
coller les mêmes arguments que pour la présence du code source.
Oui mais justement : il semble que la vérification ne soit pas au point
dans tous les domaines à lire le thread. Donc ma question : dans quels
domaines la vérification est elle valide ?
Dans les domaines où tu peux construire ton système à partir d'un
quelconque (presque) modèle formel. Ça inclut les exemples que j'ai
donnés auparavant, ça inclut les logiciels si l'auteur veut se casser
la tête à les vérifier, cela inclut les protocoles existants déjà,
mais cela exclut les programmes déjà faits et trop complexes (à moins
de vouloir les réécrire de 0), à moins de les réécrire de 0 en passant
par un modèle formel. C'est extrêmement large, mais cela nécessite de
passer par une modélisation qui est coûteuse si on doit la faire
depuis l'existant.
Dans les protocoles, on vérifie aussi bien ceux qui assurent un
secret, ceux qui assurent certaines formes d'authentification, ceux
qui permettent de voter, ceux qui permettent de signer un contrat et
on se rapproche le plus possible de la réalité en incluant
éventuellement certaines propriétés algébriques des algorithmes de
chiffrement sous-jacents (considérés sinon comme parfaits).
Ensuite, tu peux vérifier des systèmes modélisés par des automates ou
des automates d'arbre ou encore des systèmes de transitions
symboliques. Il y a beaucoup d'exemples basiques dans ce domaine,
mais les exemples réels existent et forment des automates à plusieurs
millions d'états vérifiés ensuite automatiquement. On se rapproche de
la programmation conventionnelle en utilisant des algèbres de
processus sur lesquels on dispose également d'outils automatiques pour
vérifier (mais comme le problème est la plupart du temps indécidable,
cela peut ne pas terminer).
Tiens, j'ai un autre exemple qui me vient sous la main : la
vérification de la cohérence des caches dans un système distribué (par
exemple une machine SMP). On y a trouvé des bugs mais aussi des
systèmes justes du premier coup.
Et un autre exemple qui va bien dans ce groupe : la vérification des
smart cards programmées en Java.
Mais la vérification est invisible du grand public, il s'agit d'un
test de qualité comme un autre.
--
BOFH excuse #249: Unfortunately we have run out of
bits/bytes/whatever. Don't worry, the next supply will be coming next
week.
OoO En cette aube naissante du mercredi 28 janvier 2004, vers 07:32, Azathoth disait:
La vérification, c'est une preuve. Je ne connais à ce jour rien de plus sûr qu'une preuve : tu peux la vérifier toi même ou demander à quelqu'un qui s'y connaît mieux de la vérifier. Maintenant, tu peux coller les mêmes arguments que pour la présence du code source.
Oui mais justement : il semble que la vérification ne soit pas au point dans tous les domaines à lire le thread. Donc ma question : dans quels domaines la vérification est elle valide ?
Dans les domaines où tu peux construire ton système à partir d'un quelconque (presque) modèle formel. Ça inclut les exemples que j'ai donnés auparavant, ça inclut les logiciels si l'auteur veut se casser la tête à les vérifier, cela inclut les protocoles existants déjà, mais cela exclut les programmes déjà faits et trop complexes (à moins de vouloir les réécrire de 0), à moins de les réécrire de 0 en passant par un modèle formel. C'est extrêmement large, mais cela nécessite de passer par une modélisation qui est coûteuse si on doit la faire depuis l'existant.
Dans les protocoles, on vérifie aussi bien ceux qui assurent un secret, ceux qui assurent certaines formes d'authentification, ceux qui permettent de voter, ceux qui permettent de signer un contrat et on se rapproche le plus possible de la réalité en incluant éventuellement certaines propriétés algébriques des algorithmes de chiffrement sous-jacents (considérés sinon comme parfaits).
Ensuite, tu peux vérifier des systèmes modélisés par des automates ou des automates d'arbre ou encore des systèmes de transitions symboliques. Il y a beaucoup d'exemples basiques dans ce domaine, mais les exemples réels existent et forment des automates à plusieurs millions d'états vérifiés ensuite automatiquement. On se rapproche de la programmation conventionnelle en utilisant des algèbres de processus sur lesquels on dispose également d'outils automatiques pour vérifier (mais comme le problème est la plupart du temps indécidable, cela peut ne pas terminer).
Tiens, j'ai un autre exemple qui me vient sous la main : la vérification de la cohérence des caches dans un système distribué (par exemple une machine SMP). On y a trouvé des bugs mais aussi des systèmes justes du premier coup.
Et un autre exemple qui va bien dans ce groupe : la vérification des smart cards programmées en Java.
Mais la vérification est invisible du grand public, il s'agit d'un test de qualité comme un autre. -- BOFH excuse #249: Unfortunately we have run out of bits/bytes/whatever. Don't worry, the next supply will be coming next week.
Patrice Karatchentzeff
(Nicolas George) writes:
Patrice Karatchentzeff , dans le message , a écrit :
You're welcome : on manque justement de bras...
J'ai proposé un patch il y a plusieurs mois, pour ajouter la gestion des man DocBook de Solaris : je n'ai jamais eu de réponse. Ça n'engage pas à participer.
Tu as envoyé quoi exactement à qui ? Si tu a vraiment envie de participer, n'hésite pas à venir sur debian-l10n-french : il y a tout plein de choses à faire... et on ne refuse aucune aide.
Patrice Karatchentzeff , dans le message
<87u12hozna.fsf@belledonne.chartreuse.fr>, a écrit :
You're welcome : on manque justement de bras...
J'ai proposé un patch il y a plusieurs mois, pour ajouter la gestion des
man DocBook de Solaris : je n'ai jamais eu de réponse. Ça n'engage pas
à participer.
Tu as envoyé quoi exactement à qui ? Si tu a vraiment envie de
participer, n'hésite pas à venir sur debian-l10n-french : il y a tout
plein de choses à faire... et on ne refuse aucune aide.
Patrice Karatchentzeff , dans le message , a écrit :
You're welcome : on manque justement de bras...
J'ai proposé un patch il y a plusieurs mois, pour ajouter la gestion des man DocBook de Solaris : je n'ai jamais eu de réponse. Ça n'engage pas à participer.
Tu as envoyé quoi exactement à qui ? Si tu a vraiment envie de participer, n'hésite pas à venir sur debian-l10n-french : il y a tout plein de choses à faire... et on ne refuse aucune aide.
-- Quis, quid, ubi, quibus auxiliis, cur, quomodo, quando?
Emmanuel Florac
Dans article , disait...
C'est faux. Les scientifiques sérieux savent que ce n'était nullement un canular et que les Bogdanoff ont fait un travail important.
C'est éxagéré. Disons qu'ils ont fait une thèse de physique parfaitement recevable, qu'ils ont été reçu, et voilà, il n'y a pas de quoi fouetter un chat, ils ne sont pas les seuls.
-- Quis, quid, ubi, quibus auxiliis, cur, quomodo, quando?
Dans article <b241639c.0401271532.7b92b231@posting.google.com>,
golovine@netlimit.com disait...
C'est faux. Les scientifiques sérieux savent que ce n'était nullement
un canular et que les Bogdanoff ont fait un travail important.
C'est éxagéré. Disons qu'ils ont fait une thèse de physique parfaitement
recevable, qu'ils ont été reçu, et voilà, il n'y a pas de quoi fouetter
un chat, ils ne sont pas les seuls.
--
Quis, quid, ubi, quibus auxiliis, cur, quomodo, quando?
C'est faux. Les scientifiques sérieux savent que ce n'était nullement un canular et que les Bogdanoff ont fait un travail important.
C'est éxagéré. Disons qu'ils ont fait une thèse de physique parfaitement recevable, qu'ils ont été reçu, et voilà, il n'y a pas de quoi fouetter un chat, ils ne sont pas les seuls.
-- Quis, quid, ubi, quibus auxiliis, cur, quomodo, quando?
george
Patrice Karatchentzeff , dans le message , a écrit :
Tu as envoyé quoi exactement à qui ?
À Andries Brouwer , c'est à dire le mainteneur actuel du programme.
Si tu a vraiment envie de participer, n'hésite pas à venir sur debian-l10n-french : il y a tout plein de choses à faire... et on ne refuse aucune aide.
À vrai dire, la traduction des logiciels est quelque chose que je trouve d'une utilité très secondaire. Un jour (tm), je prendrai surtout le temps de voir ce qu'il faut faire pour proposer un vrai paquet propre de Termim, qui est à mon avis largement plus utile que des pages de man traduites en français.
Patrice Karatchentzeff , dans le message
<87oesopain.fsf@belledonne.chartreuse.fr>, a écrit :
Tu as envoyé quoi exactement à qui ?
À Andries Brouwer <aeb@cwi.nl>, c'est à dire le mainteneur actuel du
programme.
Si tu a vraiment envie de
participer, n'hésite pas à venir sur debian-l10n-french : il y a tout
plein de choses à faire... et on ne refuse aucune aide.
À vrai dire, la traduction des logiciels est quelque chose que je trouve
d'une utilité très secondaire. Un jour (tm), je prendrai surtout le
temps de voir ce qu'il faut faire pour proposer un vrai paquet propre de
Termim, qui est à mon avis largement plus utile que des pages de man
traduites en français.
Patrice Karatchentzeff , dans le message , a écrit :
Tu as envoyé quoi exactement à qui ?
À Andries Brouwer , c'est à dire le mainteneur actuel du programme.
Si tu a vraiment envie de participer, n'hésite pas à venir sur debian-l10n-french : il y a tout plein de choses à faire... et on ne refuse aucune aide.
À vrai dire, la traduction des logiciels est quelque chose que je trouve d'une utilité très secondaire. Un jour (tm), je prendrai surtout le temps de voir ce qu'il faut faire pour proposer un vrai paquet propre de Termim, qui est à mon avis largement plus utile que des pages de man traduites en français.
