โครงการไมโครเคอร์เนลแบบเปิด seL4 ได้รับรางวัล ACM Software System Award ซึ่งเป็นรางวัลประจำปีที่มอบให้โดย Association for Computing Machinery (ACM) ซึ่งเป็นองค์กรระหว่างประเทศที่ได้รับการยอมรับมากที่สุดในสาขาระบบคอมพิวเตอร์ รางวัลนี้มอบให้สำหรับความสำเร็จในด้านการพิสูจน์การดำเนินการทางคณิตศาสตร์ ซึ่งบ่งชี้ถึงการปฏิบัติตามข้อกำหนดที่กำหนดในภาษาที่เป็นทางการอย่างครบถ้วน และเป็นการแสดงถึงความพร้อมสำหรับการใช้งานในภารกิจที่สำคัญยิ่ง โครงการ seL4 แสดงให้เห็นว่าไม่เพียงแต่เป็นไปได้ที่จะตรวจสอบความน่าเชื่อถือและความปลอดภัยอย่างเป็นทางการอย่างสมบูรณ์สำหรับโครงการในระดับระบบปฏิบัติการอุตสาหกรรมเท่านั้น แต่ยังทำได้สำเร็จโดยไม่สูญเสียประสิทธิภาพและความอเนกประสงค์
รางวัล ACM Software System Award จัดขึ้นเป็นประจำทุกปีเพื่อยกย่องการพัฒนาระบบซอฟต์แวร์ที่มีผลกระทบที่ชัดเจนต่ออุตสาหกรรม นำเสนอแนวคิดใหม่ๆ หรือเปิดแอปพลิเคชันเชิงพาณิชย์ใหม่ๆ จำนวนรางวัลคือ 35 ดอลลาร์สหรัฐ ในปีที่ผ่านมา รางวัล ACM มอบให้กับโครงการ GCC และ LLVM และผู้ก่อตั้ง Richard Stallman และ Chris Latner โครงการและเทคโนโลยีอื่นๆ ที่ได้รับรางวัล ได้แก่ UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB และ eclipse .
สถาปัตยกรรมของ microkernel seL4 มีความโดดเด่นในเรื่องการถอดชิ้นส่วนสำหรับจัดการทรัพยากรเคอร์เนลในพื้นที่ผู้ใช้ และสำหรับการใช้วิธีการควบคุมการเข้าถึงแบบเดียวกันสำหรับทรัพยากรดังกล่าว เช่นเดียวกับทรัพยากรของผู้ใช้ ไมโครเคอร์เนลไม่มีนามธรรมระดับสูงสำหรับการจัดการไฟล์ กระบวนการ การเชื่อมต่อเครือข่าย และอื่น ๆ ที่คล้ายคลึงกัน แต่จะจัดเตรียมกลไกขั้นต่ำสำหรับการควบคุมการเข้าถึงพื้นที่ที่อยู่ทางกายภาพ การขัดจังหวะ และทรัพยากรตัวประมวลผล สิ่งที่เป็นนามธรรมระดับสูงและไดรเวอร์สำหรับการโต้ตอบกับฮาร์ดแวร์จะถูกนำไปใช้แยกต่างหากที่ด้านบนของไมโครเคอร์เนลในรูปแบบของงานระดับผู้ใช้ การเข้าถึงงานดังกล่าวไปยังทรัพยากรที่มีให้ไมโครเคอร์เนลนั้นถูกจัดระเบียบตามคำจำกัดความของกฎ
ที่มา: opennet.ru