המיקרו-קרנל seL4 מאומת מתמטית עבור ארכיטקטורת RISC-V

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

המיקרו-קרנל seL4 אומת תחילה עבור מעבדי ARM של 32 סיביות, ומאוחר יותר עבור מעבדי 64 סיביות x86. יצוין כי השילוב של ארכיטקטורת החומרה הפתוחה RISC-V עם המיקרו-קרנל seL4 הפתוח ישיג רמת אבטחה חדשה, שכן רכיבי החומרה ניתנים לאימות מלאה גם בעתיד, דבר שאי אפשר להשיג עבור ארכיטקטורות חומרה קנייניות.

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

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

RISC-V מספקת מערכת הוראות מכונה פתוחה וגמישה המאפשרת לבנות מיקרו-מעבדים עבור יישומים שרירותיים מבלי לדרוש תמלוגים או מחרוזות המצורפות לשימוש. RISC-V מאפשר לך ליצור SoCs ומעבדים פתוחים לחלוטין. מבוסס כרגע על מפרט RISC-V על ידי חברות וקהילות שונות תחת רישיונות חינמיים שונים (BSD, MIT, Apache 2.0) מתפתח כמה עשרות גרסאות של ליבות מיקרו-מעבד, SoCs ושבבים שכבר מיוצרים. תמיכת RISC-V קיימת מאז ההפצות של Glibc 2.27, binutils 2.30, gcc 7 וליבת לינוקס 4.15.

מקור: OpenNet.ru