มูลนิธิ RISC-V เกี่ยวกับการตรวจสอบการทำงานของไมโครเคอร์เนล บนระบบที่มีสถาปัตยกรรมชุดคำสั่ง RISC-V การยืนยันลงมาที่ ความน่าเชื่อถือของการดำเนินการ seL4 ซึ่งบ่งบอกถึงการปฏิบัติตามข้อกำหนดที่ระบุในภาษาทางการอย่างสมบูรณ์ หลักฐานความน่าเชื่อถือ seL4 ในระบบที่มีภารกิจสำคัญซึ่งใช้โปรเซสเซอร์ RISC-V RV64 ซึ่งต้องการระดับความน่าเชื่อถือที่เพิ่มขึ้นและรับประกันว่าจะไม่เกิดข้อผิดพลาด นักพัฒนาซอฟต์แวร์ที่ทำงานบนเคอร์เนล seL4 สามารถมั่นใจได้อย่างสมบูรณ์ว่าหากมีความล้มเหลวในส่วนหนึ่งของระบบ ความล้มเหลวนี้จะไม่แพร่กระจายไปยังส่วนที่เหลือของระบบ และโดยเฉพาะอย่างยิ่งส่วนที่สำคัญของระบบ
ไมโครเคอร์เนล seL4 ได้รับการตรวจสอบเบื้องต้นสำหรับโปรเซสเซอร์ ARM 32 บิต และต่อมาสำหรับโปรเซสเซอร์ x64 86 บิต มีข้อสังเกตว่าการรวมกันของสถาปัตยกรรมฮาร์ดแวร์ RISC-V แบบเปิดกับไมโครเคอร์เนล seL4 แบบเปิดจะทำให้ได้รับความปลอดภัยในระดับใหม่ เนื่องจากส่วนประกอบฮาร์ดแวร์จะสามารถตรวจสอบได้อย่างสมบูรณ์ในอนาคต ซึ่งเป็นไปไม่ได้ที่จะบรรลุผลสำหรับสถาปัตยกรรมฮาร์ดแวร์ที่เป็นกรรมสิทธิ์
เมื่อตรวจสอบ seL4 จะถือว่าอุปกรณ์ทำงานตามที่ระบุไว้และข้อกำหนดอธิบายพฤติกรรมของระบบอย่างสมบูรณ์ แต่ในความเป็นจริงแล้ว อุปกรณ์ไม่ได้ปราศจากข้อผิดพลาด ซึ่งแสดงให้เห็นอย่างชัดเจนจากปัญหาที่เกิดขึ้นเป็นประจำในกลไกของการดำเนินการเก็งกำไร คำแนะนำ. แพลตฟอร์มฮาร์ดแวร์แบบเปิดช่วยให้บูรณาการการเปลี่ยนแปลงที่เกี่ยวข้องกับความปลอดภัยได้ง่ายขึ้น ตัวอย่างเช่น เพื่อบล็อกการรั่วไหลของช่องทางด้านข้างทั้งหมด ซึ่งการกำจัดปัญหาในฮาร์ดแวร์จะมีประสิทธิภาพมากกว่าการพยายามค้นหาวิธีแก้ปัญหาในซอฟต์แวร์
จำได้ว่าสถาปัตยกรรม seL4 การเคลื่อนย้ายชิ้นส่วนสำหรับการจัดการทรัพยากรเคอร์เนลในพื้นที่ผู้ใช้และการใช้วิธีการควบคุมการเข้าถึงแบบเดียวกันสำหรับทรัพยากรเช่นเดียวกับทรัพยากรผู้ใช้ ไมโครเคอร์เนลไม่ได้เตรียมนามธรรมระดับสูงไว้แล้วสำหรับจัดการไฟล์ กระบวนการ การเชื่อมต่อเครือข่าย และอื่นๆ แต่กลับให้กลไกเพียงเล็กน้อยเท่านั้นในการควบคุมการเข้าถึงพื้นที่ที่อยู่ทางกายภาพ การขัดจังหวะ และทรัพยากรตัวประมวลผล นามธรรมและไดรเวอร์ระดับสูงสำหรับการโต้ตอบกับฮาร์ดแวร์จะถูกนำไปใช้แยกกันบนไมโครเคอร์เนลในรูปแบบของงานระดับผู้ใช้ การเข้าถึงงานดังกล่าวไปยังทรัพยากรที่มีให้กับไมโครเคอร์เนลนั้นจัดขึ้นตามคำจำกัดความของกฎ
RISC-V จัดให้มีระบบคำสั่งเครื่องจักรแบบเปิดและยืดหยุ่น ซึ่งช่วยให้สามารถสร้างไมโครโปรเซสเซอร์สำหรับการใช้งานที่ต้องการได้โดยไม่จำเป็นต้องผูกมัดหรือผูกมัดใดๆ เพื่อใช้งาน RISC-V ช่วยให้คุณสร้าง SoC และโปรเซสเซอร์แบบเปิดโดยสมบูรณ์ ปัจจุบันอิงตามข้อกำหนด RISC-V โดยบริษัทและชุมชนต่างๆ ภายใต้ใบอนุญาตฟรีต่างๆ (BSD, MIT, Apache 2.0) แกนไมโครโปรเซสเซอร์, SoC และชิปที่ผลิตไปแล้วหลายสิบรุ่น มีการรองรับ RISC-V ตั้งแต่เปิดตัว Glibc 2.27, binutils 2.30, gcc 7 และ Linux kernel 4.15
ที่มา: opennet.ru