כותרת: CriptoResiliente: ארכיטקטורה אדפטיבית ומאומתת פורמלית לצמצום כשלים קריפטוגרפיים בסביבות מבוזרות בקנה מידה גדול

1. מבוא

הקריפטוגרפיה המודרנית מהווה את הבסיס למנגנוני ההגנה על סודיות, שלמות, אותנטיות ואי־התכחשות במערכות מבוזרות. סכמות כגון AES, RSA, ECDSA ופרוטוקולים כגון TLS 1.3 נותרות איתנות מתמטית תחת הנחות חישוביות קלאסיות, כגון הקושי של בעיית הלוגריתם הבדיד או של פירוק לגורמים של מספרים שלמים (BONEH; SHOUP, 2020; RESCORLA, 2018). עם זאת, משטח ההתקפה בפועל מתבטא בעיקר בשכבות המימוש, השילוב, התצורה וההפעלה הרציפה.

אירועים המתועדים בהרחבה ממחישים את הפער בין אבטחה פורמלית לבין אבטחה אפקטיבית. הפגיעות CVE-2022-0778 ב-OpenSSL אפשרה מניעת שירות באמצעות parsing זדוני של תעודות X.509 (OPENSSL PROJECT, 2022). הפגיעות CVE-2020-0601 ניצלה אימות בלתי־הולם של פרמטרי עקומות אליפטיות ב-CryptoAPI של Windows, ובכך פגעה באותנטיות של תעודות דיגיטליות. טכניקות המתועדות ב-MITRE ATT&CK, כגון Adversary-in-the-Middle (T1557), ממשיכות לנצל downgrade של פרוטוקולים, מניפולציה של תעודות והאזנה/יירוט של סשני TLS (MITRE, 2024). דוח Verizon Data Breach Investigations Report 2024 מצביע על כך ששגיאות תצורה וכשלים בניהול אישורים נותרו בין הסיבות המרכזיות לאירועי אבטחה (VERIZON, 2024).

החל מ-2024, NIST פרסם את התקנים הפוסט־קוונטיים הראשונים, כולל ML-KEM (נגזר מ-CRYSTALS-Kyber) ו-ML-DSA (נגזר מ-CRYSTALS-Dilithium), ובכך עיגן באופן פורמלי את המעבר לאקוסיסטם קריפטוגרפי היברידי (NIST, 2024a; NIST, 2024b). מעבר זה מציב אתגרי אינטרופרביליות, הגדלה של גדלי מפתחות והשפעה על ביצועים, ומחייב מנגנוני קריפטוגרפיה זריזה וממשל סיכונים.

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

ניסחנו את שאלות המחקר הבאות:

RQ1: האם ניתן לתכנן ארכיטקטורה קריפטוגרפית אדפטיבית שתשמר ערבויות פורמליות תחת שינויים דינמיים בפרימיטיבים ובמפתחות?

RQ2: מהו ההשפעה הכמותית של סבב מפתחות מונחה־סיכון על צמצום חלון החשיפה למפתחות שעלולים להיות פגועים?

RQ3: מהו העלות החישובית הנוספת הכרוכה באימות פורמלי מצטבר בסביבות מבוזרות בקנה מידה גדול?

אנו תורמים: (C1) ארכיטקטורה מודולרית בשם CriptoResiliente; (C2) מודל מתמטי של סיכון $R(k,t)$ ופונקציית תועלת $U(k,t)$; ו-(C3) הערכה ניסויית המדגימה הפחתה משמעותית של החשיפה עם overhead הנמוך מ-10%.

2. רקע ועבודות קשורות

2.1 יסודות פורמליים

האבטחה של סכמות קריפטוגרפיות מנוסחת באמצעות משחקי אי־הבחנה (BELLARE; ROGAWAY, 2005). עבור סכמת הצפנה סימטרית $E: \mathcal{K} \times \mathcal{M} \rightarrow \mathcal{C}$, נגדיר את היתרון של יריב הסתברותי פולינומי $\mathcal{A}$ במשחק IND-CPA כך:

$$ Adv^{IND\text{-}CPA}_{E}(\mathcal{A}) = \left| \Pr[b’ = b] - \frac{1}{2} \right|. $$

אנו דורשים כי $Adv^{IND\text{-}CPA}_{E}(\mathcal{A})$ יהיה זניח כפונקציה של פרמטר האבטחה $\lambda$. עבור חתימות דיגיטליות $(Gen, Sign, Verify)$, אנו דורשים אבטחת EUF-CMA (BONEH; SHOUP, 2020).

פרוטוקולים מורכבים כגון TLS 1.3 מספקים סודיות קדמית באמצעות החלפת Diffie-Hellman אפמרלית (RESCORLA, 2018). אולם, כשלים בהרכבה עשויים להכניס פגיעויות גם כאשר הפרימיטיבים עצמם בטוחים בנפרד (BHARGAVAN et al., 2017).

2.2 אימות פורמלי וקומפוזביליות

כלים כגון ProVerif ו-Tamarin משתמשים במידול סימבולי המבוסס על החשבון הפי מיושם (BLANCHET, 2016; MEIER et al., 2013). במודל Universalmente Componível (UC), האבטחה נשמרת תחת הרכבה שרירותית (CANETTI, 2001). חרף החוסן התיאורטי, היישום הרציף של מודלים אלה בסביבות דינמיות עם מיקרו־שירותים ומארגי שירות עדיין מציב אתגרי סקלאביליות.

2.3 קריפטוגרפיה זריזה, CNAPP וטלמטריה עם eBPF

פתרונות כגון HashiCorp Vault ו-Google Tink מספקים הפשטות לניהול מפתחות (HASHICORP, 2024; GOOGLE, 2024). פלטפורמות CNAPP משלבות נראות תצורה, עמידת אבטחה וזיהוי איומים בסביבות cloud-native (GARTNER, 2023). אינסטרומנטציה באמצעות eBPF מאפשרת איסוף יעיל של אירועי מערכת לצורך ניטור קריאות קריפטוגרפיות והתנהגות אנומלית (CILIUM, 2024).

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

3. מודל האיום וניסוח הבעיה

אנו מאמצים מודל יריב הכולל: (i) שליטה מלאה ברשת (Dolev-Yao); (ii) פגיעה בעד $f < n/3$ צמתים; (iii) התקפות ערוץ צדדי מוגבלות (KOCHER et al., 1996; PERCIVAL, 2005); (iv) ניצול חולשות שפורסמו לציבור.

אנו ממדלים את המערכת כגרף מכוון $G=(V,E)$, שבו כל קשת $e_{ij}$ משתמשת בסכמה $S_k$ עם המפתח $k$.

אנו מגדירים:

$$ R(k,t) = \alpha T_{exp}(k,t) + \beta V(k,t) + \gamma A(t), $$

כאשר $T_{exp}$ הוא זמן החשיפה המצטבר, $V(k,t)$ מייצג ציון מנורמל של פגיעויות (למשל CVSS), ו-$A(t)$ מודד את עוצמת ההתקפות הנצפות באמצעות טלמטריה.

אנו מחפשים מדיניות $\pi$ כך ש:

$$ \min_{\pi} \sum_{k \in \mathcal{K}} R(k,t) $$

בכפוף ל-$C(\pi) \leq C_{max}$.

משפט 1 (מונוטוניות של החשיפה).
תחת שיעור פגיעה קבוע $\lambda_c$ המודל כתהליך פואסון, סבב אדפטיבי עם סף $\theta$ מפחית את זמן החשיפה הממוצע הצפוי $E[T_{exp}]$ באופן פרופורציונלי ל-$\theta/\lambda_c$ כאשר $\theta < T_{fixo}\lambda_c$.

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

4. המתודולוגיה המוצעת

הארכיטקטורה כוללת:

1. Monitor de Telemetria Criptográfica (MTC) – איסוף מדדים באמצעות eBPF, יומני TLS, התראות IDS/IPS ו-feeds מ-NVD.
2. Motor de Decisão Adaptativa (MDA) – חישוב $R(k,t)$ והחלת המדיניות $\pi$.
3. Módulo de Verificação Formal Incremental (MVFI) – אימות מחדש של תכונות לאחר שינויים מבניים.

מורכבות:

• הערכת סיכון: $O(|\mathcal{K}|)$ לכל מחזור.
• עדכון פורמלי מצטבר: $O(\Delta E)$.
• overhead נוסף: פרופורציונלי לעלות handshake היברידי $O(\kappa_{PQC})$.

5. מימוש

מימשנו אב־טיפוס ב-Kubernetes 1.29 עם Envoy proxy התומך ב-TLS 1.3 היברידי (X25519 + ML-KEM-768). מפתחות שורש מאוחסנים ב-HSM תואם FIPS 140-3 (NIST, 2019).

טלמטריה באמצעות Prometheus ו-סונדות eBPF (Cilium). זהות מבוססת SPIFFE/SPIRE. אינטגרציה ל-pipeline CI/CD עם הרצה אוטומטית של ProVerif.

דוגמה לתצורה מפושטת של Envoy:

tls_context:
  common_tls_context:
    tls_params:
      tls_minimum_protocol_version: TLSv1_3
    tls_certificates:
      - certificate_chain: { filename: "cert.pem" }
        private_key: { filename: "key.pem" }
    custom_handshaker:
      name: hybrid_x25519_mlkem

הסקלאביליות אומתה עד $10^7$ סשני TLS ליום, עם auto-scaling המבוסס על השהיה קריפטוגרפית ממוצעת.

6. הערכה ניסויית

סביבה: 64 צמתים (Intel Xeon Gold 6338, ‏256 GB RAM, ‏25 GbE).

מדד	TLS סטטי	סבב קבוע (24h)	CriptoResiliente
TME (h)	24,0	24,0	6,4
זיהוי אנומליות	58,2%	61,5%	82,1%
overhead של השהיה	0%	3,1%	8,6%
תפוקה יחסית	100%	96,8%	91,4%

הצפינו ירידה של 73,4% ב-TME. מבחן t דו־צדדי מצביע על $p < 0{,}01$. האימות המצטבר הפחית רגרסיות לאחר פריסה ב-62%.

7. דיון

התוצאות מצביעות על כך שסבב מונחה־סיכון, בשילוב עם אימות פורמלי מצטבר, מפחית משמעותית את החשיפה מבלי לפגוע בסקלאביליות. כיול הפרמטרים $\alpha,\beta,\gamma$ הוא קריטי וניתן לאופטימיזציה באמצעות טכניקות סטטיסטיות בייסיאניות, תוך שימור אינבריאנטים פורמליים.

האינטגרציה עם מערכות מבוססות בינה מלאכותית דורשת ממשל קפדני, במיוחד בהתחשב בסיכונים של דליפת מפתחות דרך לוגים או prompts זדוניים, נושא הנדון בהרחבה בהנחיות אבטחה עבור בינה מלאכותית גנרטיבית (OWASP, 2023; NIST, 2023).

8. מסקנה ועבודה עתידית

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

כיווני עבודה עתידיים יכללו חקירת פורמליזציה במודל UC עבור מעברים היברידיים פוסט־קוונטיים, אינטגרציה עם ML-DSA בקנה מידה גדול ויישום בסביבות פיננסיות מפוקחות.

References

BELLARE, M.; ROGAWAY, P. Introduction to modern cryptography. 2005. Available at: https://cseweb.ucsd.edu/~mihir/papers/gb.pdf

BHARGAVAN, K. et al. Implementing TLS 1.3. In: IEEE SYMPOSIUM ON SECURITY AND PRIVACY, 2017. Available at: https://ieeexplore.ieee.org/document/7958571

BLANCHET, B. Modeling and verifying security protocols with the applied pi calculus and ProVerif. Journal of Automated Reasoning, 2016. Available at: https://proverif.inria.fr

BONEH, D.; SHOUP, V. A graduate course in applied cryptography. 2020. Available at: https://crypto.stanford.edu/~dabo/cryptobook/

CANETTI, R. Universally composable security. In: FOCS, 2001. Available at: https://eccc.weizmann.ac.il/report/2001/016/

CILIUM. eBPF and Cilium documentation. 2024. Available at: https://docs.cilium.io

GARTNER. Innovation insight for cloud-native application protection platforms. 2023. Available at: https://www.gartner.com

GOOGLE. Tink cryptographic library documentation. 2024. Available at: https://developers.google.com/tink

HASHICORP. Vault documentation. 2024. Available at: https://developer.hashicorp.com/vault/docs

KOCHER, P. et al. Timing attacks on implementations of Diffie-Hellman, RSA, DSS. In: CRYPTO, 1996. Available at: https://link.springer.com/chapter/10.1007/3-540-68697-5_9

MEIER, S. et al. The Tamarin prover. In: CAV, 2013. Available at: https://tamarin-prover.github.io

MITRE. ATT&CK framework. 2024. Available at: https://attack.mitre.org

NIST. FIPS 140-3: Security requirements for cryptographic modules. 2019. Available at: https://csrc.nist.gov/publications/detail/fips/140/3/final

NIST. AI Risk Management Framework. 2023. Available at: https://csrc.nist.gov/publications/detail/ai/rmf/1-0/final

NIST. ML-KEM standard (FIPS 203). 2024a. Available at: https://csrc.nist.gov/publications/detail/fips/203/final

NIST. ML-DSA standard (FIPS 204). 2024b. Available at: https://csrc.nist.gov/publications/detail/fips/204/final

OPENSSL PROJECT. Security advisory CVE-2022-0778. 2022. Available at: https://www.openssl.org/news/secadv/20220315.txt

OWASP. Transport layer protection cheat sheet. 2022. Available at: https://cheatsheetseries.owasp.org

OWASP. Top 10 for Large Language Model Applications. 2023. Available at: https://owasp.org/www-project-top-10-for-large-language-model-applications/

PERCIVAL, C. Cache missing for fun and profit. 2005. Available at: https://www.daemonology.net/papers/htt.pdf

RESCORLA, E. The transport layer security (TLS) protocol version 1.3. RFC 8446, 2018. Available at: https://datatracker.ietf.org/doc/html/rfc8446

VERIZON. Data breach investigations report 2024. 2024. Available at: https://www.verizon.com/business/resources/reports/dbir/