Inti separation dileupaskeun (kernel pamisahan) Muen, dikembangkeun ku pausahaan Swiss codelabs.
Muen ngan ukur ngadukung platform Intel x86_64 sareng mastikeun yén kernel OS sareng aplikasi anu dijalankeun dina éta henteu tiasa ngaksés sumber daya saluareun kuota anu dialokasikeun. Ieu lumaku, antara séjén, pikeun RAM, waktu CPU jeung aksés ka alat I / O.
Kernel Linux, program Ada/SPARK, sareng OS perpustakaan anu ditulis nganggo kerangka Solo5 (contona, MirageOS dina OCaml) dirojong salaku aplikasi tamu. Supir kernel disayogikeun pikeun Linux pikeun nyepetkeun aksés ka PCI sareng sumber host anu sanés.
Muen sorangan sagemblengna dilaksanakeun di SPARK, sawaréh aman tina basa Ada, sarta geus diverifikasi bébas tina kasalahan runtime. Kodeu disebarkeun dina lisénsi GPLv3.
sumber: linux.org.ru