Was eine VPN-Protokollspezifikation beweist und was nicht

Ein Protokolldokument ist ein Vertrag zwischen Implementierungen, und genaues Lesen sagt Ihnen, was zwei konforme Gegenstellen austauschen und welche Eigenschaften die Designer sichern wollten. Es sagt Ihnen nicht, welches Binärprogramm auf dem Server läuft, mit dem Sie sich verbinden, wie dieser Server konfiguriert wurde oder was danach mit Ihrem Kontodatensatz geschieht. Das sind drei verschiedene Arten von Belegen, und die Spezifikation als alle drei zu behandeln, ist der Weg, auf dem ein Protokollname beginnt, Arbeit zu leisten, die er nicht leisten kann. Die drei auseinanderzuhalten ist die ganze Übung.

Das Dokument ist der Anfang eines Arguments, nicht sein Schluss.

Was das Dokument tatsächlich festlegt

Für WireGuard definiert die Protokollbeschreibung einen Noise-IK-Handshake, eine feste Menge von Primitiven, Nachrichtenlayouts und das Transport-Framing, das anschließend Pakete trägt. Für IKEv2 ist das vergleichbare Artefakt RFC 7296, der Austausche, Nutzlasten und die Aushandlung von Vorschlägen spezifiziert. In beiden Fällen ist der Umfang präzise: die Nachrichten, die Zustandsmaschine und die Annahmen, unter denen die Sicherheitsziele gelten.

Optionale Modi erschweren die Lektüre. Eine Eigenschaft, die für einen Handshake gilt, gilt möglicherweise nicht für einen Einsatz mit anderer Authentifizierungsregelung oder einer Ausweichkonfiguration.

Wo die Garantien enden

Eine formale Analyse beantwortet eine Frage über ein Modell. Die Verifikationsarbeit zu WireGuard nutzt ein symbolisches Modell im Tamarin-Beweiser, das zeigen kann, dass das Design bestimmten Angriffen unter seinen Annahmen widersteht; es zeigt nicht, dass eine ausgelieferte Implementierung im Userspace keinen Speichersicherheitsfehler hat. Genau in dieser Lücke zwischen Modell und Maschine leben reale Vorfälle. Einen Beweis als Implementierungszertifikat zu lesen, ist ein Kategorienfehler.

Forward Secrecy veranschaulicht dieselbe Grenze. Die Eigenschaft hängt davon ab, dass Schlüssel wie vom Protokoll vorgesehen vernichtet werden, und das ist eine Eigenschaft der Implementierung und ihrer Umgebung, nicht des Nachrichtenformats. Ein Design, das Löschung vorschreibt, kann sie auf einer Plattform nicht erzwingen, die Speicher auf die Platte auslagert.

Geschichtete Abhängigkeiten erweitern die Lücke weiter: die TLS-Bibliothek hinter einem TLS-basierten Tunnel, die Kernel-Schnittstelle, die ein Userspace-Tunnel nutzt, und der Zufallszahlengenerator stehen alle außerhalb des Protokolltexts.

Verfolgen Sie die Bytes bis in den Build

Gehen Sie vom Dokument zu den Artefakten, indem Sie Versionen identifizieren und sie dann mit dem vergleichen, was tatsächlich Verkehr bedient. Ein Produkt, das ein Protokoll nennt, kann Bereitstellungs-, Telemetrie- und Verwaltungskomponenten hinzufügen, die die Spezifikation nie beschreibt.

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

Reproduzierbare Builds und veröffentlichte Prüfsummen ermöglichen es, einen Quellbaum mit einem verteilten Binärprogramm zu verbinden. Ohne diese Verbindung belegt veröffentlichter Quellcode nur, dass eine Prüfung möglich ist, nicht dass die laufende Datei ihm entspricht.

Konfiguration gehört zum selben Schritt. Cipher-Suiten, erlaubte Gegenstellen und Routing-Einstellungen sind Einsatzentscheidungen, und ein konformer Build, der nachlässig konfiguriert wurde, erzeugt immer noch einen schwachen Tunnel.

Halten Sie Betriebspraktiken getrennt

Kontodatensätze, Zahlungsdaten und Support-Eingaben sind Betreiberentscheidungen, die kein Protokolltext einschränkt. Ein Prüfbericht deckt benannte Komponenten in einem erklärten Umfang ab, und eine Datenschutzerklärung beschreibt Absichten und Praktiken; keines ersetzt das andere, und keines ist eine kryptografische Aussage.

Die genaue Schlussfolgerung ist kumulativ: Die Spezifikation erklärt das Design, Build und Konfiguration erklären den Tunnel, und die dokumentierten Praktiken des Betreibers erklären alles, was der Tunnel nie sieht. Sagen Sie, was davon Sie überprüft haben, und die Behauptung bleibt wahr.