Burps a écrit 30 commentaires

Un autre point de vue:

https://billatnapier.medium.com/a-major-advancement-on-quantum-cracking-48a484a28b51

F* est une suite de F7, qui est une surcouche à F#. L'étoile est en référence à celle des globs. Cependant, je ne me souviens plus du pourquoi de F7.

Si, car le code de la machine de Turing et de son entrée sont connus à la compilation - j'aurais du souligner les static const pour être plus clair, et aussi que l'évaluateur ne modifie pas l'état global. Je vais la faire en plus simple:

if (false)
  bla();

Maintenant le code mort est très clair ? Il est tellement clair que n'importe quel compilateur va l'enlever dans ce cas d'ailleurs. J'ai juste remplacer false par une constante plus dure à évaluer (c'est semi-décidable).

Pour moi, c'est indécidable car:

    void mon_evaluateur_de_machine_de_Turing_universelle
      (byte_t *code, byte_t *input)
    {
      /* ... */
    }

    void ma_super_fonction() {
      /* ... */
    }

    static const byte_t code [] = ...;
    static const byte_t input[] = ...;

    int main(void) {
      mon_evaluateur_de_machine_de_Turing_universelle(code, input);
      ma_super_fonction();
      return 0;
    }

Ici, ma_super_fonction est du code mort si la machine de Turing décrite par code sur l'entrée input termine. Bonne chance pour décider cela.

…mettre un espace avant un signe de ponctuation double ? Quadruple horreur !

Peut on prouver faux dans un système de typage ?

S'il n'est pas dédié à la preuve oui:

  let rec f () = f () in f () : 'a . 'a

qui prouve (forall P, P) (pour une certaine notion de quantification sur les prédicats). S'il est dédié à la preuve, il faut espérer que non. Sinon, tu obtiens une logique dont le seul modèle est à un point… pas très intéressant du point de vue logique.

Il me semblait que le "faux" se traduisait par une exception à l'exécution, ou un programme que ne termine pas. Dans le cas de racine de deux, c'est une fraction qu'on simplifie infiniment par exemple.

Il y a en effet des liens assez forts entre terminaison et consistance logique --- même s'il n'est pas forcément nécessaire d'avoir l'un pour avoir l'autre. À noter que dans mon exemple OCaml, j'ai utilisé la non-terminaison pour prouver (forall P, P).

Mais peut on créer un fonction de type dont le type de retour est "faux" ?

Une fonction qui retourne faux n'est pas problématique. C'est de pouvoir l'appliquer qui pose problème… car tu obtiens alors une preuve de faux. E.g., en Coq:

Definition f (p : False) := p.

est de type (False -> False), qui est une tautologie.

Au mon Dieu, une erreur au runtime !! Le typage de OCaml est faible du point de vue sureté (et j'inclus les GADT).

    ~ % ocaml
            OCaml version 4.02.1

    # [||].(0) ;;
    Exception: Invalid_argument "index out of bounds".
    # 

Un point sur lequel on n'insiste peut-être pas assez : ce problème n'est pas un bogue logiciel, pas un problème d'implémentation, mais bien un problème dans le protocole lui-même !

La partie MIM, quand même, personne n'obligeait les clients à se reconnecter en demandant SSL3.0, même si d'un point de vue client, être utilisable est prioritaire (TLS propose maintenant un mécanisme pour se protéger lorsqu'on désire avoir ce comportement, mais ce n'est pas un comportement impliqué par le protocole à mon avis).

Pour la partie Padding Oracle, c'est en effet intrinsèque. Mais là, pas de surprise non plus. On sait maintenant que Mac-then-Encrypt est problématique. Je suis même étonné que cette attaque ne sort que maintenant.

Je pense qu'il manque une information sur cette attaque. Le Padding Oracle est sur SSL3.0. le Downgraded Legacy vient du comportement des clients. Le scénario est le suivant:

• le client se connecte et demande une connexion en TLS1.0 - TLS1.2 par exemple
• le MIM renvoie un refus de ces versions (cette partie n'est pas encore authentifiée)
• le client se reconnecte (c'est une choix d'implémentation ici - mais qui est très répandue) et demande alors du SSL3.0

Pour éviter ce scénario, une cipher suite vide a été rajoutée: TLS Fallback Signaling Cipher Suite Value (SCSV). Cf

http://tools.ietf.org/html/draft-ietf-tls-downgrade-scsv-00

Proposer "One Time Pad" comme un moyen pratique de faire du chiffrement symétrique et éluder le problème d'échange de clé par une phrase sibylline du style "La seule petite question serait comment livrer les masques jetables à l'autre utilisateur, mais il y a des façons de le faire assez facilement" me paraît un peu rapide. Généralement, la rencontre physique est un peu compliquée quand on a besoin de telles garanties.

Sinon:
- Je n'ai pas compris comment il propose le déni plausible autrement que par "mais oui, monsieur, j'ai des fichiers totalement random et quand vous faites un xor, c'est du français, mais vraiment un truc de ouf, je m'en vais jouer ma grille de loto".
- Confidentialité persistante (Forward secrecy) ? On passera… c'est pourtant quelque chose qu'on voudrait.
- Ensuite, OTP est incassable… mathématiquement (comme dit dans l'article). Pourquoi leur implémentation ne fait apparaître aucun canal caché ? Rien n'est dit.
- Et le PRNG qui est un RNG ? Pourquoi ? Rien n'est dit. Ce n'est pas parce que il y a des cables que c'est un RNG. (Comme ce n'est pas parce que l'algorithme de PRGN a été généré aléatoirement que c'est un bon PRGN).

On a besoin d'implémentation sure (et prouvée) de protocoles cryptographiques. Et il faut expliquer pourquoi son implémentation est sure. Là, sur le site, je vois une bonne explication du problème (en effet, je ne fais pas confiance aux standards gouvernementaux), puis ensuite une rangée de trompettes sonnant triomphalement sous la bannière rutilante d'OTP, mais pas la queue d'une explication.

Non, c'est un choix de langage comme un autre… tant que le script commence avec #! /bin/bash.

Ils font quand même l'hypothèse assez forte qu'il y a un processus malveillant sur le même ordinateur, qui fonctionne en même temps que le programme de chiffrement.

Je ne trouve pas l'hypothèse si forte: tu peux retrouver la clé de chiffrement d'un disque dur pour une machine sur laquelle tu as un simple accès car dans ce cas tu peux forcer le programme de chiffrement à fonctionner en écrivant sur le disque dur. Ça a été fait en pratique, et c'est très efficace—bien sûr, ça ne marche plus aujourd'hui.

J'avais été voir une présentation de Shamir au collège de France. Il y avait présenté une attaque basée sur les variations de la tension sur les ports USB ou du bruit émis par la machine: le stepping du processeur, qui change suivant la charge demandée, provoque ces variations, au point que statistiquement tu arrives à différencier les multiplications des additions (et donc le bit de poids faible en cours d'inspection) lors du chiffrement RSA. A l'époque, c'était encore un peu fumeux, mais l'attaque s'améliore:

https://eprint.iacr.org/2013/857

Encore une question de performance, non ?

Par rapport à mon propos, oui et non. Oui, l'instruction Intel est là pour protéger AES contre ces attaques sans avoir une dégradation catastrophique des performances. Mais non, quitter l'assembleur ne va pas régler le problème des canaux cachés. J'aurais tendance à dire: au contraire même. Et l'analyse de ces implémentations va, avec l'état de l'art courant, être bien difficile aussi: il n'y a pas de modèle du JIT, il n'y a pas de modèle du GC. Ça ne veut pas dire que ça ne va pas arriver… et dans ce cas, avoir un langage de haut niveau permettra de mieux analyser le protocole en lui-même. Car TLS (même en 1.2) est très limite niveau crypto, et la RFC laisse certaine partie à interprétation.

Ce que tu montres est le support d'une extension Intel pour accéléer AES, ce qui n'est absolument pas indispensable pour faire de la crypto.

Et pour éviter de se faire casser son chiffrement de disque dur en 1s.

http://www.cs.tau.ac.il/~tromer/papers/cache.pdf

PS: je suis un grand utilisateur de langages de haut niveau. Mais il reste du travail à faire pour avoir des implémentations efficaces et sûres des primitives cryptographiques.

C'est une implémentation de référence, pas une implémentation destinée à être utilisée en production. C'est pour montrer l'utilité des méthodes formelles, et leur application à des protocoles conséquents. C'est transposable à d'autres langages (et comme je l'ai dit plus, ce n'est pas à toute épreuve, le GC introduisant des canaux cachés par exemple).

Aussi, l'implémentation de F# est sous Apache2 et testée sous Mono. C'est donc testable librement… même si encore une fois, je comprends qu'on ne puisse/veuille pas mettre un runtime mono où l'on veut !

C'est un mieux, mais ça ne doit pas donner un sentiment de sécurité à toute épreuve.

Une analyse en Coq ne va donner qu'une correction fonctionnelle ou, si tu as été jusqu'à formaliser un modèle crypto, ne va donner qu'une preuve de sécurité pour le modèle d'adversaire que tu captures.

De même, l'utilisation d'un GC va introduire des canaux cachés difficilement contrôlables.

Nonon. Je parlais bien de la disposition des barrettes. Par exemple, en mode réel, si elles sont en cercle de 256k de rayon, et que tu lis 64k vers le centre, tu tombes sur du vide.

Avec un MMU entre les deux…

Pour les flemmards comme moi qui ne sont pas allés voir le patch:

http://blog.existentialize.com/diagnosis-of-the-openssl-heartbleed-bug.html

Ça semble (un peu) moins critique que le laisse entendre la description initiale: on ne peut pas lire 64k où l'on veut. Donc récupérer le certificat doit fortement dépendre de la disposition de la mémoire…

Oui, mais certainement pas inférieur, on est d'accord (la norme est assez claire la dessus en effet).

Ceci étant, sans aller vérifier, je suppose qu'il y a un lien historique entre les noms float et double de C et les flottants simple et doucle précision de la norme IEEE, mais que la norme est moins stricte pour les archis sans ces derniers.

Et il te semble bien… Sans aller sortir la norme IEEE, on peut déjà faire:

(gdb) p sizeof (double)
$1 = 8
(gdb) p sizeof (float)
$2 = 4

Le principe de beaucoup de fruits, quand même, c'est d'attirer l'animal pour qu'il le mange et qu'il dissémine les graines. On peut donc penser que l'évolution aura fait que manger le fruit ne soit pas un traumatisme (au sens médical) pour l'arbre e.g.

Ce qui est marrant, c'est que les logiciens la font avec "un physicien, un mathématicien et un logicien…"

Je me demande quel est l'imbécile du biologiste :)

C'est pire que ça:

Lisibilité: 95 %
Used builtin function 'map'(-5%)

(i.e. map(int, values) contre [int(x) for x in values] je suppose).

Tant qu'on y est: "je l'admets".

Sinon, on peut les danser aussi !