RISC-V ตรวจสอบ microkernel seL4 บนโปรเซสเซอร์ RV64

มูลนิธิ RISC-V ประกาศว่าได้ตรวจสอบแล้ว ไมโครเคอร์เนลทำงานอย่างไร seL4 ในระบบที่มี สถาปัตยกรรมชุดคำสั่ง RISC-V. ซึ่งกระบวนการตรวจสอบจะลดลงเป็นการทดสอบทางคณิตศาสตร์ของความน่าเชื่อถือของ seL4 ซึ่งบ่งชี้ถึงการปฏิบัติตามข้อกำหนดที่ระบุไว้ในภาษาทางการ

การทดสอบความน่าเชื่อถือช่วยให้สามารถใช้ seL4 ในระบบภารกิจที่สำคัญโดยใช้โปรเซสเซอร์ RISC-V RV64ซึ่งต้องการความน่าเชื่อถือในระดับที่สูงขึ้นและไม่รับประกันความล้มเหลว

นักพัฒนาซอฟต์แวร์ที่ทำงานบนเคอร์เนล seL4 สามารถมั่นใจได้อย่างสมบูรณ์ว่าในกรณีที่เกิดความล้มเหลวในส่วนหนึ่งของระบบความล้มเหลวนี้จะไม่แพร่กระจายไปยังส่วนที่เหลือของระบบและโดยเฉพาะอย่างยิ่งในส่วนที่สำคัญ

เกี่ยวกับ seL4

สถาปัตยกรรม seL4 มีความโดดเด่นในการลบส่วนต่างๆเพื่อจัดการทรัพยากรเคอร์เนลในพื้นที่ผู้ใช้ และใช้วิธีการควบคุมการเข้าถึงเดียวกันสำหรับทรัพยากรดังกล่าวสำหรับทรัพยากรของผู้ใช้

ไมโครเคอร์เนล ไม่ได้ให้ abstractions ระดับสูง เตรียมจัดการไฟล์กระบวนการการเชื่อมต่อเครือข่าย ฯลฯ แล้ว แต่กลับเป็นเช่นนั้น มีกลไกเพียงเล็กน้อยในการควบคุมการเข้าถึงพื้นที่ที่อยู่ทางกายภาพขัดจังหวะและทรัพยากรตัวประมวลผล

นามธรรมระดับสูงและตัวควบคุมสำหรับการโต้ตอบกับคอมพิวเตอร์จะถูกนำไปใช้งานแยกกันที่ด้านบนของไมโครเคอร์เนลในรูปแบบของงานที่ดำเนินการในระดับผู้ใช้

การเข้าถึงงานดังกล่าวไปยังทรัพยากรที่มีอยู่ในไมโครเคอร์เนลจะถูกจัดระเบียบผ่านการกำหนดกฎ

RISC-V เป็นระบบที่เปิดกว้างและยืดหยุ่น ของคำแนะนำเครื่องที่ อนุญาตให้สร้างไมโครโปรเซสเซอร์สำหรับการใช้งานโดยพลการโดยไม่ต้องหักเงิน และไม่มีการกำหนดเงื่อนไขการใช้งาน

RISC-V ช่วยให้คุณสร้างโปรเซสเซอร์และ SoC แบบเปิดได้อย่างสมบูรณ์ ปัจจุบันตามข้อกำหนด RISC-V บริษัท และชุมชนต่างๆภายใต้ใบอนุญาตฟรีต่างๆ (BSD, MIT, Apache 2.0) กำลังพัฒนาไมโครโปรเซสเซอร์คอร์ SoC และชิปที่ผลิตไปแล้วหลายโหล

การสนับสนุน RISC-V มีมาตั้งแต่การเปิดตัว Glibc 2.27, binutils 2.30, gcc 7 และเคอร์เนล Linux 4.15

เกี่ยวกับการทดสอบไมโครเคอร์เนล seL4

ในขั้นต้นไมโครเคอร์เนล seL4 ได้รับการตรวจสอบสำหรับโปรเซสเซอร์ ARM 32 บิตและ ในภายหลังสำหรับโปรเซสเซอร์ x86 64 บิต.

เป็นที่สังเกตว่าการรวมกันของสถาปัตยกรรมฮาร์ดแวร์แบบเปิด RISC-V กับไมโครเคอร์เนลแบบเปิด seL4 จะได้รับความปลอดภัยระดับใหม่เนื่องจากส่วนประกอบฮาร์ดแวร์ในอนาคตสามารถตรวจสอบได้อย่างสมบูรณ์ซึ่งเป็นไปไม่ได้ที่จะบรรลุสำหรับสถาปัตยกรรมฮาร์ดแวร์ที่เป็นกรรมสิทธิ์

เมื่อเราตรวจสอบ seL4 เราต้องถือว่าฮาร์ดแวร์ทำงานอย่างถูกต้อง (นั่นคือตามที่ระบุไว้) นั่นถือว่ามีข้อกำหนดที่ไม่ชัดเจนในตอนแรกซึ่งไม่ใช่ในกรณีของฮาร์ดแวร์ทั้งหมด 

แต่ถึงแม้ว่าข้อกำหนดดังกล่าวจะมีอยู่และเป็นทางการ (นั่นคือการเรียงลำดับเป็นพิธีการทางคณิตศาสตร์ที่สนับสนุนการให้เหตุผลทางคณิตศาสตร์เกี่ยวกับคุณสมบัติของมัน) เราจะรู้ได้อย่างไรว่ามันจับพฤติกรรมของฮาร์ดแวร์ได้จริง? 

ความจริงก็คือเราค่อนข้างมั่นใจว่ามันไม่ใช่ ฮาร์ดแวร์ไม่แตกต่างจากซอฟต์แวร์ที่ทั้งสองเป็นบั๊ก

แต่การมี ISA แบบเปิดมีข้อดีที่นอกเหนือไปจากการปลอดค่าลิขสิทธิ์ หนึ่งคืออนุญาตให้ใช้ฮาร์ดแวร์โอเพนซอร์ส

เมื่อตรวจสอบ seL4 จะถือว่าอุปกรณ์ทำงานตามที่ระบุและข้อมูลจำเพาะอธิบายลักษณะการทำงานของระบบอย่างครบถ้วน แต่ในความเป็นจริงแล้วอุปกรณ์ไม่มีข้อผิดพลาดซึ่งแสดงให้เห็นได้ดีจากปัญหาที่เกิดขึ้นเป็นประจำในคำแนะนำในการดำเนินการเชิงคาดเดา

แพลตฟอร์มฮาร์ดแวร์แบบเปิดทำให้การรวมการเปลี่ยนแปลงง่ายขึ้น ที่เกี่ยวข้องกับการรักษาความปลอดภัยตัวอย่างเช่นเพื่อป้องกันช่องทางการรั่วไหลที่เป็นไปได้ทั้งหมดผ่านช่องทางของบุคคลที่สามซึ่งการกำจัดปัญหาด้วยฮาร์ดแวร์จะมีประสิทธิภาพมากกว่าการพยายามหาทางแก้ไขด้วยซอฟต์แวร์

สุดท้ายหากคุณต้องการทราบข้อมูลเพิ่มเติมคุณสามารถอ่านบันทึกในไฟล์ ลิงค์ต่อไปนี้