פרויקט seL4 זוכה בפרס מערכת תוכנת ACM

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

פרס מערכת התוכנה של ACM מוענק מדי שנה על מנת להכיר בפיתוח של מערכות תוכנה שהייתה להן השפעה מכרעת על התעשייה, הצגת מושגים חדשים או פתיחת יישומים מסחריים חדשים. סכום הפרס הוא 35 אלף דולר אמריקאי. בשנים האחרונות הוענקו פרסי ACM לפרויקטים של GCC ו-LLVM, ולמייסדיהם ריצ'רד סטולמן וכריס לטנר. פרויקטים וטכנולוגיות נוספים שזכו גם הם היו UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB ו-eclipse .

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

מקור: OpenNet.ru