Mida VPN-protokolli spetsifikatsioon tõestab ja mida mitte

Protokollidokument on implementatsioonide vaheline leping ja hoolikas lugemine ütleb, mida kaks vastavat osapoolt vahetavad ja milliseid omadusi disainerid tagada kavatsesid. See ei ütle, milline binaarfail jookseb serveris, millega ühendute, kuidas see server on konfigureeritud ega mis juhtub hiljem teie konto kirjega. Need on kolm erinevat liiki tõendit ja spetsifikatsiooni kui kõiki kolme käsitlemine on viis, kuidas protokolli nimi hakkab tegema tööd, mida ta teha ei saa. Nende kolme lahus hoidmine ongi kogu harjutus.

Dokument on argumendi algus, mitte selle järeldus.

Mida dokument tegelikult määrab

WireGuardi jaoks määratleb protokollikirjeldus Noise IK käepigistuse, fikseeritud primitiivide kogumi, sõnumipaigutused ja transpordiraamistiku, mis seejärel pakette kannab. IKEv2 jaoks on võrreldav artefakt RFC 7296, mis määrab vahetused, kasulikud koormused ja ettepanekute läbirääkimise. Mõlemal juhul on ulatus täpne: sõnumid, olekumasin ja eeldused, mille korral turvaeesmärgid kehtivad.

Valikulised režiimid muudavad lugemise keerulisemaks. Ühe käepigistuse jaoks kehtiv omadus ei pruugi kehtida juurutusele, mis kasutab teistsugust autentimiskorraldust või varukonfiguratsiooni.

Kus garantiid lõpevad

Formaalne analüüs vastab mudelit puudutavale küsimusele. WireGuardi verifitseerimistöö kasutab Tamarini tõestajas sümboolset mudelit, mis võib näidata, et disain peab oma eelduste juures teatud rünnakutele vastu; see ei näita, et tarnitud kasutajaruumi implementatsioonis pole mäluturbe viga. Just selles lõhes mudeli ja masina vahel elavad tõelised juhtumid. Tõestuse lugemine implementatsiooni sertifikaadina on kategooriaviga.

Edasisuunaline salastatus illustreerib sama piiri. Omadus sõltub sellest, et võtmed hävitatakse nii, nagu protokoll ette näeb, ja see on implementatsiooni ja selle keskkonna omadus, mitte sõnumivormingu oma. Kustutamist ette nägev disain ei saa seda peale suruda platvormil, mis viib mälu kettale.

Kihilisanduvad sõltuvused laiendavad lõhet veelgi: TLS-tunnelitagune TLS-teek, kerneli liides, mida kasutab kasutajaruumi tunnel, ja juhuarvugeneraator asuvad kõik väljaspool protokolli teksti.

Jälgige baidid buildini

Liikuge dokumendist artefaktideni, tuvastades versioonid ja võrreldes neid seejärel sellega, mis tegelikult liiklust teenindab. Toode, mis nimetab protokolli, võib lisada provisioneerimis-, telemeetria- ja halduskomponente, mida spetsifikatsioon kunagi ei kirjelda.

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

Reprodutseeritavad buildid ja avaldatud kontrollsummad võimaldavad siduda lähtekoodipuu jagatud binaarfailiga. Ilma selle lülita tõestab avaldatud lähtekood vaid seda, et kontrollimine on võimalik, mitte et jooksev fail sellele vastab.

Konfiguratsioon kuulub samasse sammu. Šifrikomplektid, lubatud osapooled ja marsruutimisseaded on juurutamisvalikud ning hooletult konfigureeritud vastav build tekitab ikkagi nõrga tunneli.

Hoidke töötamispraktikad eraldi

Kontokirjed, makseandmed ja tugipöördumised on operaatori otsused, mida ükski protokollitekst ei piira. Auditiraport katab nimetatud komponendid deklareeritud ulatuses ja privaatsuspoliitika kirjeldab kavatsusi ja praktikaid; kumbki ei asenda teist ja kumbki ei ole krüptograafiline väide.

Täpne järeldus on kumulatiivne: spetsifikatsioon selgitab disaini, build ja konfiguratsioon selgitavad tunnelit ning operaatori dokumenteeritud praktikad selgitavad kõike, mida tunnel kunagi ei näe. Öelge, mida neist kontrollisite, ja väide jääb tõeseks.