מה מוכיח מפרט פרוטוקול 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

בניות ניתנות לשחזור וסכומי בדיקה מפורסמים מאפשרים לקשר עץ מקור לקובץ בינארי מופץ. בלי החוליה הזו, מקור מפורסם מוכיח רק שבחינה אפשרית, לא שהקובץ שרץ תואם לו.

תצורה שייכת לאותו שלב. ערכות צופן, עמיתים מורשים והגדרות ניתוב הן בחירות פריסה, ובנייה תואמת שהוגדרה ברשלנות עדיין מייצרת מנהרה חלשה.

הפרידו בין נהלי תפעול

רשומות חשבון, נתוני תשלום ופניות תמיכה הם החלטות של המפעיל שאף טקסט פרוטוקול אינו מגביל. דוח ביקורת מכסה רכיבים בשמם בהיקף מוצהר, ומדיניות פרטיות מתארת כוונות ונוהגים; אף אחד מהם אינו מחליף את האחר, ואף אחד מהם אינו הצהרה קריפטוגרפית.

המסקנה המדויקת מצטברת: המפרט מסביר את התכנון, הבנייה והתצורה מסבירות את המנהרה, והנוהגים המתועדים של המפעיל מסבירים כל מה שהמנהרה אינה רואה לעולם. אמרו מה מכל אלה אימתתם, והטענה נשארת נכונה.