Le fil des geeks informatiques

[Theor]

Aujourd'hui, j'ai découverts l'existence d'un langage fonctionnel encore plus formel que Haskell : Coq. Tellement formel qu'il n'en est pas complet Turing, mais qu'il a été à l'origine de la découverte du bug d'OpenSSL/TLS !

 

http://linuxfr.org/news/sortie-de-coq-8-5-beta-un-assistant-de-preuve-formelle

[Cthulhu]

J'avais un colloc matheux qui utilisait ça plus ou moins régulièrement.

 

Parait que l'intro de son inventeur (français bien entendu) dans les confs donnait à peu près "I'm going to pull down my trousers and show you my Coq"

[Noob]

C'est pas un de ces machins développé par Dassault système ? Je sais qu'une de ces compagnies avait un langage formel permettant de prouver une partie de leur système d'armement.

[Rincevent]

Aujourd'hui, j'ai découverts l'existence d'un langage fonctionnel encore plus formel que Haskell : Coq. Tellement formel qu'il n'en est pas complet Turing, mais qu'il a été à l'origine de la découverte du bug d'OpenSSL/TLS !

 

http://linuxfr.org/news/sortie-de-coq-8-5-beta-un-assistant-de-preuve-formelle

Je connaissais Coq, mais j'ignorais qu'il avait permis la découverte de ce bug. Comme quoi, les gens vont finir un jour par s'intéresser à autre chose qu'aux accolades !

[Rübezahl]

C'est pas un de ces machins développé par Dassault système ? Je sais qu'une de ces compagnies avait un langage formel permettant de prouver une partie de leur système d'armement.

 

https://fr.wikipedia.org/wiki/Ada_%28langage%29(?)

 

[Theor]

https://fr.wikipedia.org/wiki/Ada_%28langage%29(?)

 

 

Non, j'aurais plutôt dit SPARK, mais SPARK n'est pas vraiment formel, et ne possède pas non plus les paradigmes fonctionnels du LISP, Haskell, CaML ou Coq (pas de lambdas, pas de confusion syntaxe - AST ni de confusion code-données). Ca n'en reste pas moins un langage beaucoup plus prouvable que les langages procéduraux classiques, de ce que l'on en dit.

[Poil à gratter]

On m'a dit que Bombardier au Canada utilise aussi un langage formel pour ses systèmes embarqués, mais je ne me rappelle plus du nom. C'est effectivement intéressant, mais le problème ce sont les couts de développement qui explosent. Évidemment quand le système qu'on écrit va tuer des gens si il plante, les couts de développement sont un peu secondaires.

 

Mais maintenant qu'il y a de l'informatique embarquée un peu partout et qui contrôle des systèmes qui peuvent potentiellement tuer des gens si ils plantent, ça serait peut-être bien de s’intéresser un peu plus à ce genre de langages pour tester des trucs comme GLIBC ou SSH.

 

Par exemple j'ai lu que fin d'année dernière, une fonderie en Allemagne a été endommagée par un hacker: ils ont réussi à pénétrer le système et prendre contrôle du creuset et l'ont détruit. J'imagine très bien le même genre de hack sur tout un tas de systèmes plus ou moins connectés au réseau, et ça fait flipper.

[Sekonda]

C'est pas un de ces machins développé par Dassault système ? Je sais qu'une de ces compagnies avait un langage formel permettant de prouver une partie de leur système d'armement.

Scade d'Esterel ?

[Noob]

Scade d'Esterel ?

 

Peut-être bien, je me souviens plus du nom.

[Malky]

Non, j'aurais plutôt dit SPARK, mais SPARK n'est pas vraiment formel, et ne possède pas non plus les paradigmes fonctionnels du LISP, Haskell, CaML ou Coq (pas de lambdas, pas de confusion syntaxe - AST ni de confusion code-données). Ca n'en reste pas moins un langage beaucoup plus prouvable que les langages procéduraux classiques, de ce que l'on en dit.

 

En même temps c'est pas vraiment fait pour ça. SPARK c'est du Ada hardcore - c'est fait pour développer de l'embarqué 'critique'. Pas pour prouver le théorème de Riemann.

[WBell]

Le problème de Coq, chez les Anglo-saxons, c'est le nom. C'est impossible pour un architecte ou un ingénieur d'aller voir le premier n+1 non technique pour lui dire (même dans un powerpoint) : "alors on va prouver le code, avec un outil qui s'appelle B*te"...

[neuneu2k]

C'est parce que les anglo-saxons n'ont aucun humour, quand on à des problèmes de slow consumer ou de surproduction sur un système et qu'on décide de repartir sur une base saine en rejouant les évenements, je me fait un plaisir de hurler au téléphone "Mais putain, purge la queue !" voir "Arrete la branlette et purge moi cette putain de queue !"

 

 

[Mathieu_D]

Mais putain, purge la queue !" voir "Arrete la branlette et purge moi cette putain de queue !"

Je me bats quasi tous les jours pour que les nanas de l'openspace ne disent pas "queue" mais "file" ou en prononçant en anglais "qyou".

Parce que bon "je ne peux pas lancer le reporting, il y a une trop grosse queue", dit naïvement sans se rendre compte de rien, c'est perturbant.

[neuneu2k]

Je me bats quasi tous les jours pour que les nanas de l'openspace ne disent pas "queue" mais "file" ou en prononçant en anglais "qyou".

Parce que bon "je ne peux pas lancer le reporting, il y a une trop grosse queue", dit naïvement sans se rendre compte de rien, c'est perturbant.

 

Pff, casseur de joie.

[Mathieu_D]

Une fois il y en a une qui a compris le double sens de ce qu'elle a dit et est devenue toute rouge.

[neuneu2k]

Attends, je relis ta phrase lentement "LES nanas de l'open space", et elles n'ont pas toutes l'esprit mal tourné ???

 

Tu travaille ou, détaché dans un back office conf/reglement ou compta ?

 

 

[Mathieu_D]

Presque, contrôle de gestion côté métier.

[neuneu2k]

Oui, du coup c'est une ambiance un peu plus feutrée et féminine, j'entends bien la différence par rapport à une fosse d'exploitation, un open space de dev ou une salle de marché

[Theor]

Le problème de Coq, chez les Anglo-saxons, c'est le nom. C'est impossible pour un architecte ou un ingénieur d'aller voir le premier n+1 non technique pour lui dire (même dans un powerpoint) : "alors on va prouver le code, avec un outil qui s'appelle B*te"...

 

Ca ne les dérange pourtant pas de commit/pull/clone avec git, modifier une image avec Gimp, ou mettre en place un IDS/IPS avec snort.

[Mathieu_D]

Oui, du coup c'est une ambiance un peu plus feutrée et féminine, j'entends bien la différence par rapport à une fosse d'exploitation, un open space de dev ou une salle de marché

Ben faut reconnaître que le rabat-joie dans l'histoire, c'est moi.

C'est vrai aussi que je ne réagirais pas pareil dans l'open space des dev'.

(Auquel cas je ne me ferais pas chier à venir en costard.)

[Theor]

Un bel exemple d'extreme programming, ici sur SNES. L'idée est de positionner du code dans un registre CPU et de trouver une faille pour l'exécuter. Tout à la manette et sans émulateur bien entendu.

 

D'abord pour accéder à l'écran de fin et finir le jeu en 2mn: http://hackaday.com/2015/01/22/reprogramming-super-mario-world-from-inside-the-game/

 

Et tant qu'à faire, pourquoi ne pas utiliser un émulateur pour scripter les commandes et reprogrammer le jeu à la volée en codant des niveaux qui n'ont rien à voir...

http://arstechnica.com/gaming/2014/01/how-an-emulator-fueled-robot-reprogrammed-super-mario-world-on-the-fly/

 

La préparation de l'exploit dure jusqu'à 1:40, puis c'est alors l'injection du code arbitraire via le script émulateur.

 

Le niveau des gars me fait juste fait halluciner.

[h16]

Un bel exemple d'extreme programming, ici sur SNES. L'idée est de positionner du code dans un registre CPU et de trouver une faille pour l'exécuter.

Ah non, pas dans un registre.

[Cthulhu]

C'était pas dans une texture ou un sprite ? De ce que je m'en rappelle.

[h16]

Non. Lisez l'article, c'est expliqué.

[jubal]

Il exécute du code donc c'est en mémoire, en l'occurrence la ou les coordonnées des sprites sont stockées.

En tout cas c'est vraiment énorme il peut exécuter ce qu'il veut, il jailbreak la SNES j'aime beaucoup

[Theor]

Les gars se sont encore améliorés en l'espace d'un an. Au programme, lancer un bot IRC avec en tout et pour tout... une cartouche de Pokemon Rouge sur Game Boy. Ca en est presque drôle.

Autre curiosité, le code de Super Mario Bros (NES) porté en 16 bits et envoyé à chaud dans la RAM depuis Super Mario World (SNES).

 

http://arstechnica.com/gaming/2015/01/pokemon-plays-twitch-how-a-robot-got-irc-running-on-an-unmodified-snes/

 

Sinon, dans quelques minutes (18h) commence le concours pour The Great Escape, jeu de programmation multijoueurs en ligne.

Si certains veulent s'inscrire ou essayer un tutorial, c'est par là : http://www.codingame.com/challenge/the-great-escape

[Sloonz]

Petit problème pour les cryptogeeks.

Norbert possède un gros message chiffré avec la clé A de Alice. Alice ne possède plus le message chiffré, ni le message déchiffré, mais possède toujours la clé.

Elle veut autoriser Bob à lire le message en clair, sans que :

- Bob connaisse la clé A

- Norbert connaisse la clé A

- Norbert connaisse le message en clair

- Le message ait à transiter entre Alice et Bob ou entre Alice et Norbert (trop gros pour Alice qui a une faible bande passante)

Par contre, elle peut demander à Norbert de transformer le message chiffré d’une certaine façon, et transmettre un secret autre que A à Bob.

Y aurait-il un chiffrement/protocole cryptographique qui permettrait ça ?

(note: Alice ne connait rien de Bob au moment où elle a chiffré le message avec sa clé A)

[Jesrad]

Non.

[Sloonz]

Je viens de tilter que ça marchait bien avec un XOR en fait

Norbert a M xor A. Alice lui transmet B et lui dit de calculer (M xor A) xor B, de transmettre le résultat à Bob, et transmet elle-même A xor B à Bob.

(bon le problème c’est que A étant réutilisé je peux pas me contenter d’un XOR )

[Noob]

Oui, si tu réutilises A alors tu donnes A pour autant que les deux collaborent.

 

Et plus si c'est un problème de bande passante, alors ça ne marche pas car B aura la même taille que A, donc A xor B aussi.

Avec le one time pad, il faut que la clé soit aussi longue que le message, donc il faut trouver une autre excuse pour illustrer la contrainte de ce problème   .

 

Mais de toute façon si Norbert conserve A xor M et que Bob a M alors ils ont A à tous les coups.