T'es en train de dire que faire une spécification correcte est plus dur que faire du code incorrect ? J'ai envie de dire que c'est un bon moyen de botter en touche. La gestion d'erreur, oui c'est pas ce qu'il y a de plus facile à coder c'est évident … Après de là à faire attention aux preuves j'ai envie de dire qu'avec des arguments pareils on bouge pas d'un pouce, wtf ?
Il n'y a rien qui ressemble plus à un script d'init qu'un autre script d'init. C'est peut être ''facile'' à debugger, mais c'est encore plus facile de ne pas avoir à l'écrire. Sur la trace, elle est inscrite dans le code, on peut laisser un commentaire, il y a des tests de non régression … Tu veux comparer ça avec un nième problème d'écriture d'init script pour un nouveau service qui a finalement exactement les mêmes problèmes que les autres, ou alors pas les mêmes problèmes que les autres et pour leuquel on va copier/coller un script standard qui marche pas (ou qui a l'air de marcher …) ?
Si c'est pour debugger encore et toujours les mêmes bugs, ou laisser des problèmes de fond traîner sous prétexte que c'est simple à debugger, ça ne vaut pas le coût. Autant mutualiser le tout proprement, debugger et laisser une trace de l'expérience dans le code mutualisé.
Par ailleurs (je repond un commentaire, peux plus éditer), le nom du projet "Core infrastructure" est un peu énigmatique et laisse présager un projet ambitieux. Dans quel sens ? C'est toute la question mais j'ai tendance qu'ils sont partis pour prendre le problème globalement.
Ben je parlais ici de preuve de l'implémentation évidemment. Après c'est sur qu'il faut aussi que l'OS, le compilateur et le CPU soient prouvés, et tous ces chercheurs le savent.
Mais au moins, pas de bug dans l'implémentation, c'est toujours ça de pris. Un buffer overflow en 2014 c'est à pleurer, quand même.
À ce sujet par simple curiosité, comment est fait l'import sur Wikipédia ? Théoriquement il faudrait citer les différents auteurs, ou genre faire un compte Framasoft et faire l'édition avec, avec genre un petit mot pour citer les auteurs, ou vous vous embêtez pas avec l'attribution ?
Ben c'est peut être en train de changer, mais cette culture coopérative, travailler avec d'autres pour reverser le travail de manière à ce que tout le monde en profite, c'est un peu la stratégie inverse de ce que Microsoft faisait traditionnellement depuis plusieurs années.
Évidemment il le font très probablement plutôt par culture open source et parce qu'ils y ont quelque chose à gagner, que la compétition sur le domaine de la sécurité n'est pas forcément un truc qui tourne énormément le grand public, qu'ils sont en retard sur certaines choses et qu'ils ont plutôt intérêt à récupérer ce qui se fait collaborativement plutôt que de joueur les égoïste sur ce point.
N'empêche que voilà, on peut avoir l'impression qu'ils ont été poussés dans leur retranchement et qu'ils sont allés au bout des logiques de lobbying sur le BSA pour protéger leurs acquis avant de penser à joueur le jeu autrement.
Fiction, ils vont sortir de leurs labos les Leslie Lamport et autres spécialistes des méthodes formelles de l'INRIA et ils vont pondre une infrastructure prouvée mathématiquement en formant quelques devs et ingés au passage.
Le KGB et la NSA sont tellement passées maîtres dans l'infiltration et l'espionnage que je pense qu'on peut les considérer comme une seule et même entité.
C'est ce que fait la méthode B, les spécifications générales sont faite dans le même langages, ensuite on comble les trous en implémentant petit à petit, et en vérifiant que ce qu'on a écrit correspond bien avec ce qu'on a écrit à l'étape de ''raffinage'' précédente.
Ça m'a fait un peu penser au système de ''trou'' dans le code que la dernière version d'Haskell a introduit, cf. la dépêche : on a des bouts de code pas implémenté, mais le compilo donne le type de ce qui reste à faire.
PS: je crois que je viens de trouver un bug : il y a
Vous avez jugé ce commentaire inutile. qui s'affiche sur ma page, mais un seul +1 pour le commentaire, et je pense avoir cliqué sur pertinent.
La boite qui fait le site http://www.methode-b.com/ en vit, ça a produit le code de la ligne de métro automatisée à Paris.
Sinon je dirai que ça demande des compétences qui sont pas celles du codeur de site PHP moyen, mais dans le domaine de la sécurité il y a des passionnés qui devraient s'y intéresser, c'est évident. Les méthodes formelles ont jusqu'à présent peinées à s'imposer, faute au surcout perçu et à la difficulter de former des gens (la méthode B était enseignée dans l'IUT de Nantes ou j'ai fait mon DUT, la plupart des têtes de l'amphi étaient un peu paumées bien qu'on ait rien fait de bien compliquée, faute au choc des cultures plus qu'à une réelle complexité je pense, et bien que le prof (avec une personnalité particulière et pas forcément adapté à la pédagogie) ait beaucoup réfléchi à la question de la transmission.
Il suffit de regarder le décallage entre le récent prix Turing et ses article ou il déplore qu'on cherche pas à écrire des specs potables pour démontrer que le code les vérifie : http://www.wired.com/2013/01/code-bugs-programming-why-we-need-specs/ idées qui sont jamais trop passées dans l'industrie de masse. Mais qui sais, le temps est peut être venu ?
Pour le C, je crois qu'il y a des normes industrielles, et juste une requête google "j'ai de la chance" donne ça par exemple : http://vst.cs.princeton.edu/veric/
C'est vrai que techniquement c'est pas si difficile, mais les discussions sur les intégrations plus compliquées genre le wiktionnaire et la gestion des méta données de commons, qui sont quand même particulièrement intéressantes, sont pas tranchées encore. Pour les intégrations plus simple évidemment ça va plus vite une fois rodé.
Entre quelques requêtes fait par des technophiles sur des données vieilles de plusieurs jours
Pas vraiment, il me semble qu'il le fasse plutôt avec des données avec quelques minutes de retard.
Sinon oui effectivement, c'était quand même une idée un peu curieuse de gérer une queue de propagation avec une BDD SQL. Mais c'est de l'histoire ancienne pour le coup.
C'est dans les priorités mais il semble que l'équipe de dev manque de ressources pour aller plus vite. On peut déja construire des infoboxs, même si l'accès d'une page Wikipédia aux données de Wikidata est toujours limité aux données de son entité. La migrations des infoboxes ne semble pas très rapide par contre, faute de main d'oeuvre et d'attentisme du côté des Wikipédias.
De l'extérieur j'ai l'impression que l'équipe de dev est essentiellement constitué de développeurs avec relativement peu d'expérience, le code a été audité relativement récemment et des problèmes d'architecture ont étés trouvés, j'ai l'impression qu'ils ont du passer pas mal de temps en refactoring ces derniers temps, pour tenir la charge et s'intégrer au système de cache de mediawiki. Ils doivent travailler sur la propagation des changements sur les différents Wikis clients de manière efficace, et sur le tracking de 'qui utilise quelles données', dans les mêmes objectifs.
Ils ont aussi sans doute passé pas mal de temps en intégration avec les autres projets Wikimedias, alors qu'à l'origine ils devaient se concentrer sur Wikipédia, changement de plans en cours de route.
C'est un peu surprenant étant donné que wikidata query semble ne pas vraiment avoir de problèmes de performances, mais faut croire qu'il a moins de charge, et moins de contrainte d'intégrations dans le code du Wiki.
Je veux pas voter spécifiquement pour une liste qui ne produira que des candidats spécialisés dans le numérique. Certes c'est important le numérique mais il y a pleins d'autres sujets sur lesquels j'ai envie que ma voix ait une chance de compter.
Le comportement déclaratif il porte en général une sémantique qui fait que le compilateur doit nécessairement garantir des tas de propriétés qu'il font que c'est plus simple de vérifier, voire de prouver qu'il est exempt d'une certains classe de bugs. Pour l'implicite, je vois pas trop le rapport avec la hauteur du langage, les cast implicites il y en a en C et c'est pas toujours beau à voir.
[^] # Re: On verra
Posté par Thomas Douillard . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 5.
T'es en train de dire que faire une spécification correcte est plus dur que faire du code incorrect ? J'ai envie de dire que c'est un bon moyen de botter en touche. La gestion d'erreur, oui c'est pas ce qu'il y a de plus facile à coder c'est évident … Après de là à faire attention aux preuves j'ai envie de dire qu'avec des arguments pareils on bouge pas d'un pouce, wtf ?
[^] # Re: If it works, don't fix it.
Posté par Thomas Douillard . En réponse au journal Chronique des dinosaures rétrogrades. Évalué à 6.
Systemd peut lancer un script, non ?
[^] # Re: If it works, don't fix it.
Posté par Thomas Douillard . En réponse au journal Chronique des dinosaures rétrogrades. Évalué à 6.
Il n'y a rien qui ressemble plus à un script d'init qu'un autre script d'init. C'est peut être ''facile'' à debugger, mais c'est encore plus facile de ne pas avoir à l'écrire. Sur la trace, elle est inscrite dans le code, on peut laisser un commentaire, il y a des tests de non régression … Tu veux comparer ça avec un nième problème d'écriture d'init script pour un nouveau service qui a finalement exactement les mêmes problèmes que les autres, ou alors pas les mêmes problèmes que les autres et pour leuquel on va copier/coller un script standard qui marche pas (ou qui a l'air de marcher …) ?
[^] # Re: If it works, don't fix it.
Posté par Thomas Douillard . En réponse au journal Chronique des dinosaures rétrogrades. Évalué à 10.
Si c'est pour debugger encore et toujours les mêmes bugs, ou laisser des problèmes de fond traîner sous prétexte que c'est simple à debugger, ça ne vaut pas le coût. Autant mutualiser le tout proprement, debugger et laisser une trace de l'expérience dans le code mutualisé.
[^] # Re: On verra
Posté par Thomas Douillard . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 2.
On peut imaginer plus, genre l'infrastructure de compilation sur les questions de sécurité.
[^] # Re: On verra
Posté par Thomas Douillard . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 2.
Par ailleurs (je repond un commentaire, peux plus éditer), le nom du projet "Core infrastructure" est un peu énigmatique et laisse présager un projet ambitieux. Dans quel sens ? C'est toute la question mais j'ai tendance qu'ils sont partis pour prendre le problème globalement.
[^] # Re: On verra
Posté par Thomas Douillard . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 4.
Ben je parlais ici de preuve de l'implémentation évidemment. Après c'est sur qu'il faut aussi que l'OS, le compilateur et le CPU soient prouvés, et tous ces chercheurs le savent.
Mais au moins, pas de bug dans l'implémentation, c'est toujours ça de pris. Un buffer overflow en 2014 c'est à pleurer, quand même.
[^] # Re: Pourquoi utiliser un framapad?
Posté par Thomas Douillard . En réponse à la dépêche Appel à traduction et amélioration d'un article sur Wikipédia : liste des migrations vers GNU/Linux. Évalué à 4.
À ce sujet par simple curiosité, comment est fait l'import sur Wikipédia ? Théoriquement il faudrait citer les différents auteurs, ou genre faire un compte Framasoft et faire l'édition avec, avec genre un petit mot pour citer les auteurs, ou vous vous embêtez pas avec l'attribution ?
[^] # Re: C'est assez drole
Posté par Thomas Douillard . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 4.
Ben c'est peut être en train de changer, mais cette culture coopérative, travailler avec d'autres pour reverser le travail de manière à ce que tout le monde en profite, c'est un peu la stratégie inverse de ce que Microsoft faisait traditionnellement depuis plusieurs années.
Évidemment il le font très probablement plutôt par culture open source et parce qu'ils y ont quelque chose à gagner, que la compétition sur le domaine de la sécurité n'est pas forcément un truc qui tourne énormément le grand public, qu'ils sont en retard sur certaines choses et qu'ils ont plutôt intérêt à récupérer ce qui se fait collaborativement plutôt que de joueur les égoïste sur ce point.
N'empêche que voilà, on peut avoir l'impression qu'ils ont été poussés dans leur retranchement et qu'ils sont allés au bout des logiques de lobbying sur le BSA pour protéger leurs acquis avant de penser à joueur le jeu autrement.
[^] # Re: On verra
Posté par Thomas Douillard . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 10.
Fiction, ils vont sortir de leurs labos les Leslie Lamport et autres spécialistes des méthodes formelles de l'INRIA et ils vont pondre une infrastructure prouvée mathématiquement en formant quelques devs et ingés au passage.
[^] # Re: Et les algorithmes GOST ?
Posté par Thomas Douillard . En réponse au journal OpenSSL est mort, vive (le futur) LibreSSL. Évalué à 7.
Le KGB et la NSA sont tellement passées maîtres dans l'infiltration et l'espionnage que je pense qu'on peut les considérer comme une seule et même entité.
[^] # Re: Petit jeu en HTML5
Posté par Thomas Douillard . En réponse à la dépêche Petit jeu en HTML5 et découverte de Crafty. Évalué à -2.
Qui toune sous plateforme
* GNU/Linux/Xorg - Web/Javascript/CSS3/HTML5
* GNU/Linux/wayland - Web/Javascript/CSS3/HTML5
* Linux/Android - Chrome/Javascript/CSS3/HTML5
* Win32 - Chrome/Javascript/CSS3/HTML5
* …
[^] # Re: Vérification formelle
Posté par Thomas Douillard . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 2.
Sans compter les techniques d'interprétations abstraite qui peuvent prouver certains trucs aussi.
[^] # Re: Vérification formelle
Posté par Thomas Douillard . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 6. Dernière modification le 18 avril 2014 à 13:43.
C'est ce que fait la méthode B, les spécifications générales sont faite dans le même langages, ensuite on comble les trous en implémentant petit à petit, et en vérifiant que ce qu'on a écrit correspond bien avec ce qu'on a écrit à l'étape de ''raffinage'' précédente.
Ça m'a fait un peu penser au système de ''trou'' dans le code que la dernière version d'Haskell a introduit, cf. la dépêche : on a des bouts de code pas implémenté, mais le compilo donne le type de ce qui reste à faire.
PS: je crois que je viens de trouver un bug : il y a
Vous avez jugé ce commentaire inutile. qui s'affiche sur ma page, mais un seul +1 pour le commentaire, et je pense avoir cliqué sur pertinent.
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par Thomas Douillard . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 7.
Dans le genre méthodes formelles appliquées, il y a la méthode B, qui produit en sortie du C ou de l'ADA, avec tout démontré y compris le compilateur.
Méthode B
La boite qui fait le site http://www.methode-b.com/ en vit, ça a produit le code de la ligne de métro automatisée à Paris.
Sinon je dirai que ça demande des compétences qui sont pas celles du codeur de site PHP moyen, mais dans le domaine de la sécurité il y a des passionnés qui devraient s'y intéresser, c'est évident. Les méthodes formelles ont jusqu'à présent peinées à s'imposer, faute au surcout perçu et à la difficulter de former des gens (la méthode B était enseignée dans l'IUT de Nantes ou j'ai fait mon DUT, la plupart des têtes de l'amphi étaient un peu paumées bien qu'on ait rien fait de bien compliquée, faute au choc des cultures plus qu'à une réelle complexité je pense, et bien que le prof (avec une personnalité particulière et pas forcément adapté à la pédagogie) ait beaucoup réfléchi à la question de la transmission.
Il suffit de regarder le décallage entre le récent prix Turing et ses article ou il déplore qu'on cherche pas à écrire des specs potables pour démontrer que le code les vérifie : http://www.wired.com/2013/01/code-bugs-programming-why-we-need-specs/ idées qui sont jamais trop passées dans l'industrie de masse. Mais qui sais, le temps est peut être venu ?
[^] # Re: Les analyseurs ne sont pas non plus une panacee
Posté par Thomas Douillard . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 4.
Pour le C, je crois qu'il y a des normes industrielles, et juste une requête google "j'ai de la chance" donne ça par exemple : http://vst.cs.princeton.edu/veric/
[^] # Re: Ça existe ou ça a existé :
Posté par Thomas Douillard . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 3.
Ben si il passe dans le coin, faudrait qu'il nous donne des nouvelles :)
[^] # Re: euh...
Posté par Thomas Douillard . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 4.
J'aurai du mettre "naïve", c'est vrai :) Si ça se trouve j'étais déjà tombé sur le projet de Sylvestre et je m'en souviens pas /o.
[^] # Re: Utilisation des données de Wikidata
Posté par Thomas Douillard . En réponse au journal Chronique de Wikidata : Esprit Unix appliqué aux données, et plus encore.. Évalué à 3.
C'est vrai que techniquement c'est pas si difficile, mais les discussions sur les intégrations plus compliquées genre le wiktionnaire et la gestion des méta données de commons, qui sont quand même particulièrement intéressantes, sont pas tranchées encore. Pour les intégrations plus simple évidemment ça va plus vite une fois rodé.
Pas vraiment, il me semble qu'il le fasse plutôt avec des données avec quelques minutes de retard.
Sinon oui effectivement, c'était quand même une idée un peu curieuse de gérer une queue de propagation avec une BDD SQL. Mais c'est de l'histoire ancienne pour le coup.
[^] # Re: Utilisation des données de Wikidata
Posté par Thomas Douillard . En réponse au journal Chronique de Wikidata : Esprit Unix appliqué aux données, et plus encore.. Évalué à 9.
C'est dans les priorités mais il semble que l'équipe de dev manque de ressources pour aller plus vite. On peut déja construire des infoboxs, même si l'accès d'une page Wikipédia aux données de Wikidata est toujours limité aux données de son entité. La migrations des infoboxes ne semble pas très rapide par contre, faute de main d'oeuvre et d'attentisme du côté des Wikipédias.
De l'extérieur j'ai l'impression que l'équipe de dev est essentiellement constitué de développeurs avec relativement peu d'expérience, le code a été audité relativement récemment et des problèmes d'architecture ont étés trouvés, j'ai l'impression qu'ils ont du passer pas mal de temps en refactoring ces derniers temps, pour tenir la charge et s'intégrer au système de cache de mediawiki. Ils doivent travailler sur la propagation des changements sur les différents Wikis clients de manière efficace, et sur le tracking de 'qui utilise quelles données', dans les mêmes objectifs.
Ils ont aussi sans doute passé pas mal de temps en intégration avec les autres projets Wikimedias, alors qu'à l'origine ils devaient se concentrer sur Wikipédia, changement de plans en cours de route.
C'est un peu surprenant étant donné que wikidata query semble ne pas vraiment avoir de problèmes de performances, mais faut croire qu'il a moins de charge, et moins de contrainte d'intégrations dans le code du Wiki.
[^] # Re: Le lien vers le blog est mauvais.
Posté par Thomas Douillard . En réponse au journal Chronique de Wikidata : Esprit Unix appliqué aux données, et plus encore.. Évalué à 4.
oups, le lien correct : http://magnusmanske.de/wordpress/?p=189
[^] # Re: Trompé de site ?
Posté par Thomas Douillard . En réponse au journal Le Parti Pirate cherche 5 femmes pour les Européennes avant le 21 avril. Évalué à 2.
Administration et politique, cf. le dernier journal trollesque, le choc des clichés pique les yeux :)
[^] # Re: Et le programme ?
Posté par Thomas Douillard . En réponse au journal Le Parti Pirate cherche 5 femmes pour les Européennes avant le 21 avril. Évalué à 5.
Je veux pas voter spécifiquement pour une liste qui ne produira que des candidats spécialisés dans le numérique. Certes c'est important le numérique mais il y a pleins d'autres sujets sur lesquels j'ai envie que ma voix ait une chance de compter.
[^] # Re: Remplacer l'assembleur par Ada ou Rust ?
Posté par Thomas Douillard . En réponse à la dépêche Nouvelle vulnérabilité dans l’implémentation OpenSSL. Évalué à 6.
Le comportement déclaratif il porte en général une sémantique qui fait que le compilateur doit nécessairement garantir des tas de propriétés qu'il font que c'est plus simple de vérifier, voire de prouver qu'il est exempt d'une certains classe de bugs. Pour l'implicite, je vois pas trop le rapport avec la hauteur du langage, les cast implicites il y en a en C et c'est pas toujours beau à voir.
[^] # Re: Remplacer l'assembleur par Ada ou Rust ?
Posté par Thomas Douillard . En réponse à la dépêche Nouvelle vulnérabilité dans l’implémentation OpenSSL. Évalué à 4.
Ça isole un peu la partie du code à vérifier si on sait déja qu'il n'y a que là qu'il y a des risques d'en avoir.