בכל פעם שאתה קונה משהו באמזון, נתוני הלקוחות שלך מתעדכנים ומאוחסנים אוטומטית באלפי מכונות וירטואליות בענן. עבור עסקים כמו אמזון, הקפדה על בטיחות ואבטחת הנתונים של מיליוני לקוחותיה היא חיונית. זה נכון לגבי ארגונים גדולים וקטנים כאחד. אך עד כה לא הייתה שום דרך להבטיח שמערכת תוכנה מאובטחת מפני באגים, האקרים ופגיעות.
ייתכן שחוקרי קולומביה הנדסה פתרו את נושא האבטחה הזה. הם פיתחו את SeKVM, המערכת הראשונה שמבטיחה - באמצעות הוכחה מתמטית - את האבטחה של מכונות וירטואליות בענן. במאמר חדש שיוצג ב- 26 במאי 2021, בסימפוזיון ה- 42 של IEEE בנושא אבטחה ופרטיות, החוקרים מקווים להניח את הבסיס לחידושים עתידיים באימות תוכנות מערכת, מה שמוביל לדור חדש של תוכנות מערכת עמידות סייבר.
SeKVM היא המערכת המאומתת באופן רשמי למחשוב ענן. אימות רשמי הוא שלב קריטי מכיוון שהוא תהליך ההוכחה שתוכנה נכונה מתמטית, שקוד התוכנית עובד כמו שצריך, ואין שום באגי אבטחה נסתרים לדאוג.
"זו הפעם הראשונה שמערכת תוכנה מרובת מעבדים בעולם האמיתי הוכחה כנכונה ומאובטחת מבחינה מתמטית", אמר ג'ייסון ניה, פרופסור למדעי המחשב ומנהל שותף במעבדה למערכות תוכנה. "המשמעות היא שנתוני המשתמשים מנוהלים כראוי על ידי תוכנה הפועלת בענן והם בטוחים מפני באגי אבטחה והאקרים."
בניית תוכנת מערכת נכונה ומאובטחת הייתה אחד האתגרים הגדולים של מחשוב. ניה עבד על היבטים שונים של מערכות תוכנה מאז הצטרפותו לקולומביה הנדסה בשנת 1999. כאשר רונגהוי גו, פרופסור עוזר משפחת טאנג למדעי המחשב ומומחה לאימות פורמלי, הצטרף למחלקה למדעי המחשב בשנת 2018, הוא וניה החליטו לשתף פעולה. על בחינת אימות רשמי של מערכות תוכנה.
המחקר שלהם זכה להתעניינות רבה: שני החוקרים זכו בפרס המחקר של אמזון, במענקים מרובים של הקרן הלאומית למדע, וכן בחוזה של סוכנות פרויקט מחקר מתקדם להגנה (DARPA) בהיקף של מיליון מיליון דולר לקידום פיתוח פרויקט SeKVM בנוסף, ניה הוענק מלגת גוגנהיים עבור עבודה זו.
במהלך תריסר השנים האחרונות הוקדשה תשומת לב רבה לאימות פורמלי, כולל עבודה על אימות מערכות הפעלה מרובות מעבדים. "אך כל המחקר נערך על מערכות דומות לצעצועים שאף אחד לא משתמש בהן בחיים האמיתיים", אמר גו. "אימות מערכת סחורות מרובת מעבדים, מערכת בשימוש נרחב כמו לינוקס, נחשבה בלתי אפשרית פחות או יותר."
הצמיחה האקספוננציאלית של מחשוב ענן אפשרה לחברות ולמשתמשים להעביר את הנתונים והחישוב שלהם מחוץ לאתר למכונות וירטואליות הפועלות על מארחים בענן. ספקי מחשוב ענן, כמו אמזון, פורשים מפקחי יתר לתמיכה במכונות הווירטואליות הללו
Hypervisor הוא פיסת התוכנה המרכזית המאפשרת מחשוב ענן. אבטחת הנתונים של המכונה הווירטואלית תלויה בנכונות ובמהימנותו של ה- hypervisor. למרות חשיבותם, היפרוויזורים מסובכים - הם יכולים לכלול מערכת הפעלה שלמה של לינוקס. רק חוליה חלשה אחת בקוד - כזו שלמעשה בלתי אפשרית לזיהוי באמצעות בדיקות מסורתיות - יכולה להפוך את המערכת לפגיעה בפני האקרים. גם אם Hypervisor נכתב בצורה נכונה ב 99%, האקר עדיין יכול להתגנב למערך המסוים הזה של 1% ולהשתלט על המערכת.
עבודתם של ניה וגו היא הראשונה לאמת מערכת סחורות, במיוחד ה- KVM hypervisor הנמצא בשימוש נרחב, המשמש להפעלת מכונות וירטואליות על ידי ספקי ענן כמו אמזון. הם הוכיחו כי SeKVM, שהוא KVM עם כמה שינויים קטנים, הוא מאובטח ומבטיח שמחשבים וירטואליים מבודדים זה מזה.
"הראינו שהמערכת שלנו יכולה להגן על אבטחת נתונים פרטיים ומחשוב שהועלו לענן עם ערבויות מתמטיות," אמר Xupeng Li, דוקטורט בגו. סטודנט ומחבר משותף של העיתון. "זה מעולם לא נעשה לפני כן."
SeKVM אומתה באמצעות MicroV, מסגרת חדשה לאימות מאפייני האבטחה של מערכות גדולות. היא מבוססת על ההשערה ששינויים קטנים במערכת יכולים להקל באופן משמעותי על אימות, טכניקה חדשה שמכנים החוקרים אימות MICR. טכניקת ריבוד חדשה זו מחדשת מערכת קיימת ומחלצת את הרכיבים האוכפים אבטחה לליבה קטנה המאומתת ומבטיחה את אבטחת המערכת כולה.
השינויים הדרושים לחידוש מערכת גדולה הם צנועים למדי - החוקרים הוכיחו שאם הגרעין הקטן של המערכת הגדולה הוא שלם, אז המערכת מאובטחת ולא ידלפו נתונים פרטיים. כך הם הצליחו לאמת מערכת גדולה כמו KVM, שבעבר נחשבה בלתי אפשרית.
"תחשוב על בית - סדק בקיר הגבס לא אומר ששלמות הבית בסכנה," הסביר ניה. "זה עדיין בריא מבנית ומערכת המבנה המרכזית טובה."
שי-וויי לי, הדוקטורט של ניה. סטודנט ומחבר המחקר המשותף, הוסיף, "SeKVM ישמש אמצעי הגנה בתחומים שונים, החל ממערכות בנקאיות ומכשירי האינטרנט של הדברים וכלה בכלי רכב אוטונומיים ומטבעות קריפטוגרפיים."
כמפקח הסחורות המאומת הראשון, SeKVM יכול לשנות את האופן שבו יש לתכנן, לפתח, לפרוס ולסמוך עליהם על שירותי ענן. בעולם שבו אבטחת סייבר הוא דאגה גוברת, גמישות זו מבוקשת מאוד. חברות ענן גדולות כבר בוחנות כיצד הן יכולות למנף את SeKVM כדי לענות על דרישה זו.