מערכת הפעלה מאובטחת בקוד פתוח של גוגל KataOS

גוגל הודיעה על גילוי פיתוחים הקשורים לפרויקט KataOS, שמטרתם ליצור מערכת הפעלה מאובטחת עבור חומרה משובצת. רכיבי מערכת KataOS נכתבים ב-Rust ומופעלים על גבי המיקרו-קרנל seL4, שעבורו סופקה הוכחה מתמטית לאמינות במערכות RISC-V, המעידה על כך שהקוד תואם באופן מלא למפרטים המצוינים בשפה הרשמית. קוד הפרויקט פתוח תחת רישיון Apache 2.0.

המערכת מספקת תמיכה לפלטפורמות המבוססות על ארכיטקטורות RISC-V ו-ARM64. כדי לדמות את הפעולה של seL4 וסביבת KataOS על גבי החומרה, נעשה שימוש במסגרת Renode במהלך תהליך הפיתוח. כיישום ייחוס, מוצע מתחם התוכנה והחומרה של Sparrow, המשלב את KataOS עם שבבים מאובטחים המבוססים על פלטפורמת OpenTitan. הפתרון המוצע מאפשר לך לשלב ליבת מערכת הפעלה מאומתת לוגית עם רכיבי חומרה אמינים (RoT, Root of Trust), שנבנו באמצעות פלטפורמת OpenTitan וארכיטקטורת RISC-V. בנוסף לקוד KataOS, מתוכנן לפתוח את כל שאר רכיבי Sparrow, כולל רכיב החומרה, בעתיד.

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

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

להגנה נוספת, כל הרכיבים מלבד המיקרו-קרנל מפותחים באופן מקורי ב-Rust תוך שימוש בטכניקות תכנות בטוחות הממזערות שגיאות זיכרון שמובילות לבעיות כגון גישה לזיכרון לאחר שחרור, הפניית מצביע אפס וחריפות מאגר. ב-Rust נכתבו טוען יישומים בסביבת seL4, שירותי מערכת, מסגרת לפיתוח אפליקציות, API לגישה לקריאות מערכת, מנהל תהליכים, מנגנון להקצאת זיכרון דינמי וכו'. המכלול המאומת משתמש בערכת הכלים CAmkES, שפותחה על ידי פרויקט seL4. ניתן ליצור רכיבים עבור CAmkES גם ב- Rust.

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

מקור: OpenNet.ru