Google ได้ประกาศการค้นพบการพัฒนาที่เกี่ยวข้องกับโครงการ KataOS โดยมีเป้าหมายเพื่อสร้างระบบปฏิบัติการที่ปลอดภัยสำหรับฮาร์ดแวร์ฝังตัว ส่วนประกอบของระบบ KataOS เขียนด้วยภาษา Rust และทำงานบนไมโครเคอร์เนล seL4 ซึ่งมีการพิสูจน์ความน่าเชื่อถือทางคณิตศาสตร์บนระบบ RISC-V ซึ่งบ่งชี้ว่าโค้ดเป็นไปตามข้อกำหนดที่ระบุในภาษาทางการอย่างสมบูรณ์ รหัสโครงการเปิดภายใต้ลิขสิทธิ์ Apache 2.0
ระบบให้การสนับสนุนแพลตฟอร์มที่ใช้สถาปัตยกรรม RISC-V และ ARM64 เพื่อจำลองการทำงานของ seL4 และสภาพแวดล้อม KataOS ที่ด้านบนของฮาร์ดแวร์ เฟรมเวิร์ก Renode จะถูกนำมาใช้ในระหว่างกระบวนการพัฒนา เพื่อเป็นการดำเนินการอ้างอิง มีการเสนอซอฟต์แวร์และฮาร์ดแวร์ Sparrow ที่ซับซ้อน โดยผสมผสาน KataOS เข้ากับชิปที่ปลอดภัยบนแพลตฟอร์ม OpenTitan โซลูชันที่นำเสนอช่วยให้คุณสามารถรวมเคอร์เนลระบบปฏิบัติการที่ได้รับการตรวจสอบตามตรรกะเข้ากับส่วนประกอบฮาร์ดแวร์ที่เชื่อถือได้ (RoT, Root of Trust) ซึ่งสร้างขึ้นโดยใช้แพลตฟอร์ม OpenTitan และสถาปัตยกรรม RISC-V นอกเหนือจากโค้ด KataOS แล้ว ยังมีแผนที่จะเปิดส่วนประกอบ Sparrow อื่นๆ ทั้งหมด รวมถึงส่วนประกอบฮาร์ดแวร์ในอนาคต
แพลตฟอร์มดังกล่าวกำลังได้รับการพัฒนาโดยคำนึงถึงการใช้งานในชิปพิเศษที่ออกแบบมาเพื่อใช้งานแอพพลิเคชั่นสำหรับการเรียนรู้ของเครื่องและการประมวลผลข้อมูลที่เป็นความลับ ซึ่งต้องการการป้องกันในระดับพิเศษและการยืนยันการขาดความล้มเหลว ตัวอย่างของแอปพลิเคชันดังกล่าว ได้แก่ ระบบที่จัดการภาพบุคคลและการบันทึกเสียง การใช้การตรวจสอบความน่าเชื่อถือของ KataOS ช่วยให้มั่นใจได้ว่าหากส่วนหนึ่งของระบบล้มเหลว ความล้มเหลวจะไม่แพร่กระจายไปยังส่วนที่เหลือของระบบ และโดยเฉพาะอย่างยิ่ง ไปยังเคอร์เนลและส่วนที่สำคัญ
สถาปัตยกรรม seL4 มีความโดดเด่นในเรื่องการเคลื่อนย้ายชิ้นส่วนสำหรับการจัดการทรัพยากรเคอร์เนลในพื้นที่ผู้ใช้ และการใช้เครื่องมือควบคุมการเข้าถึงแบบเดียวกันสำหรับทรัพยากรเช่นเดียวกับทรัพยากรผู้ใช้ ไมโครเคอร์เนลไม่ได้เตรียมนามธรรมระดับสูงไว้แล้วสำหรับจัดการไฟล์ กระบวนการ การเชื่อมต่อเครือข่าย และอื่นๆ แต่กลับให้กลไกเพียงเล็กน้อยเท่านั้นในการควบคุมการเข้าถึงพื้นที่ที่อยู่ทางกายภาพ การขัดจังหวะ และทรัพยากรตัวประมวลผล นามธรรมและไดรเวอร์ระดับสูงสำหรับการโต้ตอบกับฮาร์ดแวร์จะถูกนำไปใช้แยกกันบนไมโครเคอร์เนลในรูปแบบของงานระดับผู้ใช้ การเข้าถึงงานดังกล่าวไปยังทรัพยากรที่มีให้กับไมโครเคอร์เนลนั้นจัดขึ้นตามคำจำกัดความของกฎ
สำหรับการป้องกันเพิ่มเติม ส่วนประกอบทั้งหมดยกเว้นไมโครเคอร์เนลได้รับการพัฒนาโดยกำเนิดใน Rust โดยใช้เทคนิคการเขียนโปรแกรมที่ปลอดภัยซึ่งจะลดข้อผิดพลาดของหน่วยความจำที่นำไปสู่ปัญหาต่างๆ เช่น การเข้าถึงหน่วยความจำหลังจากปล่อยว่าง การยกเลิกการอ้างอิงตัวชี้ค่าว่าง และการโอเวอร์รันบัฟเฟอร์ ตัวโหลดแอปพลิเคชันในสภาพแวดล้อม seL4, บริการระบบ, เฟรมเวิร์กสำหรับการพัฒนาแอปพลิเคชัน, API สำหรับการเข้าถึงการเรียกของระบบ, ตัวจัดการกระบวนการ, กลไกสำหรับการจัดสรรหน่วยความจำแบบไดนามิก ฯลฯ ถูกเขียนด้วยภาษา Rust แอสเซมบลีที่ได้รับการตรวจสอบแล้วใช้ชุดเครื่องมือ CAmkES ซึ่งพัฒนาโดยโครงการ seL4 ส่วนประกอบสำหรับ CAmkES สามารถสร้างได้ใน Rust
Rust บังคับใช้ความปลอดภัยของหน่วยความจำ ณ เวลาคอมไพล์ผ่านการตรวจสอบการอ้างอิง ความเป็นเจ้าของอ็อบเจ็กต์ และการติดตามอายุการใช้งานของอ็อบเจ็กต์ (ขอบเขต) และโดยการประเมินความถูกต้องของการเข้าถึงหน่วยความจำ ณ รันไทม์ นอกจากนี้ Rust ยังให้การป้องกันจำนวนเต็มล้น โดยกำหนดให้ต้องกำหนดค่าตัวแปรก่อนใช้งาน ใช้แนวคิดของการอ้างอิงและตัวแปรที่ไม่เปลี่ยนรูปตามค่าเริ่มต้น และเสนอการพิมพ์แบบคงที่ที่แข็งแกร่งเพื่อลดข้อผิดพลาดเชิงตรรกะให้เหลือน้อยที่สุด
ที่มา: opennet.ru