แนะนำไมโครเคอร์เนล seL4 [PDF]
(sel4.systems)- seL4 เป็นไมโครเคอร์เนลของ OS ที่มุ่งเป้าไปที่ระบบฝังตัวและระบบไซเบอร์-กายภาพที่ให้ความสำคัญกับความมั่นคงปลอดภัยและความปลอดภัย โดยทำหน้าที่แยกและมัลติเพล็กซ์ทรัพยากรฮาร์ดแวร์ แต่ไม่ใช่ OS อเนกประสงค์ที่สมบูรณ์
- ลดโค้ดใน kernel mode เหลือประมาณ 10 kSLOC เพื่อลด TCB และพื้นผิวการโจมตี และผลักบริการของ OS เช่น ระบบไฟล์ เครือข่าย และไดรเวอร์ ไปไว้ใน user mode
- เป็นเคอร์เนล OS ตัวแรกของโลกที่มี การตรวจสอบแบบเป็นทางการ ในระดับโค้ด และในระบบที่กำหนดค่าอย่างถูกต้อง เคอร์เนลยังรับประกันคุณสมบัติด้านความปลอดภัยอย่างความลับ ความถูกต้องครบถ้วน และความพร้อมใช้งานได้ด้วย
- ผสานการควบคุมการเข้าถึงแบบ capability, การวิเคราะห์ WCET, การรองรับระบบ real-time แบบ mixed-criticality และความสามารถของไฮเปอร์ไวเซอร์ เพื่อจัดการทั้งการแยกส่วนอย่างละเอียดและความเป็น real-time
- API ของ seL4 อยู่ในระดับต่ำมาก จึงสร้างระบบซับซ้อนโดยตรงได้ยาก และแนวทางที่เป็นจริงคือใช้เฟรมเวิร์กอย่าง Microkit เมื่อสถาปัตยกรรมแบบคงที่เหมาะกับงาน
ขอบเขตที่ seL4 รับผิดชอบ
- seL4 คือไมโครเคอร์เนล ซึ่งเป็นแกนหลักระดับต่ำของระบบปฏิบัติการ
- OS ควบคุมฮาร์ดแวร์และทรัพยากรใน kernel mode ซึ่งเป็นโหมดการทำงานที่มีสิทธิ์สูงกว่าของโปรเซสเซอร์
- แอปพลิเคชันทำงานใน user mode และเข้าถึงฮาร์ดแวร์ได้เฉพาะตามวิธีที่ OS อนุญาตเท่านั้น
- ไมโครเคอร์เนลคือแกนหลักของ OS ที่ลดโค้ดซึ่งทำงานด้วยสิทธิ์สูงให้เหลือน้อยที่สุด
- seL4 อยู่ใน ตระกูลไมโครเคอร์เนล L4 ซึ่งย้อนกลับไปได้ถึงช่วงกลางทศวรรษ 1990
- seL4 ไม่เกี่ยวข้องกับ seLinux
- seL4 ไม่ใช่ OS ที่สมบูรณ์ แต่เป็นเคอร์เนลระดับต่ำที่ทำหน้าที่มัลติเพล็กซ์และแยกทรัพยากรฮาร์ดแวร์อย่างปลอดภัย
- บริการ OS ทั่วไป เช่น ระบบไฟล์, network stack, และไดรเวอร์อุปกรณ์ ไม่ได้อยู่ภายในเคอร์เนล
- บริการเหล่านี้ต้องถูกจัดให้เป็นโปรแกรมใน user mode
โครงสร้างไมโครเคอร์เนลและการลดพื้นผิวการโจมตี
- เคอร์เนลแบบ monolithic อย่าง Linux ให้บริการ OS เช่น การจัดเก็บไฟล์และเครือข่ายผ่านโค้ดใน kernel mode
- โค้ดใน kernel mode เข้าถึงทรัพยากรระบบได้อย่างไม่จำกัด ดังนั้นหากบั๊กนำไปสู่การยกระดับสิทธิ์หรือการรันโค้ดตามอำเภอใจ ระบบทั้งหมดอาจเสียหายได้
- เคอร์เนล Linux มีขนาดประมาณ 20 MSLOC และคาดว่าอาจมีบั๊กหลายหมื่นรายการ
- ไมโครเคอร์เนลที่ออกแบบดีอย่าง seL4 ลดโค้ดใน kernel mode ลงเหลือระดับประมาณ 10 kSLOC
- ซึ่งเล็กกว่าเคอร์เนล Linux ถึงระดับหลายร้อยเท่า
- เมื่อ TCB ลดลง พื้นผิวการโจมตีก็ลดลงตามไปด้วย
- บริการ OS ส่วนใหญ่ถูกย้ายออกนอกเคอร์เนล และไมโครเคอร์เนลทำงานเหมือน wrapper บาง ๆ รอบฮาร์ดแวร์
- ฟังก์ชันหลักที่ให้คือ การแยกส่วน ระหว่างโปรแกรม และกลไกการเรียกใช้อย่างปลอดภัย
- บริการต่าง ๆ กลายเป็นโปรแกรมใน user mode ที่ทำงานใน sandbox แยกต่างหาก ไม่ใช่อยู่ในเคอร์เนล
- งานวิจัยที่วิเคราะห์กรณีการเจาะระบบ Linux ที่เป็นที่รู้จักและร้ายแรงพบว่า การออกแบบแบบไมโครเคอร์เนลสามารถกำจัดกรณี 29% ได้ทั้งหมด และบรรเทาอีก 55% จนไม่ถูกจัดว่าเป็นกรณีร้ายแรงอีกต่อไป
PPC, capability และการควบคุมสิทธิ์อย่างละเอียด
- seL4 มีกลไก protected procedure call (PPC)
- ด้วยเหตุผลทางประวัติศาสตร์ยังคงมีคำว่า IPC อยู่ แต่คำว่า IPC อาจทำให้เข้าใจผิดและนำไปสู่การออกแบบที่ไม่ดีได้
- PPC ช่วยให้โปรแกรมหนึ่งเรียกฟังก์ชันของโปรแกรมที่อยู่ใน sandbox อื่นได้อย่างปลอดภัย
- ไมโครเคอร์เนลส่งผ่านอินพุตและเอาต์พุตในการทำ PPC และบังคับใช้ interface
- ฟังก์ชันระยะไกลถูกเรียกได้เฉพาะผ่าน entry point ที่ export ไว้เท่านั้น
- เรียกได้เฉพาะ client ที่ได้รับอนุญาตอย่างชัดเจนและมี capability ที่เหมาะสมเท่านั้น
- capability คือโทเค็นการเข้าถึงที่ทำให้เข้าถึงทรัพยากรเฉพาะของระบบได้
- ควบคุมได้อย่างละเอียดมากว่า entity ใดเข้าถึงทรัพยากรใดได้
- รองรับหลักการสิทธิ์ขั้นต่ำ หรือหลักการ least authority (POLA)
- วิธีควบคุมการเข้าถึงของระบบกระแสหลักอย่าง Linux หรือ Windows ไม่สามารถทำให้ได้ระดับสิทธิ์ขั้นต่ำแบบนี้ได้
- seL4 ถูกประเมินว่าเป็น OS หนึ่งเดียวของโลกที่ทั้งใช้ capability-based และผ่านการตรวจสอบแบบเป็นทางการ ซึ่งการผสานกันนี้ทำให้มีข้ออ้างที่ปกป้องได้ว่าเป็น OS ที่ปลอดภัยที่สุดในโลก
การตรวจสอบแบบเป็นทางการและการรับประกันความปลอดภัย
- seL4 ให้ หลักฐานพิสูจน์ที่เป็นทางการ ทางคณิตศาสตร์ และตรวจสอบด้วยเครื่อง เกี่ยวกับความถูกต้องของการทำงานตามการออกแบบ
- หลักฐานนี้หมายถึงว่าเคอร์เนล “ไม่มีบั๊ก” ในความหมายที่เข้มงวดมากเมื่อเทียบกับสเปก
- seL4 เป็นเคอร์เนล OS ตัวแรกของโลกที่มีหลักฐานพิสูจน์เช่นนี้ในระดับโค้ด
- นอกเหนือจากความถูกต้องของการทำงานตามการออกแบบแล้ว seL4 ยังมีหลักฐานเพิ่มเติมเกี่ยวกับการบังคับใช้นโยบายความปลอดภัย
- ในระบบที่ใช้ seL4 และกำหนดค่าอย่างถูกต้อง เคอร์เนลรับประกัน ความลับ, ความถูกต้องครบถ้วน และความพร้อมใช้งาน
- ห่วงโซ่การตรวจสอบเป็นจุดแตกต่างสำคัญของ seL4
- ในระบบที่สำคัญต่อความมั่นคงปลอดภัยและความปลอดภัย หากเคอร์เนลจะเป็นฐานความเชื่อถือได้ จำเป็นต้องมีการรับประกันที่แข็งแรงทั้งต่อการทำงานตามการออกแบบและคุณสมบัติด้านความปลอดภัย
ความเป็น real-time และระบบ mixed-criticality
- seL4 เป็นเคอร์เนล OS ที่ผ่านการวิเคราะห์ worst-case execution time (WCET) อย่างครบถ้วนและถูกต้อง
- หากกำหนดค่าเคอร์เนลอย่างเหมาะสม การทำงานของเคอร์เนลทั้งหมดจะมีขอบเขตด้านเวลา
- และรู้ค่าขอบเขตนั้นด้วย
- คุณสมบัตินี้เป็นเงื่อนไขตั้งต้นของการสร้าง ระบบ hard real-time
- มุ่งเป้าไปที่ระบบที่อาจเกิดผลร้ายแรงหากไม่สามารถตอบสนองต่อเหตุการณ์ภายในเวลาที่จำกัดอย่างเข้มงวด
- seL4 ยังรองรับระบบ real-time แบบ mixed-criticality (MCS)
- มุ่งเป้าไปที่สภาพแวดล้อมที่ต้องรับประกันเวลาให้กิจกรรมสำคัญ แม้โค้ดที่มีความน่าเชื่อถือต่ำกว่าจะทำงานร่วมกันบนแพลตฟอร์มเดียวกัน
- ต่างจากการแบ่งพาร์ทิชันเวลาและพื้นที่แบบเข้มงวดและไม่ยืดหยุ่นที่ OS แบบ MCS เดิมใช้ seL4 ให้โมเดลที่ยืดหยุ่นซึ่งยังคงการใช้ทรัพยากรไว้ได้
การใช้ seL4 เป็นไฮเปอร์ไวเซอร์
- seL4 เป็นทั้งไมโครเคอร์เนลและ ไฮเปอร์ไวเซอร์
- สามารถรัน virtual machine บน seL4 ได้
- ภายใน virtual machine สามารถรัน guest OS ทั่วไปอย่าง Linux ได้
- guest และแอปพลิเคชันสามารถสื่อสารกันได้ตามช่องทางการสื่อสารที่ seL4 บังคับใช้
- และสามารถสื่อสารกับแอปพลิเคชัน native ได้ด้วย
- สามารถใช้ Linux VM เป็นวิธีจัดหาบริการระบบได้
- ในตัวอย่างการกำหนดค่า จะยืมบริการอย่างเครือข่ายและสตอเรจจาก Linux หลาย instance ที่รันอยู่ใน VM แยกกัน
วิธีสร้างระบบบน seL4
- API ของ seL4 อยู่ในระดับต่ำมาก แม้เทียบกับไมโครเคอร์เนลอื่น ๆ
- ให้เฉพาะ abstraction ขั้นต่ำที่จำเป็นต่อการจัดการฮาร์ดแวร์อย่างปลอดภัย
- seL4 ถูกเปรียบว่าเป็น “ภาษาแอสเซมบลีของระบบปฏิบัติการ”
- การสร้างระบบซับซ้อนบน seL4 โดยตรงไม่ใช่วิธีที่เหมาะสม
- เฟรมเวิร์กระดับสูงกว่าควรช่วยให้โฟกัสกับโค้ดที่ implement บริการ และทำให้ความซับซ้อนของฮาร์ดแวร์กับการผสานระบบเป็นอัตโนมัติ
- seL4 มีเฟรมเวิร์กคอมโพเนนต์โอเพนซอร์สหลัก 3 ตัว
- Microkit: ทำให้ API ของ seL4 ง่ายขึ้นด้วย abstraction จำนวนน้อยที่เน้น protection domain และมี SDK สำหรับรวมโมดูลที่คอมไพล์แยกกันกับไบนารีของเคอร์เนลเพื่อสร้างอิมเมจที่บูตได้
- CAmkES: เป็นรุ่นก่อนหน้าของ Microkit และเป็นเฟรมเวิร์กคอมโพเนนต์สำหรับระบบสถาปัตยกรรมแบบคงที่ แต่ไม่มี SDK ทำให้กระบวนการ build ไม่สะดวกกว่าและมี overhead สูง
- Genode: รองรับไมโครเคอร์เนลหลายตัว มีบริการและไดรเวอร์สำหรับแพลตฟอร์ม x86 มากมาย และไม่บังคับใช้สถาปัตยกรรมแบบคงที่ แต่ไม่สามารถใช้ฟีเจอร์ด้านความมั่นคงปลอดภัยและความปลอดภัยทั้งหมดของ seL4 ได้ และไม่มีเรื่องราวการรับประกัน
- ตราบใดที่สถาปัตยกรรมระบบแบบคงที่ตรงกับข้อกำหนด แนะนำให้ใช้ Microkit สำหรับการสร้างระบบบน seL4
- สถาปัตยกรรมแบบคงที่คือโมเดลที่กำหนดชุดโมดูลและโครงสร้างการสื่อสาร ณ เวลาตั้งค่าระบบ
- มองว่าโมเดลนี้ตรงกับความต้องการของระบบฝังตัวส่วนใหญ่ รวมถึงระบบไซเบอร์-กายภาพที่ซับซ้อนอย่างรถยนต์และอากาศยาน
1 ความคิดเห็น
ความคิดเห็นบน Hacker News
ตัว seL4 เองเป็นเรื่องเก่าแล้ว แต่สงสัยว่ามี เลเยอร์หรือคอมโพเนนต์ที่ผ่านการตรวจสอบแบบเป็นทางการ ใหม่ ๆ เพิ่มเข้ามานอกเหนือจากไมโครเคอร์เนลหรือไม่
อีกอย่าง พอเห็นคำว่า “พิสูจน์” ก็ดูเหมือนมีบางคนที่เกิดภาวะอารมณ์ล้นจนความคิดหยุดชะงักไป การตรวจสอบแบบเป็นทางการไม่ใช่ยาครอบจักรวาลที่จะมาแก้ปัญหาอันไร้ขอบเขตของ IT ที่ปลอดภัย และไม่ใช่วิธีสร้างซอฟต์แวร์ที่สมบูรณ์แบบไร้ที่ติ
เท่าที่เข้าใจคือเป็นการพิสูจน์ว่าภายใต้เงื่อนไขบางอย่าง จะเป็นไปตามข้อกำหนดบางข้อ และข้อกำหนดกับเงื่อนไขเหล่านั้นอาจค่อนข้างแคบ อีกทั้งไม่ได้กล่าวอะไรเลยเกี่ยวกับฟังก์ชันและเงื่อนไขที่อยู่นอกสเปก อยากรู้ว่าประมาณนี้ถูกไหม
ในทางปฏิบัติ ผู้เชี่ยวชาญด้านความปลอดภัยคาดหวังอะไรเมื่อเห็น “ซอฟต์แวร์ที่ผ่านการตรวจสอบแบบเป็นทางการ” ก็อยากรู้เหมือนกัน ผมคิดว่าข้อมูลสำคัญตรงนี้น่าจะเป็นว่า seL4 เป็นไปตามสเปกอะไร
https://github.com/seL4/seL4/pull/243
https://github.com/seL4/l4v/pull/453
ใน issue tracker ก็มีบั๊กเกี่ยวกับหน่วยความจำอยู่หลายรายการ
https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
ที่น่าสนใจคือ PR ที่แก้ “register clobbering” ของหน่วยความจำไม่ได้ติดป้าย bug ดังนั้นถ้ากรองด้วย “bug” จะไม่เจอ เมื่อก่อนเคยคิดว่าเพราะมีการพิสูจน์ seL4 จึงมีภูมิคุ้มกันต่อปัญหาแบบนี้ แต่หลังจากเห็นกรณีนี้แล้วก็เริ่มมองว่าการพิสูจน์ไม่ได้ครอบคลุมกว้างเท่าที่ชุมชนเชื่อกัน ถึงอย่างนั้น seL4 ก็ยังเป็นซอฟต์แวร์ที่น่าประทับใจมาก
ตอบคำถามก็คือ สเปกที่ seL4 เป็นไปตามนั้นเผยแพร่อยู่บน GitHub
https://github.com/seL4/l4v
mixed-criticality scheduling ให้การเข้าถึงเวลา CPU แบบอิง capability, การจำกัดเพดานการรันของเธรด, การรับประกันลำดับความสำคัญและการเข้าถึงทรัพยากรของงานที่มีความสำคัญสูง และ “passive servers” ที่ทำงานด้วยเวลาการจัดตารางที่ผู้เรียกบริจาคให้
Microkit เป็นเลเยอร์นามธรรมที่ตรวจสอบแล้ว ซึ่งทำให้สร้างระบบจริงบน seL4 ได้ง่ายขึ้นมาก ส่วน Device Driver Framework คือเทมเพลตไดรเวอร์อุปกรณ์สำหรับ I/O ประสิทธิภาพสูงบน seL4, การทำ control/data plane, และเครื่องมือสำหรับเขียนไดรเวอร์กับทำ device virtualization
การตรวจสอบแบบเป็นทางการสามารถรับประกันได้ว่าภายใต้เงื่อนไขบางอย่าง ข้อกำหนดบางข้อเป็นจริง โดยทั่วไปก็ถูกที่ข้อกำหนดและเงื่อนไขแบบนั้นอาจแคบได้ แต่ในตัว seL4 เองมีการพิสูจน์จำนวนมากที่ครอบคลุมคุณสมบัติในขอบเขตกว้างซึ่งเราคาดหวังจากเคอร์เนล และการรับประกันเหล่านั้นยังคงใช้ได้แม้อยู่ภายใต้สมมติฐานที่อ่อนมาก ๆ ไม่ต้องสมมติด้วยซ้ำว่า C compiler ถูกต้อง เพราะมีเครื่องมือแยกต่างหากที่ดูผลลัพธ์จากคอมไพเลอร์แล้วพิสูจน์ว่าไบนารีที่คอมไพล์มาทำงานสอดคล้องกับ semantics ของ C ที่ต้องการ
ข้อกำหนดที่ seL4 เป็นไปตามนั้นรวมถึงการที่โค้ดไบนารีของเคอร์เนล seL4 ทำงานตามพฤติกรรมที่ระบุไว้ในสเปกนามธรรมอย่างถูกต้องพอดี และไม่ทำเกินกว่านั้น ไม่มี buffer overflow, memory leak, pointer error, null pointer dereference, undefined behavior ในโค้ด C, หรือการยุติเคอร์เนลด้วยวิธีอื่นนอกเหนือจากวิธีที่ระบุไว้อย่างชัดเจนในสเปก
สเปกและไบนารีของ seL4 ยังเป็นไปตามคุณสมบัติด้านความปลอดภัยเรื่อง integrity และ confidentiality ด้วย integrity หมายถึงโปรเซสไม่มีทางเปลี่ยนข้อมูลที่ไม่ได้รับสิทธิ์อย่างชัดเจนได้เลย ส่วน confidentiality หมายถึงไม่สามารถอ่านข้อมูลที่ไม่มีสิทธิ์ได้ไม่ว่าด้วยวิธีใด ยังแสดงให้เห็นด้วยว่าไม่สามารถอนุมานข้อมูลทางอ้อมผ่านช่องทางข้างเคียงบางชนิดได้ นอกเหนือจากความปลอดภัยแล้ว ยังเป็นไปตามการรับประกันเวลาเรียกใช้กรณีเลวร้ายที่สุดที่คาดไว้และคุณสมบัติด้าน scheduling ด้วย
งานปัจจุบันมุ่งไปทาง LionsOS ซึ่งตั้งใจให้มีการนำไปใช้ในวงกว้างขึ้น: https://lionsos.org/
https://docs.sel4.systems/projects/sel4/frequently-asked-que...
ใช้ type-level programming เยอะมากเพื่อติดตามทรัพยากร การเข้าถึงฮาร์ดแวร์ และ capability ตั้งแต่ตอนคอมไพล์ เพราะการไปเจอปัญหาแล้วดีบักตอน runtime นั้นเลวร้ายเกินไป จึงเป็นความพยายามที่จะยกการรับประกันบางส่วนของเคอร์เนลพื้นฐานขึ้นไปฝั่งคอมไพเลอร์
ผมชอบ ไมโครเคอร์เนลโฮสต์ ที่รัน guest monolithic kernel ดังนั้นเซิร์ฟเวอร์ของผมจึงรัน seL4 เป็นชั้นความปลอดภัยและแบ็กอัปให้ FreeBSD VM และข้างในนั้นใช้ jail สำหรับ renderfarm, คลัสเตอร์ BEAM และ Jenkins
สิ่งที่น่าเสียดายคือไม่มีพอร์ต ARM สำหรับ threading และ in-process kernel ของ DragonflyBSD หรือก็คือการออกแบบแบบไฮบริดเคอร์เนล ความฝันคือการรัน OpenMoonRay บน Ampere Altra 128 คอร์ให้มีประสิทธิภาพยิ่งขึ้น
ตอนนี้ดูเหมือนว่า การถกเถียงสนับสนุน/คัดค้านไมโครเคอร์เนล เองแทบไม่มีความหมายมากนักแล้ว วิธีเดียวที่จะเข้าถึงบริการที่มีสิทธิ์ได้อย่างรวดเร็ว มีประสิทธิภาพ และปลอดภัยคือมาตรการบรรเทาในฮาร์ดแวร์ ส่วนสิ่งที่ซอฟต์แวร์ทำได้มีขีดจำกัด
คล้ายกับความแตกต่างระหว่าง 80286 กับ 80386 ตัวหลังเพิ่มการรองรับระดับฮาร์ดแวร์สำหรับมัลติทาสกิงจริง ๆ ซึ่งตัวแรกไม่มี หลังจากนั้น กลไกการป้องกันระดับฮาร์ดแวร์ที่ทำให้ไฮเปอร์ไวเซอร์เป็นไปได้ก็เพิ่มขึ้นเรื่อย ๆ
โดยเฉพาะ Apple ใส่ความสามารถจำนวนมากลงใน SoC เพื่อปกป้องเคอร์เนล ไดรเวอร์ และองค์ประกอบต่าง ๆ ในระดับชิป และบังคับใช้สิทธิ์เมื่อใช้เธรดที่กำลังรันและพอยน์เตอร์ https://support.apple.com/guide/security/operating-system-in...
นั่นไม่ได้หมายความว่า OS จะเจาะไม่ได้ แต่มีประสิทธิภาพกว่ายุทธศาสตร์ที่จัดการสิทธิ์ด้วยซอฟต์แวร์เพียงอย่างเดียวมาก หากใช้ความสามารถเหล่านี้หรือสิ่งที่คล้ายกัน โครงสร้างเคอร์เนลก็ดูเหมือนไม่ได้สำคัญมากอีกต่อไป เลยสงสัยว่าผมเข้าใจผิดหรือเปล่า
ยังมีสิ่งให้เรียนรู้อีกมากจากระบบไมโคร/ไฮบริดที่ประกอบร่วมกันได้มากขึ้น ตัวอย่างเช่น Plan 9 เป็นระบบไฮบริดที่ยอดเยี่ยม ซึ่งเปิดเผยอ็อบเจ็กต์ทั้งหมดของระบบให้กับ user space ผ่านโปรโตคอลเดียวคือ 9P ที่ว่าเป็นไฮบริดเพราะบางส่วนอย่าง IP หรือ TLS อยู่ในเคอร์เนลเพื่อหลีกเลี่ยงโอเวอร์เฮดของ system call
อีกการออกแบบที่น่าสนใจคือ ไดรเวอร์ภายในเคอร์เนลส่วนใหญ่เป็นเพียงรูปแบบขั้นต่ำที่ทำหน้าที่เป็นอินเทอร์เฟซ 9P ให้กับลอจิกของฮาร์ดแวร์ วิธีนี้เปลี่ยนอ็อบเจ็กต์ของเครื่องอย่างพอยน์เตอร์หรือเรคคอร์ดให้เป็นไฟล์ที่เรียกดูได้ ปกป้องไฟล์เหล่านั้นด้วยสิทธิ์มาตรฐานของ Unix และกระจายองค์ประกอบไปยังหลายเครื่องผ่านเครือข่ายได้ง่าย ผลคือสามารถผลักลอจิกของไดรเวอร์ออกไปเป็นโปรแกรม user space ได้อย่างปลอดภัย
9P โปร่งใสต่อเครือข่ายและสถาปัตยกรรม จึงทำงานร่วมกันได้ทันทีบนเครื่องหลากหลายอย่าง Arm, x86, mips เป็นต้น พอกลับจาก Plan 9 ไปใช้ Linux/Unix หรือ Windows ก็รู้สึกเศร้าและอึดอัด ความยืดหยุ่นแทบจะแข็งระดับหินอัคนี และฟังก์ชันต่าง ๆ ถูกต่อเติมแบบเข้ากันไม่ได้ด้วยโปรโตคอลจำนวนมากที่ทำสิ่งเดียวกันคือการให้บริการไฟล์/อ็อบเจ็กต์
จากมุมมองวิศวกรรมเชิงปฏิบัติ เคอร์เนลแบบโมโนลิธิกเร็วกว่า ง่ายกว่า และมีทรัพยากรมากกว่า ส่วนความปลอดภัยก็อยู่ในระดับที่ C ทำได้ คือพยายามเต็มที่พร้อมบั๊กจำนวนมาก มีฮาร์ดแวร์จำนวนมากถูกนำมาใช้เพื่อบรรเทาความยุ่งเหยิงนั้น แต่ถ้าเป็น SeL4 ในทางทฤษฎีอาจไม่จำเป็นต้องมี security coprocessor เพราะมีความเชื่อมั่นสูงมากต่อการแยกกันระหว่างโปรเซสและการไม่มีเอ็กซ์พลอยต์ระดับ root ดังนั้นการออกแบบฮาร์ดแวร์/ซอฟต์แวร์ร่วมกันจึงสำคัญ
อย่างไรก็ตาม ทีม SeL4 ก็ต้องใช้ทรัพยากรวิศวกรรมจำนวนมากในการกำจัด side channel ของฮาร์ดแวร์ เพราะโลกจริงไม่ได้สนใจการจำลองทางฟิสิกส์ ฮาร์ดแวร์จึงมีข้อบกพร่องเช่นกัน
ข้อดีของไมโครเคอร์เนลตรงนี้คือมันเล็กพอให้ formal verification จัดการได้ ตัว proof เองมีขนาด 10 เท่าของเคอร์เนล การสลับบริบทของ SeL4 เร็วกว่า Linux ในระดับหนึ่งหลักของจำนวนเท่า ดังนั้นผลกระทบด้านประสิทธิภาพควรเล็กจนมองข้ามได้ แต่ถ้าสามารถตรวจพิสูจน์เคอร์เนลโมโนลิธิกหลายล้านบรรทัดได้ราวกับมีเวทมนตร์ ฝั่งที่ไม่ต้องสลับบริบทย่อมยังเร็วกว่าอยู่ดี จริง ๆ แล้วทีม SeL4 เคยพยายามย้าย scheduler ไปไว้ใน user space แต่ต้นทุนด้านประสิทธิภาพสูงเกินไป จึงปล่อยให้อยู่ในเคอร์เนลและเพิ่มภาระการพิสูจน์เข้าไป
ตรงกันข้าม บทบาทหลักของฮาร์ดแวร์คือเพิ่มประสิทธิภาพ ตัวอย่างเช่น ไมโครเคอร์เนลสมัยนี้ค่อนข้างแข็งแรงอยู่แล้ว เพราะใช้ฮาร์ดแวร์อย่าง MMU ได้ดี จากนั้นฐานการประมวลผลที่เชื่อถือได้ขนาดเล็กของไมโครเคอร์เนลก็ให้ความน่าเชื่อถือแก่เคอร์เนล และเคอร์เนลกับฮาร์ดแวร์ร่วมกันสร้างรากฐานที่แข็งแกร่ง
สุดท้ายเป็นเรื่องว่าจะยอมให้ฮาร์ดแวร์ “โกง” ได้ถึงระดับไหน แต่โดยรวมแล้วไมโครเคอร์เนลใช้ประโยชน์จากฟีเจอร์ป้องกันได้ดีกว่า หรือจะดูเอ็กโซเคอร์เนลก็ได้
https://genode.org/index
เป็นระบบปฏิบัติการที่มี การรองรับ seL4
เคย นำเสนอเรื่อง SeL4 ที่แชปเตอร์ OWASP ในพื้นที่อยู่ครั้งหนึ่ง ไม่แน่ใจว่าจะยังหาสไลด์/เอกสารได้ไหม
โปรเจกต์นี้เป็นสิ่งที่ทำออกมาได้ดีมากจริง ๆ แต่โดยเฉพาะในงานคอมพิวติ้งทั่วไป ผมยังลังเลที่จะมองว่าเป็นตัวแทน Linux อย่างไรก็ตาม นั่นไม่ได้หมายความว่าไมโครเคอร์เนลโดยรวมไม่เหมาะกับงานทั่วไป RedoxOS ช่วงหลังดูเหมือนจะมีความคืบหน้าอยู่บ้าง และใช้ไมโครเคอร์เนลที่เขียนด้วย Rust
ถึงอย่างนั้น หาก Redox ประสบความสำเร็จ แค่นั้นก็ถือเป็นความก้าวหน้าที่ดีแล้ว seL4 มีลักษณะเช่นนี้ในแบบที่สุดโต่งยิ่งกว่า ข้อดีทางเทคนิคนั้นยอดเยี่ยม แต่จนถึงตอนนี้และอาจรวมถึงต่อจากนี้ ก็คงยังไม่มีอะไรที่จะทำให้มันกลายเป็น ‘กระแสหลักถัดไป’ ได้ หากตัดปัจจัยทางการเมืองออกไป ผมคิดว่าไมโครเคอร์เนลจะประสบความสำเร็จ และก็ควรเป็นเช่นนั้น
เพื่อให้ seL4 มีประโยชน์จริง ยังต้องมีสิ่งต่าง ๆ อีกมากที่อยู่บนมัน โชคดีที่ในส่วนนั้นก็มีงานโอเพนซอร์สคืบหน้าไปมาก และอยู่ในจุดที่ดีกว่าเมื่อไม่กี่ปีก่อนมาก
สำหรับสถานการณ์แบบคงที่มี LionsOS[0] และตอนนี้ก็ใช้งานได้ค่อนข้างดีแล้ว
สำหรับสถานการณ์แบบไดนามิกมี Provably Secure, General-Purpose Operating System[1] ซึ่งยังอยู่ในช่วงเริ่มต้น
ทั้งสองอย่างหาได้จากหน้า Projects[2] ของ trustworthy systems ที่ลิงก์อยู่บนเว็บไซต์ seL4
[0] https://trustworthy.systems/projects/LionsOS/
[1] https://trustworthy.systems/projects/smos/
[2] https://trustworthy.systems/projects/
สงสัยว่า OS ที่รันอยู่บนเคอร์เนลนี้ก็ต้องผ่าน การตรวจพิสูจน์เชิงรูปแบบ ด้วยหรือไม่ เพื่อให้การรับประกันด้านความปลอดภัยยังใช้ได้
แน่นอนว่าเคอร์เนลอย่างเดียวไม่ได้มีประโยชน์มากนัก ดังนั้นการออกแบบไดรเวอร์ เซิร์ฟเวอร์ระบบไฟล์ และบริการอื่น ๆ ที่รันอยู่บนเคอร์เนลยังคงสำคัญอยู่
อีกจุดที่สำคัญคือ ระบบอื่นส่วนใหญ่รวมถึง Linux มีข้อบกพร่องในระดับพื้นฐาน แต่ seL4 ช่วยให้สร้าง ระบบที่ปลอดภัยและเชื่อถือได้ ได้จริง
ด้วยเหตุนี้จึงสามารถรันเคอร์เนล Linux ข้าง ๆ โปรเซสที่ต้องการความปลอดภัยสูงได้ และยังมีการรับประกันว่าทั้งสองถูกแยกออกจากกัน ยกเว้น IPC ที่ได้รับอนุญาต
แต่มีข้อจำกัดอยู่ ต้องปิด DMA และไดรเวอร์ก็ต้องใช้เฉพาะตัวที่ผ่านการตรวจพิสูจน์เชิงรูปแบบแล้วเท่านั้น
อีกจุดสำคัญคือ เคอร์เนลแบบมัลติคอร์ ของ seL4 ยังไม่ได้รับการตรวจพิสูจน์
Helios Microkernel ของ Drew DeVault ก็น่าสนใจเช่นกัน ว่ากันว่าสร้างบนพื้นฐานของ SeL4
https://ares-os.org/docs/helios/
ที่มหาวิทยาลัย Karlsruhe นั้น L4 เคยได้รับความนิยม ผมไม่เคยลงไปดูรายละเอียดจริงจัง แต่ดูเหมือนเป็นโปรเจ็กต์ที่สนใจการทดสอบแนวคิดเชิงทฤษฎีเป็นหลัก มากกว่าการสร้างสิ่งที่มีประโยชน์ในทางปฏิบัติ
นั่นเป็นเรื่องเมื่อ 20 ปีก่อน และในสายตาผมตอนนี้ก็ยังไม่ได้เปลี่ยนไปมากนัก ลองค้นเร็ว ๆ ดูเหมือนว่ามีความพยายามสร้าง OS บนมันอยู่บ้าง แต่ก็ดูใกล้เคียงกับการพิสูจน์แนวคิดมากกว่าการใช้งานจริง
“ยอดจัดส่ง OKL4 เกิน 1.5 พันล้านชุดเมื่อต้นปี 2012 โดยส่วนใหญ่เป็นชิปโมเด็มไร้สายของ Qualcomm จุดติดตั้งอื่น ๆ รวมถึงระบบอินโฟเทนเมนต์ในรถยนต์”
“โปรเซสเซอร์ตระกูล Apple A ตั้งแต่ A7 เป็นต้นไปมีโคโปรเซสเซอร์ Secure Enclave ที่รันระบบปฏิบัติการ L4 อยู่ โดย OS นี้คือ sepOS ซึ่งอิงจากเคอร์เนล L4-embedded ที่พัฒนาโดย NICTA ในปี 2006 ส่งผลให้ L4 ถูกใส่อยู่ในอุปกรณ์ Apple สมัยใหม่ทั้งหมด รวมถึง Mac ที่ใช้ Apple silicon”
Rittinghaus ซึ่งเป็นศิษย์เก่าของ Bellosa มีส่วนเกี่ยวข้องกับ Unikraft[0] ที่เคยถูกพูดถึงใน HN อยู่หลายครั้ง และใช้เทคโนโลยี unikernel
[0] https://unikraft.org/
“Secure Enclave Processor รัน L4 microkernel เวอร์ชันที่ Apple ปรับแต่งเอง”
https://support.apple.com/de-at/guide/security/sec59b0b31ff/...
https://www.kernkonzept.com/kk_events/elektrobit-advances-au...
เท่าที่ผมดู เคอร์เนล L4Re ก็น่าจะเป็นส่วนหนึ่งของ Elektrobit Safe Linux ด้วย
ผมทำ OS ที่อิงกับ Pistachio เป็นวิทยานิพนธ์จบการศึกษา ผมคิดเสมอว่าถ้าได้เรียนที่ Karlsruhe ก็คงไปสายวิจัย OS แน่ ๆ
ผมเองก็เคยมีไอเดียด้านการออกแบบระบบปฏิบัติการ และ capability ที่พิจารณาไว้นั้นใช้ความสามารถในการแทรกกลางและมอบหมายสิทธิ์แบบเดียวกับ seL4 นอกจากสิ่งที่เขียนไว้ตรงนั้นแล้วยังมีข้อดีอื่นด้วย เช่น สามารถใช้ proxy capability เพื่อใส่ฟิลเตอร์กับเสียง หรือทำให้เครือข่ายโปร่งใสได้
ผมคิดว่าความสามารถแบบ real-time อาจอนุญาตให้เป็นการใช้งานแบบเลือกได้ ไอเดียของผมใกล้กับสเปกมากกว่าการ implement เพียงแบบเดียว
อีกฟีเจอร์ที่อยากได้คือให้ทุกโปรแกรม ทำงานแบบกำหนดผลได้แน่นอน ยกเว้นอินพุต/เอาต์พุต หากไม่มีอินพุต/เอาต์พุต ก็จะรู้วันที่/เวลา หรือเวลารันของโปรแกรมไม่ได้ และตรวจสอบความสามารถของโปรเซสเซอร์ไม่ได้ด้วย หากใช้ฟีเจอร์ที่ฮาร์ดแวร์ไม่รองรับ ระบบปฏิบัติการก็อาจ emulate ให้ได้
เพื่อ implement สิ่งนี้ ผมคิดว่าจะใช้ทั้งการสนับสนุนจากฮาร์ดแวร์และซอฟต์แวร์ผสมกัน ในเอกสารมีบันทึกเรื่องการโจมตี capability ที่ implement ด้วยฮาร์ดแวร์ แต่ผมไม่มีเอกสารอ้างอิง จึงไม่รู้ว่าการโจมตีนั้นใช้ได้กับวิธีที่ผมคิดไว้ด้วยหรือไม่
ในมุมมองด้านความปลอดภัย ดูเหมือนจะมีความล้มเหลวแบบเดียวกับ KVM ในเคอร์เนล Linux ถ้าไฮเปอร์ไวเซอร์อยู่ใน ring 0 ก็มีความเสี่ยงที่จะหลุดจาก VM หนึ่งไปยัง VM อื่นหรือไปยังโฮสต์เอง
ผมสงสัยว่าความเสี่ยงนั้นถูกบรรเทาอย่างไร
VMM ไม่มี capability มากกว่า VM เอง ดังนั้นหากไม่นับความหมายเชิงวิชาการแล้ว การหลุดออกจาก VM ก็ไม่มีคุณค่า
ดูหน้า 8–10 ของ PDF ต้นฉบับได้