Шта доказује спецификација VPN протокола, а шта не

Документ протокола је уговор између имплементација, и пажљиво читање вам каже шта ће две усклађене стране разменити и која су својства дизајнери намеравали да обезбеде. Не каже вам која бинарна датотека ради на серверу на који се повезујете, како је тај сервер конфигурисан ни шта се после дешава са записом вашег рачуна. То су три различите врсте доказа, а третирање спецификације као сва три је начин на који име протокола почиње да ради посао који не може. Раздвајање тих три је цела вежба.

Документ је почетак аргумента, а не његов закључак.

Шта документ заиста одређује

За WireGuard, опис протокола дефинише Noise IK руковање, фиксни скуп примитива, изгледе порука и транспортно уоквиривање које потом носи пакете. За IKEv2 упоредиви артефакт је RFC 7296, који одређује размене, корисна оптерећења и преговарање предлога. У оба случаја обим је прецизан: поруке, машина стања и претпоставке под којима сигурносни циљеви важе.

Необавезни режими компликују читање. Својство које важи за једно руковање можда се не односи на постављање с другачијим распоредом аутентификације или резервном конфигурацијом.

Где гаранције престају

Формална анализа одговара на питање о моделу. WireGuardov рад на верификацији користи симболички модел у 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

Репродуцибилне изградње и објављене контролне суме омогућавају повезивање стабла изворног кода са дистрибуираном бинарном датотеком. Без те везе, објављени извор доказује само да је преглед могућ, а не да датотека која се извршава одговара њему.

Конфигурација припада истом кораку. Скупови шифара, дозвољене стране и поставке усмеравања су избори постављања, а усклађена изградња конфигурисана безбрижно и даље даје слаб тунел.

Држите оперативне праксе одвојено

Записи рачуна, подаци о плаћању и захтеви за подршку су одлуке оператера које ниједан текст протокола не ограничава. Извештај о ревизији покрива именоване компоненте у оквиру наведеног обима, а политика приватности описује намере и праксе; ниједно не замењује друго и ниједно није криптографска изјава.

Прецизан закључак је кумулативан: спецификација објашњава дизајн, изградња и конфигурација објашњавају тунел, а документоване праксе оператера објашњавају све што тунел никада не види. Реците шта сте од тога проверили и тврдња остаје тачна.