Ce qu’une spécification de protocole VPN prouve et ce qu’elle ne prouve pas

Un document de protocole est un contrat entre implémentations, et le lire attentivement vous dit ce que deux pairs conformes échangeront et quelles propriétés les concepteurs entendaient garantir. Il ne vous dit pas quel binaire s’exécute sur le serveur auquel vous vous connectez, comment ce serveur a été configuré ni ce qu’il advient ensuite de l’enregistrement de votre compte. Ce sont trois types de preuves différents, et traiter la spécification comme s’il s’agissait des trois est la manière dont un nom de protocole commence à faire un travail qu’il ne peut pas faire. Garder les trois séparés est tout l’exercice.

Le document est le début d’un argument, pas sa conclusion.

Ce que le document spécifie réellement

Pour WireGuard, la description du protocole définit une poignée de main Noise IK, un ensemble fixe de primitives, des formats de message et le cadrage de transport qui achemine ensuite les paquets. Pour IKEv2, l’artefact comparable est la RFC 7296, qui spécifie les échanges, les charges utiles et la négociation des propositions. Dans les deux cas, la portée est précise : les messages, la machine à états et les hypothèses sous lesquelles les objectifs de sécurité tiennent.

Les modes optionnels compliquent la lecture. Une propriété qui vaut pour une poignée de main peut ne pas s’appliquer à un déploiement utilisant une autre disposition d’authentification ou une configuration de repli.

Où les garanties s’arrêtent

Une analyse formelle répond à une question sur un modèle. Le travail de vérification de WireGuard utilise un modèle symbolique dans le prouveur Tamarin, qui peut montrer que la conception résiste à certaines attaques compte tenu de ses hypothèses ; il ne montre pas qu’une implémentation livrée en espace utilisateur n’a aucun défaut de sûreté mémoire. C’est dans cet écart entre le modèle et la machine que vivent les incidents réels. Lire une preuve comme un certificat d’implémentation est une erreur de catégorie.

La confidentialité persistante illustre la même frontière. La propriété dépend de la destruction des clés comme le protocole l’entend, et c’est une propriété de l’implémentation et de son environnement, non du format du message. Une conception qui prescrit l’effacement ne peut pas l’imposer sur une plateforme qui pagine la mémoire vers le disque.

Les dépendances en couches élargissent encore l’écart : la bibliothèque TLS derrière un tunnel fondé sur TLS, l’interface du noyau qu’utilise un tunnel en espace utilisateur et le générateur de nombres aléatoires se situent tous hors du texte du protocole.

Suivez les octets jusqu’à la compilation

Passez du document aux artefacts en identifiant les versions, puis en les comparant à ce qui sert réellement le trafic. Un produit qui nomme un protocole peut ajouter des composants de provisionnement, de télémétrie et de gestion que la spécification ne décrit jamais.

openvpn --version | head -3
wg --version
dpkg -l | grep -E 'openvpn|wireguard|libssl'
ss -lunp | grep -E '1194|51820'
sha256sum ./wireguard-tools_1.0.20210914_amd64.deb

Les compilations reproductibles et les sommes de contrôle publiées permettent de relier une arborescence source à un binaire distribué. Sans ce lien, la source publiée prouve seulement que l’inspection est possible, pas que le fichier en cours d’exécution y correspond.

La configuration relève de la même étape. Les suites de chiffrement, les pairs autorisés et les paramètres de routage sont des choix de déploiement, et une compilation conforme configurée avec négligence produit encore un tunnel faible.

Tenez les pratiques d’exploitation à part

Les enregistrements de compte, les données de paiement et les demandes d’assistance sont des décisions de l’opérateur que nul texte de protocole ne contraint. Un rapport d’audit couvre des composants nommés dans un périmètre déclaré, et une politique de confidentialité décrit des intentions et des pratiques ; ni l’un ni l’autre ne remplace l’autre, et ni l’un ni l’autre n’est un énoncé cryptographique.

La conclusion précise est cumulative : la spécification explique la conception, la compilation et la configuration expliquent le tunnel, et les pratiques documentées de l’opérateur expliquent tout ce que le tunnel ne voit jamais. Dites ce que vous avez vérifié parmi ces éléments, et l’affirmation reste vraie.