Que les devs soient payés n'implique pas vraiment qu'ils aient beaucoup plus de comptes à te rendre. Je suis plutôt content qu'ils aient de l'argents pour pérenniser un peu leurs efforts, Firefox face à Chrome, Gimp face à Photoshop, aussi bien Firefox que Gimp ne jouent pas dans la même cour au niveau moyen que Google ou Adobe.
Oui et non, l'approche de la méthode B c'est d'écrire des specs et de vérifier que l'implémentation respecte bien les specs, et au passage qu'il n'y a pas de bug à la con comme des buffer overflow. Après comme toujours les specs ont des limites, on peut pas vérifier la cohérence d'un protocole cryptographique si on code seulement un client et un serveur indépendament en B. Ni que la précondition P=NP qui serait l'hypothétique garantie de la sécurité du protocole en question, mais on c'est pas parce qu'on fait du B qu'on est obligé d'essayer :) ~~~~
Pas du tout, si j'ai bien compris le principe de la faille, elle permet d'accéder à une zone mémoire qui ne devrait tout simplement pas être accessible. C'est pas une bête histoire de borne ?
Bien sur que si, déja si on peut garantir qu'il n'y a pas de bug d'implémentation type heartbleed c'est pas mal. Ça démontrera pas la totale correction du protocole c'est sur. À part ça, j'ai vu passer un récent ajout de modélisation système pour la méthode B sur l'article Wikipédia, je sais pas ce que ça recouvre et j'ai pas investigué, mais si ça se trouve ils s'intéressent à certaines problématiques de distribution.
Pour revenir a des choses plus terre à terre, la faille qui a provoqué tout ça elle n'a pas un nombre arbitraire de pairs et il s'agissait juste d'une erreur de validation des IOs :) On peut prouver des choses rien qu'en bétonnant les IO, évidemment c'est plus compliqué de valider Internet dans sa globalité.
La spec, dans la méthode B, elle est haut niveau au début du developpement et elle se précise au fur et à mesure (c'est le raffinage) justqu'à devenir compilable. Les trous dans la spec tu les détectes parce que c'est impossible de montrer que ton raffinage est compatible avec ce que tu as écris avant. Ils mettent le processus de spec et de preuve au coeur du développement.
C'est dur de prouver des systèmes distribués, certes, mais écrire du code correct et être sûr qu'il est correct c'est carrément ultra dur aussi. Il y a quand même des patterns connus pour prouver qu'un calcul distribué termine par exemple. On peut montrer aussi des propriétés d'autostabilisation ou des choses comme ça.
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.
[^] # Re: Vie privée et Piwik
Posté par thoasm . En réponse à la dépêche Un nouveau pelage pour Firefox 29. Évalué à 2. Dernière modification le 02 mai 2014 à 14:19.
Que les devs soient payés n'implique pas vraiment qu'ils aient beaucoup plus de comptes à te rendre. Je suis plutôt content qu'ils aient de l'argents pour pérenniser un peu leurs efforts, Firefox face à Chrome, Gimp face à Photoshop, aussi bien Firefox que Gimp ne jouent pas dans la même cour au niveau moyen que Google ou Adobe.
[^] # Re: OSEF
Posté par thoasm . En réponse au journal Ubuntu 14.04 LTS : Pourquoi il vaudrait mieux ne pas du tout s'en servir. Évalué à 4.
Euh, moi je vois surtout des gens qui s'estiment super mauvais en anglais, je vois pas en quoi le constat est nié.
[^] # Re: OSEF
Posté par thoasm . En réponse au journal Ubuntu 14.04 LTS : Pourquoi il vaudrait mieux ne pas du tout s'en servir. Évalué à 2.
Et on s'arrête au constat ? Si on s'arrête là on a aucune solution.
[^] # Re: On verra
Posté par thoasm . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 2.
Oui et non, l'approche de la méthode B c'est d'écrire des specs et de vérifier que l'implémentation respecte bien les specs, et au passage qu'il n'y a pas de bug à la con comme des buffer overflow. Après comme toujours les specs ont des limites, on peut pas vérifier la cohérence d'un protocole cryptographique si on code seulement un client et un serveur indépendament en B. Ni que la précondition P=NP qui serait l'hypothétique garantie de la sécurité du protocole en question, mais on c'est pas parce qu'on fait du B qu'on est obligé d'essayer :) ~~~~
[^] # Re: On verra
Posté par thoasm . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 3.
Pas du tout, si j'ai bien compris le principe de la faille, elle permet d'accéder à une zone mémoire qui ne devrait tout simplement pas être accessible. C'est pas une bête histoire de borne ?
[^] # Re: On verra
Posté par thoasm . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 2.
Je parle pas vraiment de faire de la preuve de protocole, en fait, on dialogue de sourd.
[^] # Re: On verra
Posté par thoasm . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 2.
Bien sur que si, déja si on peut garantir qu'il n'y a pas de bug d'implémentation type heartbleed c'est pas mal. Ça démontrera pas la totale correction du protocole c'est sur. À part ça, j'ai vu passer un récent ajout de modélisation système pour la méthode B sur l'article Wikipédia, je sais pas ce que ça recouvre et j'ai pas investigué, mais si ça se trouve ils s'intéressent à certaines problématiques de distribution.
[^] # Re: On verra
Posté par thoasm . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 1.
Pour revenir a des choses plus terre à terre, la faille qui a provoqué tout ça elle n'a pas un nombre arbitraire de pairs et il s'agissait juste d'une erreur de validation des IOs :) On peut prouver des choses rien qu'en bétonnant les IO, évidemment c'est plus compliqué de valider Internet dans sa globalité.
# Ça learne quoi ?
Posté par thoasm . En réponse au journal Le Web comme un learning machine. Évalué à -1.
TEDLT
[^] # Re: On verra
Posté par thoasm . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 4.
La spec, dans la méthode B, elle est haut niveau au début du developpement et elle se précise au fur et à mesure (c'est le raffinage) justqu'à devenir compilable. Les trous dans la spec tu les détectes parce que c'est impossible de montrer que ton raffinage est compatible avec ce que tu as écris avant. Ils mettent le processus de spec et de preuve au coeur du développement.
[^] # Re: On verra
Posté par thoasm . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 2.
C'est dur de prouver des systèmes distribués, certes, mais écrire du code correct et être sûr qu'il est correct c'est carrément ultra dur aussi. Il y a quand même des patterns connus pour prouver qu'un calcul distribué termine par exemple. On peut montrer aussi des propriétés d'autostabilisation ou des choses comme ça.
[^] # Re: On verra
Posté par thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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 thoasm . 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.