Quand votre navigateur affiche un petit cadenas à côté d’une URL, il vient de tenir une conversation cryptographique avec le serveur — le handshake TLS. Cette conversation est d’habitude gérée par d’énormes bibliothèques en C : OpenSSL, BoringSSL, des centaines de milliers de lignes que personne ne relit jamais entièrement.

Cet article est le capstone de l’arc crypto de la série. On y montre l’aboutissement : un vrai navigateur ouvre une page HTTPS servie par un binaire dont chaque transformation cryptographique — l’échange de clés, la signature d’identité, le chiffrement des données, le hash — est du code machine émis par verbose. Pas une ligne d’OpenSSL. Et le navigateur, le client TLS le plus exigeant qui soit, ne voit pas la différence : il fait le handshake et il affiche la page.

On s’appuie ici sur le SHA-256 (chapitre 1 de l’arc) — il revient partout dans TLS. Les détails de chaque brique (AES, Ed25519) viendront dans leurs propres chapitres ; ici, on prend de la hauteur et on regarde l’ensemble fonctionner.

Un handshake, en trois idées

Avant tout échange chiffré, le navigateur et le serveur doivent régler trois choses. C’est tout TLS, en une phrase chacune :

  1. Se mettre d’accord sur un secret que personne d’autre ne peut deviner, même en écoutant toute la conversation (l’échange de clés).
  2. Prouver son identité — le serveur montre un certificat et signe, pour qu’on sache qu’on parle au bon interlocuteur (la signature).
  3. Parler chiffré — une fois le secret partagé, tout le reste est chiffré avec un algorithme symétrique rapide (le chiffrement des données).

Sur le fil, ça ressemble à ça :

  NAVIGATEUR                              SERVEUR (binaire verbose)
      │                                          │
      │ ─── ClientHello ───────────────────────► │  « voici mes algos + ma clé »
      │ ◄── ServerHello ─────────────────────── │  « voici la mienne »
      │            (à partir d'ici, chiffré)      │
      │ ◄── Certificate + signature ──────────── │  « voici qui je suis, signé »
      │ ─── Finished ──────────────────────────► │
      │ ◄══ page HTML (chiffrée AES-GCM) ═══════ │  « Hello from Verbose TLS »
      │                                          │

Chacune des trois idées demande un ingrédient cryptographique. Et c’est là que verbose intervient.

Les ingrédients — et où passe la frontière

Voici la partie qui compte pour la thèse de verbose. Toute la cryptographie est du code machine verbose. L’hôte (en Python) ne fait que la plomberie : ouvrir la socket, découper les messages TLS, et tirer l’unique secret aléatoire (os.urandom).

  ┌──────────────────────────────────────────────────────────┐
  │  HÔTE (Python)  : socket, découpe des records TLS,         │
  │                   os.urandom (le seul secret en entrée)    │
  ├──────────────────────────────────────────────────────────┤
  │  VERBOSE (code machine x86-64) :                           │
  │     X25519          l'échange de clés                      │
  │     Ed25519 / P-256 la signature d'identité                │
  │     AES-128-GCM     le chiffrement des données             │
  │     SHA-256 + HKDF  le hash et la dérivation des clés       │
  └──────────────────────────────────────────────────────────┘

Chaque ligne du bloc verbose a été validée octet pour octet contre une référence avant d’être assemblée :

  • AES-128-GCM contre le vecteur NIST GCM Test Case 2 ;
  • X25519 contre la RFC 7748 ;
  • Ed25519 contre les trois vecteurs de la RFC 8032 §7.1 ;
  • HKDF contre la RFC 5869 ;
  • SHA-256, on l’a vu au chapitre 1, contre sha256sum.

Rien n’est cru sur parole parce que « ça a marché une fois ». Chaque brique est confrontée à la spec officielle, isolément, avant qu’on l’empile dans la suivante.

La seule boucle de tout TLS : le ladder X25519

Presque toute la cryptographie ici est déroulée : chaque opération se termine en un nombre fixe d’étapes que le vérificateur peut suivre statiquement. Il y a une seule vraie boucle — l’échange de clés X25519, qui fait grimper une « échelle » (le Montgomery ladder) sur 255 marches.

En verbose, une boucle s’écrit en récursion, et — comme à l’article #3 — elle doit prouver qu’elle se termine :

rule ladder
  logic:
    ...
    out = if s.i == 0 then <le résultat de l'échelle>
          else ladder(LadderState { ..., i: s.i - 1, ... })
  proofs:
    termination:
      decreasing : i

(L’état réel porte une cinquantaine de champs — les éléments de corps sur 10 limbes — élidés ici.) Le point essentiel : decreasing : i est une promesse vérifiée à la compilation. La marche i descend strictement à chaque appel, donc le compilateur prouve que l’échelle s’arrête. Les 255 itérations tournent à l’exécution ; la garantie qu’elles finissent, elle, est établie avant même que le binaire existe. Aucune construction de boucle générale n’a été ajoutée pour faire du TLS — les outils de preuve du chapitre 3 suffisent.

Le grain de sable : un vrai navigateur ne transige pas

Le premier serveur signait son identité avec Ed25519. Contre openssl s_client — le client de test habituel — tout passait : Verify return code: 0 (ok), signature ed25519. On aurait pu s’arrêter là et crier victoire.

Sauf qu’un vrai navigateur a refusé. Net : illegal_parameter.

Pourquoi ? Dans son ClientHello, le navigateur annonce les schémas de signature qu’il accepte (l’extension signature_algorithms). Et les navigateurs offrent ecdsa_secp256r1_sha256 (P-256), pas Ed25519. La RFC 8446 impose au serveur de signer avec un schéma offert. Ed25519 ne l’était pas → rejet immédiat.

C’est exactement la valeur d’un vrai navigateur comme cible : il impose des contraintes qu’un client de test laisse passer. Il a donc fallu construire toute la pile ECDSA P-256 — arithmétique du corps GF(p256), addition/doublement de points, multiplication scalaire, l’inverse modulaire, et la signature ECDSA-P256-SHA256 (nonce déterministe RFC 6979, encodage DER, low-s) — validée contre les vecteurs RFC 6979 §A.2.5 et openssl dgst -verify.

Avec un certificat P-256, le navigateur ne dit plus illegal_parameter. Il complète le handshake. Il affiche la page : « Hello from Verbose TLS ». Le seul avertissement restant, c’est celui — attendu — du certificat auto-signé. Pas une erreur de crypto. La page se rend.

Le détail qui plaît : plus petit, gratuitement

Deux réécritures en récursion, la même semaine, sans rien coûter en calcul :

  • p256_ninv : 11,2 Mo → 84 Ko de natif (131× plus petit), 8/8 octet pour octet vs la version déroulée.
  • x25519_finish : 1,3 Mo → 42 Ko (31× plus petit), 266 multiplications de corps identiques à la version déroulée. Handshake openssl re-validé après la cure.

Même algorithme, même sortie exacte, zéro surcoût CPU. Le chemin récursif introduit pour l’auto-hébergement (Phase A) s’est révélé être le bon outil pour replier d’immenses chaînes cryptographiques déroulées en code machine compact.

Pourquoi ça compte

TLS 1.3 n’est pas un jouet : c’est un empilement de primitives cryptographiques, dans une machine à états, dans un format de fil, avec un client public — votre navigateur — qui ne transige sur rien. Le faire tenir de bout en bout, c’est la preuve empirique que le langage et son compilateur peuvent exprimer, vérifier et exécuter un vrai protocole, pas une démo.

Et la méthode est le message. La cryptographie ici n’est pas crédible parce qu’un outil l’a produite — elle est crédible parce qu’elle est confrontée, brique par brique, aux vecteurs des RFC, puis à OpenSSL, puis à un navigateur qui ne pardonne rien. On ne fait pas confiance, on vérifie. C’est toute la différence, et c’est tout verbose : un binaire assez petit pour se lire, des preuves déclarées dans la source, et une sortie confrontée au réel à chaque étape.

L’arc a commencé avec un hash de 12 Ko au chapitre 1. Il finit avec un navigateur qui rend une page chiffrée par un binaire qu’on peut lire ligne à ligne. Entre les deux, il reste à raconter chaque brique en détail — AES, Ed25519, l’échelle de Montgomery. Ce sont les prochains chapitres.