RISC-V אימת את המיקרו-קרנל seL4 במעבדי ה- RV64 שלהם

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

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

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

אודות seL4

ארכיטקטורת seL4 בולט בהסרת חלקים לניהול משאבי הליבה במרחב המשתמשים והשתמש באותן שיטות בקרת גישה למשאבים כאלה כמו למשאבי משתמשים.

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

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

הגישה של משימות כאלה למשאבים הזמינים במיקרו-קרנל מאורגנת באמצעות הגדרת כללים.

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

RISC-V מאפשר לך ליצור מעבדים ו- SoC פתוחים לחלוטין. נכון לעכשיו, על בסיס מפרט RISC-V, כמה חברות וקהילות תחת רישיונות חופשיים שונים (BSD, MIT, Apache 2.0) מפתחות כמה עשרות גרסאות של ליבות מיקרו-מעבדים שכבר יוצרו, SoCs וצ'יפס.

תמיכת RISC-V קיימת מאז שחרורם של Glibc 2.27, binutils 2.30, gcc 7 וליבת הלינה 4.15.

על בדיקת מיקרו-קרנל seL4

בתחילה, המיקרו-קרנל seL4 אומתה עבור מעבדי ARM של 32 סיביות, ו מאוחר יותר עבור מעבדי 86 סיביות x64.

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

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

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

המציאות היא שאנחנו יכולים להיות די בטוחים שלא. חומרה אינה שונה מתוכנה בכך ששניהם באגי.

אך לקיום ISA פתוח יש יתרונות שמעבר להיותם ללא מלכים. האחת היא שהיא מאפשרת יישומי חומרה בקוד פתוח.

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

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

לבסוף, אם ברצונך לדעת יותר על כך, תוכל להתייעץ עם ההערה ב הקישור הבא.