🏜️ المقارنة المعمارية: Hisn-seL4 ضد MirageOS

🏜️

أنظمة عامة

البرنامج كنظام تشغيل (Unikernel): يحول برامجك مباشرة إلى أنظمة تشغيل مصغرة ومستقلة (Unikernels) للعمل على السحابة، متخلصاً من الحاجة لنظام وسيط مثل Linux.
أمان لغوي (OCaml): يعتمد بشكل شبه كلي على قوة نظام الأنواع (Type System) في لغة OCaml لمنع أخطاء الذاكرة والثغرات، ليعوض غياب العزل العتادي الداخلي.
احتكار لغوي صارم: لكي تستفيد من أمانه، أنت مجبر هندسياً على كتابة كل تطبيقاتك وتطويراتك حصرياً بلغة OCaml، مما يجعله بيئة مغلقة وصعبة التبني.
عزل يعتمد على الـ Hypervisor: رغم أمان اللغة، يظل البرنامج والنواة في فضاء واحد؛ وإذا حدث اختراق، فالعزل الوحيد المتبقي هو برنامج الاستضافة السحابية (Hypervisor).

🛡️

مثبت رياضياً

عزل عتادي لا يحتكر لغة: لا يجبرك Hisn-seL4 على لغة واحدة؛ فهو يوفر درعاً رياضياً (seL4) يعزل الحاويات عتادياً سواء كانت برامجها مكتوبة بـ C أو Rust أو غيرها.
أمان مزدوج (عتاد + رياضيات): أمان OCaml ممتاز، لكن Hisn-seL4 يدمج بين لغة آمنة (Rust) وبرهان رياضي (Isabelle/HOL) وحدود عتادية (MMU) في منظومة واحدة لا تُقهر.
عزل داخلي مستقل: بينما يحتاج MirageOS لـ Hypervisor سحابي خارجي ليعزله عن جيرانه، Hisn-seL4 هو طبقة العزل بحد ذاته، ويدير العزل داخلياً دون مساعدة.
للمكتب لا للسحابة فقط: MirageOS مخصص لبناء خدمات سحابية دقيقة (Microservices) — Hisn-seL4 موجه لبناء حاسوب شخصي آمن بالكامل ومتعدد المهام للمستخدم اليومي.

🏜️ المقارنة المعمارية: Hisn-seL4 ضد MirageOS ​