Il y a une phrase, dans le document de conception de la couche TLS de verbose, section 4 :

No cryptography in the host.

Aucune cryptographie côté hôte. Toute la crypto — AES, GHASH, la dérivation de clés, SHA-256 — était censée tourner dans des binaires émis par verbose, avec leurs preuves. Le script Python qui les orchestre ne devait faire que de la plomberie : lancer, transporter des octets, ranger.

Trois sections plus loin, dans le même document, un audit numéroté MAJOR-1 dit que c’est faux. Six calculs étaient encore en Python : le nonce, l’en-tête authentifié, le bloc de compteur initial, le bloc de longueurs, le tag, et la comparaison du tag. Pas de la plomberie. De la cryptographie — petite, mais de la vraie, celle qui, ratée, fait accepter un message forgé.

La section 4 n’a pas été discrètement réécrite. La section 7 a été ajoutée, avec le mot faux dedans. Puis les six calculs ont déménagé. C’est la PR #199, et c’est tout ce que raconte cet article.

Ce que c’est, l’« encadrement »

On ne va pas réexpliquer AES-GCM. On va regarder ce qui entoure le chiffrement, parce que c’est là que vivaient les six calculs.

L’analogie : une lettre recommandée. Le message est dans l’enveloppe, chiffré — ça, verbose le faisait déjà. Mais autour, il y a :

  ┌─────────────────────────────────────────────────────────────┐
  │  numéro de suivi     ← ne doit JAMAIS se répéter            │
  │  ─────────────────                                          │
  │  en-tête visible     ← le facteur le lit, mais s'il est     │
  │  (type, version,       modifié, le sceau ne tient plus       │
  │   longueur)                                                  │
  │  ─────────────────                                          │
  │  [ contenu chiffré ]                                        │
  │  ─────────────────                                          │
  │  sceau de cire       ← 16 octets qui prouvent que rien,     │
  │                        ni l'en-tête ni le contenu,          │
  │                        n'a bougé                            │
  └─────────────────────────────────────────────────────────────┘

Et à la réception : vérifier le sceau sans dire au faussaire à quel endroit son faux a échoué. On y reviendra, c’est le cœur de l’article.

Les six calculs, mis en face de l’enveloppe :

  règle          ce qu'elle produit                            taille
  ───────────────────────────────────────────────────────────────────
  gcm_nonce      le numéro de suivi : IV ⊕ numéro de séquence   12 o
  gcm_j0         le bloc de départ du compteur : nonce ‖ 0³¹ ‖ 1 16 o
  gcm_aad        l'en-tête visible : 23 ‖ 0303 ‖ longueur        5 o
  gcm_lenblock   les longueurs en bits, pour le sceau            16 o
  gcm_tag        le sceau : S ⊕ E_K(J0)                          16 o
  gcm_tag_eq     « le sceau reçu est-il le bon ? »               0 / 1

Chacune cite sa référence — RFC 8446 pour TLS, SP 800-38D pour GCM — dans son @intention. Chacune est une règle verbose ordinaire, avec ses preuves de pureté et de terminaison.

Pourquoi maintenant, et pourquoi sans toucher au compilateur

Regardez la colonne de droite. 12, 16, 5, 16, 16, 1. Tout est à largeur fixe.

C’est ça, la clé. Il y a quelques semaines, l’arc des agrégats a appris aux règles verbose à renvoyer un record — une structure de plusieurs champs — à une autre règle, sans copie. Une règle qui renvoie 16 octets sous forme de record, c’est exactement ce dont un encadrement TLS a besoin, et exactement ce qui n’existait pas quand la section 4 a été écrite.

Alors les six calculs sont devenus six règles. La PR touche src/native.rs sur 178 lignes — toutes des tests. Zéro changement au compilateur. Le langage avait déjà tout ce qu’il fallait ; il fallait juste cesser de faire le travail ailleurs.

Ce qui reste côté hôte est nommé, et c’est précisément ce que la section 4 autorisait depuis le début : la boucle CTR bloc par bloc sur un contenu de longueur variable, le remplissage d’une queue de longueur variable, et le transport des records entre binaires. À largeur variable, hors périmètre. À largeur fixe, dans verbose. La frontière est enfin là où la doc disait qu’elle était.

La règle qui mérite qu’on s’arrête

Cinq des six règles assemblent des octets. La sixième les compare, et c’est là qu’une erreur ne se voit pas.

Voici le problème. Vous recevez un enregistrement TLS avec son tag de 16 octets. Vous recalculez le tag de votre côté. Il faut dire égal ou pas égal. La façon évidente :

  pour chaque octet i de 0 à 15 :
      si tag_reçu[i] ≠ tag_calculé[i] :
          répondre « faux »        ← on s'arrête au premier écart
  répondre « vrai »

C’est correct. C’est ce qu’on écrirait sans réfléchir. Et c’est une faille.

L’analogie : un videur qui vérifie un mot de passe lettre par lettre, et qui vous refoule dès la première lettre fausse. Vous n’avez pas le mot de passe. Mais vous avez un chronomètre. Vous essayez A…, B…, C… — le refus est immédiat. Puis S… — le refus arrive un poil plus tard. Il a vérifié une lettre de plus : la première est un S. Recommencez pour la deuxième. Seize lettres, quelques centaines d’essais, et vous êtes entré sans jamais avoir deviné le mot de passe : vous l’avez mesuré.

C’est une attaque par canal temporel, et pour un tag d’authentification c’est fatal : un attaquant qui peut forger un tag peut faire accepter n’importe quel message. La règle est donc absolue : le temps de la comparaison ne doit dépendre d’aucun octet des deux tags. Pas de if. Pas de sortie anticipée. Le même nombre d’opérations, toujours.

Voici gcm_tag_eq, telle qu’elle est dans le dépôt :

rule gcm_tag_eq
  @intention: "constant-time equality of two 16-byte tags: 1 when every
               byte matches, 0 otherwise, with no data-dependent branch
               in the accumulation"
  input:
    p : TagPair            -- a0..a15 : le tag calculé, r0..r15 : le tag reçu
  output:
    eq : number
  logic:
    let d0  = bxor(p.a0, p.r0)
    let d1  = bor(d0,  bxor(p.a1,  p.r1))
    let d2  = bor(d1,  bxor(p.a2,  p.r2))
    ...
    let d15 = bor(d14, bxor(p.a15, p.r15))
    eq = 1 - min(d15, 1)
  proofs:
    purity:
      reads : [p.a0, …, p.a15, p.r0, …, p.r15]
      calls : []
    termination:
      bound : 2

Déroulons-la. bxor — le OU exclusif — vaut 0 si et seulement si les deux octets sont identiques. bor — le OU — accumule : dès qu’une différence est apparue, elle ne disparaît plus.

  Cas 1 — les deux tags sont identiques :

    bxor(a0,r0)=0   bxor(a1,r1)=0   …   bxor(a15,r15)=0
    d0 = 0
    d1 = 0 | 0 = 0
    …
    d15 = 0
    eq  = 1 - min(0, 1) = 1 - 0 = 1          → égal

  Cas 2 — un seul octet diffère, le troisième :

    bxor(a0,r0)=0   bxor(a1,r1)=0   bxor(a2,r2)=0   bxor(a3,r3)=0x5A   …
    d0 = 0
    d1 = 0
    d2 = 0
    d3 = 0 | 0x5A = 0x5A         ← la différence entre
    d4 = 0x5A | 0 = 0x5A            elle reste, quoi qu'il arrive après
    …
    d15 = 0x5A
    eq  = 1 - min(0x5A, 1) = 1 - 1 = 0        → pas égal

Regardez ce que font les deux cas : seize XOR, quinze OR, un min, une soustraction. Trente-trois opérations dans les deux cas. Que la différence soit au troisième octet, au seizième, ou nulle part, le chemin est le même. Le chronomètre ne mesure plus rien.

Le min(d15, 1) mérite un mot : d15 vaut 0 ou n’importe quoi de non nul — 0x5A, 0xFF, 3. On veut un booléen propre. min(x, 1) ramène tout non-nul à 1 sans brancher. Puis 1 - … inverse. Deux opérations arithmétiques là où on aurait envie d’écrire if d15 == 0.

Et le bloc proofs: dit au compilateur : cette règle lit exactement ces 32 champs, n’appelle rien, termine en deux pas. Ce n’est pas un commentaire ; si la logique lisait un champ non déclaré, ça ne compilerait pas. La promesse habituelle — l’auteur déclare, le binaire ne dérive pas — s’applique ici à une règle dont la forme est une propriété de sécurité.

L’oracle qui ne ment pas

Comment sait-on que ces six règles sont justes ? Pas en les relisant — on a vu cet été ce que vaut la relecture pour ce genre de bug.

Trois niveaux, du plus local au plus impitoyable :

  1. Chaque règle contre une référence indépendante. gcm_nonce est comparée octet pour octet à une implémentation RFC 8446 tierce. gcm_tag_eq est passée sur : deux tags égaux → 1 ; un bit inversé à chacune des seize positions → 0 à chaque fois ; deux tags entièrement différents → 0.
  2. Le harnais de crypto — VCRYPTO_OK, avec une nouvelle étape framing à 2 ms, et un aller-retour AEAD complet.
  3. Une vraie poignée de main TLS 1.3, contre un vrai openssl s_client 3.6.2, en PSK-DHE : Protocol: TLSv1.3, Verify return code: 0, et un hello world livré à travers le tunnel.

Le troisième niveau est celui qui compte. Un nonce décalé d’un bit, un bloc de longueurs en octets au lieu de bits, un tag calculé sur le mauvais en-tête — et openssl refuse la session. Il ne connaît pas verbose, il ne lit pas la doc, il ne fait pas confiance. C’est exactement ce qu’on veut d’un oracle.

Et l’obsession habituelle : les 128 binaires du corpus, recompilés avant et après, identiques à l’octet. Six règles ajoutées, rien d’autre n’a bougé.

Ce que ça apprend

Une doc qui dit « aucune cryptographie côté hôte » alors qu’il y en a six morceaux, ce n’est pas un mensonge — c’est une intention écrite avant que le langage ne sache la tenir. Ce qui compte, c’est ce qu’on en fait le jour où l’écart est mesuré. Ici : on l’a écrit noir sur blanc dans le même document, puis on a rendu la phrase vraie. La section 4 est aujourd’hui restated honestly — c’est le mot de la PR.

Et la limite, nommée comme les fois précédentes : v0.11.0 n’est pas taguée, ~25 commits après la v0.10.0, avec en plus huit PRs en brouillon empilées cette semaine sur un arc HTTP borné. Le rythme a changé de forme — moins de merges, plus de chantiers parallèles. On verra ce que ça donne.

Seize XOR, pas un seul if. Le sceau se vérifie en trente-trois opérations, toujours les mêmes, et la seule chose qu’un chronomètre y apprendra, c’est qu’il n’y a rien à apprendre.