שחרור של Muen 1.0, מיקרו-קרנל בקוד פתוח לבניית מערכות אמינות במיוחד

לאחר שמונה שנים של פיתוח, שוחרר פרויקט Muen 1.0, שפיתח את ליבת ההפרדה, שהיעדר שגיאות בקוד המקור שלו אושר באמצעות שיטות מתמטיות של אימות מהימנות פורמלי. הליבה זמינה עבור ארכיטקטורת x86_64 וניתן להשתמש בה במערכות קריטיות למשימה הדורשות רמה מוגברת של אמינות והבטחה ללא תקלות. קוד המקור של הפרויקט כתוב בשפת Ada והדיאלקט הניתן לאימות SPARK 2014. הקוד מופץ תחת רישיון GPLv3.

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

הליבה פועלת במצב VMX root, בדומה ל-hypervisor, וכל שאר הרכיבים פועלים במצב VMX non-root, בדומה למערכות אורחות. הגישה לציוד נעשית באמצעות הרחבות Intel VT-d DMA ומיפוי מחדש של פסיקה, המאפשרת ליישם כריכה מאובטחת של התקני PCI לרכיבים הפועלים תחת Muen.

היכולות של Muen כוללות תמיכה במערכות מרובות ליבות, דפי זיכרון מקוננים (EPT, Extended Page Tables), MSI (הפסקות איתות של הודעות), וטבלאות תכונות דפי זיכרון (PAT, Page Attribute Table). Muen מספקת גם מתזמן סבב קבוע המבוסס על טיימר מנע של Intel VMX, זמן ריצה קומפקטי שאינו משפיע על הביצועים, מערכת ביקורת קריסות, מנגנון הקצאת משאבים סטטי מבוסס כללים, מערכת לטיפול באירועים וערוצי זיכרון משותפים עבור תקשורת בתוך רכיבים פועלים.

הוא תומך ברכיבים עם קוד מכונה של 64 סיביות, מכונות וירטואליות של 32 או 64 סיביות, יישומי 64 סיביות בשפות Ada ו-SPARK 2014, מכונות וירטואליות של לינוקס ו"יוניקרנלים" עצמאיים המבוססים על MirageOS על גבי Muen.

החידושים העיקריים המוצעים במהדורת Muen 1.0:

• פורסמו מסמכים עם מפרטים של הליבה (התקן וארכיטקטורה), מערכת (מדיניות מערכת, Tau0 וערכת כלים) ורכיבים, המתעדים את כל ההיבטים של הפרויקט.
• נוספה ערכת הכלים Tau0 (Muen System Composer), הכוללת סט של רכיבים מאומתים מוכנים להכנת תמונות מערכת ופיתוח שירותים סטנדרטיים הפועלים על גבי Muen. הרכיבים שסופקו כוללים מנהל התקן AHCI (SATA), מנהל ההתקנים (DM), טוען אתחול, מנהל מערכת, מסוף וירטואלי וכו'.
• מנהל ההתקן muenblock Linux (יישום של התקן בלוק הפועל על גבי הזיכרון המשותף של Muen) הומר לשימוש ב-blockdev 2.0 API.
• הוטמע כלים לניהול מחזור החיים של רכיבים מקומיים.
• תמונות המערכת הומרו לשימוש ב-SBS (Signed Block Stream) ו-CSL (Command Stream Loader) כדי להגן על שלמות.
• הוטמע מנהל התקן AHCI-DRV מאומת, שנכתב בשפת SPARK 2014 ומאפשר לחבר כוננים התומכים בממשק ATA או מחיצות דיסק בודדות לרכיבים.
• תמיכת ייחודיות משופרת מפרויקטים של MirageOS ו-Solo5.
• ערכת הכלים לשפת Ada עודכנה עבור מהדורת GNAT Community 2021.
• מערכת האינטגרציה הרציפה הועברה מאמולטור Bochs לסביבות מקוננות של QEMU/KVM.
• תמונות רכיבי לינוקס משתמשות בליבת Linux 5.4.66.

מקור: OpenNet.ru