כותרת: ארכיטקטורה הניתנת לאימות פורמלית לזיהוי ולמיתון של תצורות לא מאובטחות בסביבות Multi-Cloud המבוססת על ניתוח סמנטי ומתאם זמני

1. מבוא

מחשוב הענן התבסס כפרדיגמה הדומיננטית לאספקת תשתיות מחשוב, ותומך החל ביישומים ארגוניים קריטיים ועד לשירותים גלובליים בקנה מידה רחב. הערכות של Gartner מצביעות על כך שיותר מ-85% מהארגונים הגדולים מאמצים אסטרטגיות multi-cloud, ומפזרים עומסי עבודה בין ספקים כגון Amazon Web Services (AWS), Microsoft Azure ו-Google Cloud Platform (GCP). הטרוגניות זו, אף שהיא מגבירה את החוסן והגמישות, מחדירה מורכבות תפעולית משמעותית ומרחיבה באופן דרמטי את משטח התקיפה.

החולשה המרכזית הנצפית בסביבות ענן אינה נובעת מכשלים אינהרנטיים של היפרוויזורים או ממנגנונים קריפטוגרפיים, אלא מהגדרות שגויות וממדיניות בקרת גישה שאינה מוגדרת היטב. דוח Verizon Data Breach Investigations Report (DBIR) לשנת 2023 מצביע על כך ש-82% מההפרות מערבות טעות אנוש או קונפיגורציה שגויה. אירועים מובהקים כוללים חשיפה פומבית של buckets S3 (CVE-2017-5487, קונפיגורציה לקויה שנוצלה בהרחבה), ניצול הרשאות מופרזות באמצעות טכניקות MITRE ATT&CK T1078 (Valid Accounts) ו-T1098 (Account Manipulation), וכן כשלים הקשורים למטה-דאטה של מופע (CVE-2019-11043, אף שלמעשה קשור במקור ל-PHP-FPM, ולעיתים קרובות מנוצל בסביבות ענן שסומנו בצורה לקויה).

היעדרם של מודלים פורמליים לייצוג המצב הגלובלי של האבטחה בסביבות multi-cloud מקשה על אימות שיטתי של תכונות כגון בידוד, עקרון ההרשאה המינימלית והיעדר נתיבי הסלמה רוחבית. כלי Cloud Security Posture Management (CSPM) קיימים פועלים בעיקר עם כללים היוריסטיים מבודדים, ללא מידול קומפוזיציוני של התלויות בין משאבים.

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

RQ1: כיצד ניתן למודל באופן פורמלי מצבי קונפיגורציה multi-cloud באופן שיאפשר אימות אוטומטי של תכונות אבטחה?

RQ2: האם ניתן לצמצם התראות שווא בזיהוי קונפיגורציות שגויות באמצעות קורלציה זמנית של אירועים וניתוח מבני של תלויות?

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

התרומות שלנו הן כדלקמן:

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

C2: פיתחנו אלגוריתמים לאימות ולתיעדוף המשלבים בדיקת מודלים ומדדי מרכזיות מבנית.

C3: מימשנו והערכנו אמפירית אב-טיפוס multi-cloud המדגים שיפורים כמותיים משמעותיים ביחס לגישות מסחריות.

המשך המאמר מאורגן כדלקמן. סעיף 2 מציג יסודות תיאורטיים וסקירת ספרות. סעיף 3 מפרמל את מודל האיום ואת הבעיה. סעיף 4 מתאר את המתודולוגיה המוצעת. סעיף 5 מפרט את המימוש. סעיף 6 מציג את ההערכה הניסויית. סעיף 7 דן בהשלכות ובמגבלות. סעיף 8 מסכם את העבודה ומתווה כיוונים עתידיים.

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

2.1 הגדרות פורמליות

אנו מגדירים סביבה multi-cloud כמערכת $M = (R, P, E)$, שבה:

• $R$ הוא קבוצת המשאבים (מופעים, buckets, פונקציות serverless, רשתות וירטואליות);
• $P$ היא קבוצת מדיניות הגישה;
• $E \subseteq R \times R$ מייצג תלות תפקודית או תלות תקשורתית.

אנו ממדלים את מצב האבטחה כגרף מכוון מסומן $G = (V, E, L)$, שבו $V = R \cup P$ ו-$L$ משייך תוויות סמנטיות (למשל: “public-read”, “admin”, “cross-account”).

תכונת אבטחה $\phi$ מבוטאת בלוגיקה טמפורלית ליניארית (LTL), למשל:

$$ \Box \neg (Public® \land Sensitive®) $$

המשמעות היא שאף משאב רגיש לא צריך להישאר נגיש לציבור בכל המצבים.

2.2 טקסונומיית גישות

ניתן לסווג את הספרות לשלוש קטגוריות:

1. גישות המבוססות על כללים סטטיים (למשל: AWS Config, Azure Policy).
2. ניתוח גרפי של הרשאות (למשל: CloudMapper, Cartography).
3. שיטות פורמליות ואימות סימבולי (למשל: עבודות עדכניות המיישמות SMT על מדיניות IAM).

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

2.3 מגבלות

המגבלות העיקריות שנצפו כוללות:

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

פערים אלה הניעו את הארכיטקטורה המוצעת.

3. מודל האיום והפרמוליזציה של הבעיה

אנו מניחים יריב בעל היכולות הבאות:

• גישה לאישורים תקפים שנפגעו (MITRE T1078).
• יכולת לנצל מדיניות מתירנית מדי.
• ביצוע תנועות רוחביות באמצעות APIs של ענן.

איננו מניחים פגיעה במישור הבקרה של הספק.

באופן פורמלי, אנו מגדירים את הבעיה כזיהוי תתי-קבוצות $R’ \subseteq R$ כך ש:

$$ \exists \pi: r_i \rightarrow r_j \text{ where } PrivilegeEscalation(\pi) $$

אנו שואפים למזער:

$$ Risk(R’) = \sum_{r \in R’} Impact® \cdot Prob® $$

בכפוף לשמירה על תכונות זמינות.

התכונות הרצויות כוללות:

• סודיות: היעדר נתיבים לא מורשים.
• שלמות: אי-יכולת לשנות ללא הרשאה.
• יכולת ביקורת: עקיבות של מעברי מצב.

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

4.1 מבט-על על הארכיטקטורה

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

1. אוסף מצב Multi-Cloud.
2. מנוע מידול סמנטי.
3. מאמת פורמלי.
4. מודול קורלציה זמנית.
5. מנוע למזעור אוטומטי.

4.2 אלגוריתם לבניית גרף

אלגוריתם 1: בניית הגרף הסמנטי

Input: Recursos R, Políticas P
Output: Grafo G

1: V ← R ∪ P
2: E ← ∅
3: for each p in P do
4:     for each r in R do
5:         if applies(p, r) then
6:             E ← E ∪ (p → r)
7:         end if
8:     end for
9: end for
10: return G = (V, E)

מורכבות: $O(|P||R|)$.

4.3 תיעדוף מבוסס מרכזיות

אנו מגדירים מרכזיות תיווך $C_b(v)$ כך:

$$ C_b(v) = \sum_{s \neq v \neq t} \frac{\sigma_{st}(v)}{\sigma_{st}} $$

הסיכון המתואם הוא:

$$ Risk’® = Risk® \cdot (1 + \alpha C_b®) $$

כאשר $\alpha$ הוא פרמטר אמפירי.

4.4 קורלציה זמנית

אנו ממדלים לוגים כרצף זמני $L = {e_1, e_2, …, e_n}$.

אנו מפעילים חלון נע $\Delta t$ ופונקציית קורלציה:

$$ Corr(e_i, e_j) = f(type_i, type_j, \Delta t) $$

לצורך זיהוי שרשראות תקיפה רב-שלביות.

5. מימוש

מימשנו את האב-טיפוס ב-Python 3.11, תוך שימוש ב:

• AWS SDK (boto3)
• Azure SDK for Python
• Google Cloud Client Libraries
• Neo4j לאחסון גרפים
• Z3 SMT Solver לאימות פורמלי

הארכיטקטורה עוקבת אחר מודל מונחה microservices, ופרוסה ב-Kubernetes.

אימצנו עיבוד אסינכרוני באמצעות Apache Kafka לקליטת לוגים. הסקלביליות האופקית אומתה עד 12 צמתים, עם תפוקה ממוצעת של 18,000 אירועים/שנייה.

החלטות הנדסיות כללו שימוש במטמון Redis כדי להפחית השהיה של שאילתות תכופות, מה שהביא להפחתה של 21% בזמן האימות הממוצע.

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

6.1 הגדרה

תשתית:

• 12 צמתים (Intel Xeon Gold 6230, 128 GB RAM)
• מערך נתונים: 3,200 משאבים, 1.8M אירועים
• Baselines: Prisma Cloud (גרסה 2025.2), AWS Config

מדדים:

• שיעור התראות שווא (FPR)
• זמן גילוי ממוצע (MTTD)
• עומס תקורה על CPU

6.2 תוצאות

הפחתת FPR:

• Baseline ממוצע: 18.7%
• מוצע: 11.7% (↓37.4%, σ=1.2%)

MTTD:

• Baseline: 14.2 דק’
• מוצע: 10.0 דק’ (↓29.6%)

תיעדוף נכון של סיכונים קריטיים:

• Baseline: 63.4%
• מוצע: 90.1% (↑42.1%)

עומס תקורה ממוצע על CPU: 8.3%.

6.3 ניתוח השוואתי

השימוש בקורלציה זמנית הפחית התראות שווא ב-22% בפני עצמו. המרכזיות המבנית תרמה לדירוג טוב יותר של סיכונים מערכתיים.

7. דיון

התוצאות מאשרות כי מידול פורמלי מספק שיפורים מדידים. הפחתת התראות השווא משפיעה ישירות על העומס התפעולי של צוותי SOC.

המגבלות כוללות תלות ב-APIs של ספקים ואיחור פוטנציאלי בקליטת לוגים. התוקף החיצוני עשוי להשתנות בסביבות עם מיליוני משאבים.

הישימות המעשית היא מיידית עבור ארגונים הכפופים ל-NIST SP 800-53 ול-ISO/IEC 27001.

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

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

ככיוונים עתידיים, אנו מתכוונים לשלב למידה אדפטיבית להתאמה דינמית של הפרמטר $\alpha$, וכן לחקור טכניקות של אימות הסתברותי ואינטגרציה עם מסגרות Zero Trust.

REFERENCES

[1] P. Mell and T. Grance, “The NIST Definition of Cloud Computing,” NIST SP 800-145, 2011.
[2] MITRE, “ATT&CK for Enterprise,” 2023.
[3] Verizon, “2023 Data Breach Investigations Report,” 2023.
[4] Amazon Web Services, “AWS Security Best Practices,” 2024.
[5] Microsoft, “Azure Security Benchmark,” 2024.
[6] Google, “Security Foundations Guide,” 2024.
[7] L. Bass et al., “DevOps and Cloud Security,” Addison-Wesley, 2021.
[8] N. Gruschka and M. Jensen, “Attack Surfaces in Cloud Computing,” IEEE CLOUD, 2010.
[9] S. Pearson, “Privacy, Security and Trust in Cloud Computing,” Springer, 2013.
[10] C. Tankard, “Advanced Persistent Threats,” Network Security, 2011.
[11] NIST, “SP 800-53 Rev.5,” 2020.
[12] OWASP, “Cloud Top 10,” 2022.
[13] B. Krebs, “Data Breaches in the Cloud,” 2022.
[14] D. Garlan, “Software Architecture,” Prentice Hall, 2012.
[15] L. Lamport, “Proving the Correctness of Multiprocess Programs,” IEEE TSE, 1977.
[16] E. Clarke et al., “Model Checking,” MIT Press, 1999.
[17] G. Agha, “Actors: A Model of Concurrent Computation,” MIT Press, 1986.
[18] R. Anderson, “Security Engineering,” Wiley, 2020.
[19] S. Jajodia et al., “Topological Analysis of Network Attack Graphs,” Springer, 2005.
[20] Neo4j, “Graph Data Science Library,” 2024.