{"id":101775,"date":"2021-10-25T22:22:37","date_gmt":"2021-10-25T20:22:37","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/vypusk-muen-1-0-otkrytogo-mikroyadra-dlya-sozdaniya-vysokonadyozhnyh-sistem"},"modified":"2021-10-25T22:22:37","modified_gmt":"2021-10-25T20:22:37","slug":"vypusk-muen-1-0-otkrytogo-mikroyadra-dlya-sozdaniya-vysokonadyozhnyh-sistem","status":"publish","type":"post","link":"https:\/\/prohoster.info\/cs\/blog\/news\/vypusk-muen-1-0-otkrytogo-mikroyadra-dlya-sozdaniya-vysokonadyozhnyh-sistem","title":{"rendered":"Vyd\u00e1n\u00ed Muen 1.0, otev\u0159en\u00e9ho mikroj\u00e1dra pro vytv\u00e1\u0159en\u00ed vysoce spolehliv\u00fdch syst\u00e9m\u016f","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Po osmi letech v\u00fdvoje byl uveden projekt Muen 1.0, kter\u00fd vyv\u00edj\u00ed j\u00e1dro odd\u011blen\u00ed (Separation kernel), jeho\u017e absence chyb v zdrojov\u00fdch textech byla potvrzena matematick\u00fdmi metodami form\u00e1ln\u00ed verifikace spolehlivosti. J\u00e1dro je dostupn\u00e9 pro architekturu x86_64 a m\u016f\u017ee b\u00fdt pou\u017eito v kritick\u00fdch syst\u00e9mech, vy\u017eaduj\u00edc\u00edch zv\u00fd\u0161enou \u00farove\u0148 spolehlivosti a z\u00e1ruku absence selh\u00e1n\u00ed. Zdrojov\u00e9 texty projektu jsou naps\u00e1ny v jazyce Ada a jeho verifikovateln\u00e9 variant\u011b SPARK 2014. K\u00f3d je distribuov\u00e1n pod licenc\u00ed GPLv3. <\/p>\n
J\u00e1dro odd\u011blen\u00ed p\u0159edstavuje mikro-j\u00e1dro, kter\u00e9 poskytuje prost\u0159ed\u00ed pro prov\u00e1d\u011bn\u00ed izolovan\u00fdch komponent, jejich\u017e interakce jsou p\u0159\u00edsn\u011b regulov\u00e1ny stanoven\u00fdmi pravidly. Izolace je zalo\u017eena na pou\u017eit\u00ed roz\u0161\u00ed\u0159en\u00ed virtualizace Intel VT-x a zahrnuje tak\u00e9 mechanismy ochrany k blokov\u00e1n\u00ed organizace skryt\u00fdch komunika\u010dn\u00edch kan\u00e1l\u016f. J\u00e1dro odd\u011blen\u00ed je minimalisti\u010dt\u011bj\u0161\u00ed a stati\u010dt\u011bj\u0161\u00ed ne\u017e ostatn\u00ed mikro-j\u00e1dra, co\u017e umo\u017e\u0148uje sn\u00ed\u017eit po\u010det situac\u00ed, kter\u00e9 by mohly v\u00e9st k selh\u00e1n\u00ed. <\/p>\n
J\u00e1dro b\u011b\u017e\u00ed v ko\u0159enov\u00e9m re\u017eimu VMX, obdobn\u011b jako hypervizor, zat\u00edmco v\u0161echny ostatn\u00ed komponenty b\u011b\u017e\u00ed v nekorenov\u00e9m re\u017eimu VMX, obdobn\u011b jako hostitelsk\u00e9 syst\u00e9my. P\u0159\u00edstup k hardwaru se realizuje pomoc\u00ed roz\u0161\u00ed\u0159en\u00ed Intel VT-d DMA a p\u0159emapov\u00e1n\u00ed p\u0159eru\u0161en\u00ed, co\u017e umo\u017e\u0148uje bezpe\u010dn\u00e9 p\u0159i\u0159azen\u00ed PCI za\u0159\u00edzen\u00ed k komponent\u00e1m, kter\u00e9 b\u011b\u017e\u00ed pod spr\u00e1vou Muen.
<\/center> <\/p>\n
Mezi mo\u017enosti Muen pat\u0159\u00ed podpora v\u00edcej\u00e1drov\u00fdch syst\u00e9m\u016f, vlo\u017een\u00fdch str\u00e1nek pam\u011bti (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), tabulek atribut\u016f str\u00e1nek pam\u011bti (PAT, Page Attribute Table). Muen tak\u00e9 poskytuje pevn\u00fd cyklick\u00fd pl\u00e1nova\u010d zalo\u017een\u00fd na vyhazovac\u00edm \u010dasova\u010di Intel VMX, kompaktn\u00ed runtime, kter\u00fd neovliv\u0148uje v\u00fdkon, syst\u00e9m auditu selh\u00e1n\u00ed, mechanismus statick\u00e9ho p\u0159i\u0159azen\u00ed zdroj\u016f na z\u00e1klad\u011b pravidel, syst\u00e9m zpracov\u00e1n\u00ed ud\u00e1lost\u00ed a kan\u00e1ly sd\u00edlen\u00e9 pam\u011bti pro interakci mezi spu\u0161t\u011bn\u00fdmi komponentami. <\/p>\n
![\"Vyd\u00e1n\u00ed](\"\/wp-content\/uploads\/2021\/10\/bd30e656326f6fd3667eec5773341420.jpg\")
<\/center> <\/p>\n