แนะนำไมโครเคอร์เนล seL4 [PDF]

• seL4 เป็นไมโครเคอร์เนลของระบบปฏิบัติการ ที่รันในโหมดเคอร์เนลด้วยโค้ดให้น้อยที่สุดเพื่อควบคุมทรัพยากรฮาร์ดแวร์และเสริมความปลอดภัย
• อยู่ในตระกูลไมโครเคอร์เนล L4 และมีการพัฒนามาตั้งแต่ช่วงกลางทศวรรษ 1990
• สามารถทำงานเป็นไฮเปอร์ไวเซอร์ได้ จึงรองรับการรัน guest OS แบบ Linux
• เป็นเคอร์เนลระบบปฏิบัติการตัวแรกของโลกที่พิสูจน์ความถูกต้องเชิงฟังก์ชันได้ โดยมีการพิสูจน์ทางคณิตศาสตร์เสร็จสมบูรณ์ในระดับโค้ด
• ใช้โมเดลความปลอดภัยแบบอิง Capability (ความสามารถ) เพื่อการควบคุมการเข้าถึงอย่างละเอียด

โครงสร้างของ seL4 และความสามารถด้านไฮเปอร์ไวเซอร์

• โมโนลิธิกเคอร์เนล vs ไมโครเคอร์เนล
  • โมโนลิธิกเคอร์เนล (Linux เป็นต้น): โค้ดเคอร์เนลมีขนาดใหญ่มาก จึงมีช่องโหว่ด้านความปลอดภัยจำนวนมาก → ประมาณ 20 ล้านบรรทัดโค้ด (20M SLOC)
  • ไมโครเคอร์เนล (seL4): ใช้โค้ดเคอร์เนลให้น้อยที่สุด → ประมาณ 10,000 บรรทัดโค้ด (10K SLOC)
  • การลดขนาดเคอร์เนล → เสริมความปลอดภัยและลดพื้นผิวการโจมตี
• seL4 ทำหน้าที่เป็นไฮเปอร์ไวเซอร์ได้
  • สามารถรัน guest OS เต็มรูปแบบอย่าง Linux ภายใน VM ได้
  • แต่ละ VM ทำงานแยกจากกันโดยอิสระและไม่สามารถรบกวนกันได้ → รับประกันการแยกส่วนที่แข็งแกร่ง
  • การเรียกโพรซีเยอร์แบบป้องกัน (PPC) → ทำให้สื่อสารอย่างปลอดภัยระหว่าง VM ได้

การตรวจพิสูจน์และโมเดลความปลอดภัยของ seL4

• การตรวจพิสูจน์ความถูกต้องเชิงฟังก์ชัน
  • seL4 ได้รับการพิสูจน์ทางคณิตศาสตร์ในระดับโค้ดว่าทำงานได้ถูกต้องตามหน้าที่
  • รับประกันว่าการทำงานทั้งหมดของเคอร์เนลเป็นไปตามสเปก
• การตรวจพิสูจน์การแปล (Translation Validation)
  • พิสูจน์ว่าโค้ดไบนารีที่คอมไพเลอร์สร้างขึ้นตรงกับโค้ด C ต้นฉบับอย่างถูกต้อง
  • ดำเนินการผ่าน toolchain แบบอัตโนมัติ
• การตรวจพิสูจน์คุณสมบัติด้านความปลอดภัย
  • ความลับ (Confidentiality): เข้าถึงข้อมูลได้เฉพาะเมื่อได้รับอนุญาตไว้อย่างชัดเจนเท่านั้น
  • ความสมบูรณ์ถูกต้อง (Integrity): แก้ไขข้อมูลได้เฉพาะเมื่อได้รับอนุญาตไว้อย่างชัดเจนเท่านั้น
  • ความพร้อมใช้งาน (Availability): ใช้ทรัพยากรได้เฉพาะเมื่อได้รับอนุญาตไว้อย่างชัดเจนเท่านั้น

โมเดลความปลอดภัยแบบอิง Capability

• Capability คืออะไร?
  • โทเคนความปลอดภัยที่มอบสิทธิ์การเข้าถึงต่อออบเจ็กต์ที่กำหนด
  • เข้ารหัสทั้งการอ้างอิงออบเจ็กต์และสิทธิ์การเข้าถึงไว้ด้วยกัน
  • ควบคุมการเข้าถึงได้อย่างละเอียด → ใช้หลักสิทธิ์เท่าที่จำเป็น (Principle of Least Privilege, POLA)
• ข้อดีของ Capability
  • ควบคุมการเข้าถึงได้ละเอียด → ลดสิทธิ์ให้เหลือน้อยที่สุดได้
  • สามารถมอบสิทธิ์ต่อ (Delegation) และเพิกถอนสิทธิ์ได้
  • เป็นโมเดลความปลอดภัยที่แข็งแกร่ง → เหนือกว่าโมเดลควบคุมการเข้าถึงแบบดั้งเดิม (ACL)
• การแก้ปัญหา confused deputy
  • ในระบบแบบ ACL ดั้งเดิม สถานะความปลอดภัยจะถูกกำหนดตาม security ID ของผู้กระทำ
  • ใน seL4 Capability จะเป็นตัวกำหนดสิทธิ์ด้านความปลอดภัยโดยตรง → ทำให้ควบคุมสิทธิ์ได้อย่างชัดเจน

การรองรับระบบเรียลไทม์และระบบผสมระดับความสำคัญ

• รองรับระบบเรียลไทม์
  • seL4 รองรับการจัดตารางเวลาแบบอิงลำดับความสำคัญ
  • มีการวิเคราะห์เวลารันสูงสุดในกรณีเลวร้ายที่สุด (WCET) ของงานทั้งหมดในเคอร์เนลครบถ้วนแล้ว → รับประกัน hard real-time
• รองรับระบบผสมระดับความสำคัญ (Mixed-Criticality System, MCS)
  • จัดสรรและแยกทรัพยากร CPU ตาม scheduling context
  • ควบคุมไม่ให้งานที่มีลำดับความสำคัญสูงผูกขาด CPU
  • สามารถรันงานวิกฤตและงานไม่วิกฤตพร้อมกันได้

ประสิทธิภาพและความมีประสิทธิผล

• ไมโครเคอร์เนลที่มีประสิทธิภาพสูงสุด
  • แม้ในกรณีที่ประสิทธิภาพมีความสำคัญ ก็ไม่ต้องลดทอนความปลอดภัย
  • ค่าใช้จ่ายของ system call และ IPC ต่ำมาก → เร็วกว่าระบบคู่แข่งมากกว่า 5 เท่า
• ประสิทธิภาพเหนือกว่าระบบคู่แข่ง
  • Fiasco.OC: ช้ากว่า seL4 ประมาณ 2 เท่า
  • Zircon: ช้ากว่า seL4 ประมาณ 9 เท่า
  • CertiKOS: ช้ากว่า seL4 ประมาณ 5 เท่า

การใช้งานจริงและการเสริมความปลอดภัยแบบค่อยเป็นค่อยไป

• กรณีการใช้งานจริง

  • นำไปใช้สำเร็จใน ULB (เฮลิคอปเตอร์ไร้คนขับ) ของ Boeing
  • ยืนยันได้ว่าช่วยเสริมความปลอดภัยและเพิ่มเสถียรภาพของระบบ

• การเสริมความปลอดภัยให้ระบบเดิมแบบค่อยเป็นค่อยไป (Incremental Cyber Retrofit)

  • รันระบบเดิมภายใน VM พร้อมค่อย ๆ ปรับให้เป็นโมดูลมากขึ้น
  • เสริมความปลอดภัยพร้อมลดผลกระทบต่อประสิทธิภาพให้น้อยที่สุด

บทสรุป

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