Какво доказва спецификацията на VPN протокол и какво не

Протоколният документ е договор между реализации и внимателното му четене ви казва какво ще разменят два съответстващи си партньора и какви свойства са предвидили дизайнерите. Той не ви казва кой двоичен файл работи на сървъра, към който се свързвате, как е конфигуриран този сървър или какво се случва с акаунтния ви запис след това. Това са три различни вида доказателство и третирането на спецификацията като всичките три е начинът, по който едно име на протокол започва да върши работа, която не може. Разделянето на трите е цялото упражнение.

Документът е началото на един аргумент, не неговото заключение.

Какво всъщност определя документът

За WireGuard описанието на протокола дефинира ръкостискане Noise IK, фиксиран набор от примитиви, оформления на съобщенията и транспортното рамкиране, което след това носи пакетите. За IKEv2 сравнимият документ е RFC 7296, който специфицира размените, полезните натоварвания и договарянето на предложения. И в двата случая обхватът е точен: съобщенията, машината на състоянията и допусканията, при които целите за сигурност са в сила.

Незадължителните режими усложняват четенето. Свойство, което е в сила за едно ръкостискане, може да не се отнася за внедряване с различна схема за удостоверяване или резервна конфигурация.

Къде спират гаранциите

Формалният анализ отговаря на въпрос за модел. Работата по верификация на WireGuard използва символен модел в доказателя Tamarin, който може да покаже, че дизайнът устоява на определени атаки при дадените допускания; той не показва, че доставена реализация в потребителското пространство няма дефект в безопасността на паметта. Именно в тази разлика между модел и машина живеят реалните инциденти. Четенето на доказателство като сертификат за реализация е категорийна грешка.

Пряката поверителност илюстрира същата граница. Свойството зависи от унищожаването на ключовете, както протоколът предвижда, а това е свойство на реализацията и нейната среда, а не на формата на съобщението. Дизайн, който предписва изтриване, не може да го наложи на платформа, която изнася паметта на диск.

Слоестите зависимости разширяват пропастта още повече: TLS библиотеката зад тунел, базиран на TLS, интерфейсът на ядрото, който използва тунел в потребителското пространство, и генераторът на случайни числа стоят извън текста на протокола.

Проследете байтовете до самата компилация

Преминете от документ към артефакти, като идентифицирате версиите и след това ги сравните с това, което действително обслужва трафика. Продукт, който назовава протокол, може да добави компоненти за предоставяне, телеметрия и управление, които спецификацията никога не описва.

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

Възпроизводимите компилации и публикуваните контролни суми правят възможно свързването на дърво на изходния код с разпространяван двоичен файл. Без тази връзка публикуваният изходен код доказва само, че инспекцията е възможна, а не че работещият файл съответства на него.

Конфигурацията принадлежи към същата стъпка. Наборите от шифри, разрешените партньори и настройките за маршрутизиране са избори за внедряване и съответстваща компилация, конфигурирана небрежно, все още произвежда слаб тунел.

Пазете оперативните практики отделно

Акаунтните записи, платежните данни и заявките за поддръжка са решения на оператора, които никакъв протоколен текст не ограничава. Одиторският доклад покрива посочени компоненти в рамките на заявен обхват, а политиката за поверителност описва намерения и практики; нито едното замества другото и нито едното не е криптографско твърдение.

Точният извод е кумулативен: спецификацията обяснява дизайна, компилацията и конфигурацията обясняват тунела, а документираните практики на оператора обясняват всичко, което тунелът никога не вижда. Кажете кое от тях сте проверили и твърдението остава вярно.