{"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\/da\/blog\/news\/vypusk-muen-1-0-otkrytogo-mikroyadra-dlya-sozdaniya-vysokonadyozhnyh-sistem","title":{"rendered":"Udgivelse af Muen 1.0, et \u00e5bent mikrokerne til oprettelse af h\u00f8j-p\u00e5lidelige systemer","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"

Efter otte \u00e5rs udvikling blev projektet Muen 1.0 lanceret, som udvikler kernen for adskillelse (Separation kernel), hvis frav\u00e6r af fejl i kildekoden er bekr\u00e6ftet gennem matematisk formelverifikation af p\u00e5lidelighed. Kernen er tilg\u00e6ngelig for x86_64-arkitektur og kan anvendes i kritiske systemer, der kr\u00e6ver et h\u00f8jt niveau af p\u00e5lidelighed og garanti for frav\u00e6r af nedbrud. Kildekoden til projektet er skrevet i Ada-sproget og dens verifiable dialekt SPARK 2014. Koden distribueres under GPLv3-licensen. <\/p>\n

Adskillelseskernen er et mikrokerne, der giver et milj\u00f8 til udf\u00f8relse af isolerede komponenter, hvis interaktioner strengt reguleres af fastsatte regler. Isoleringen baseres p\u00e5 anvendelsen af Intel VT-x virtualiseringsudvidelser og omfatter ogs\u00e5 beskyttelsesmekanismer til at blokere oprettelsen af skjulte kommunikationskanaler. Adskillelseskernen er mere minimalistisk og statisk sammenlignet med andre mikrokerner, hvilket reducerer antallet af situationer, der kan for\u00e5rsage nedbrud. <\/p>\n

Kernen k\u00f8rer i VMX-root mode p\u00e5 lignende m\u00e5de som en hypervisor, mens alle andre komponenter k\u00f8rer i non-root mode VMX, p\u00e5 samme m\u00e5de som g\u00e6stesystemer. Adgang til hardware sker ved hj\u00e6lp af Intel VT-d DMA-udvidelser og remapping af afbrydelser, hvilket muligg\u00f8r sikker binding af PCI-enheder til komponenter, der k\u00f8res under Muen.

\"Udgivelse<\/center> <\/p>\n

Blandt Muen's muligheder er st\u00f8tte til flerkernede systemer, indlejrede hukommelsessider (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), hukommelsesside-attributtabeller (PAT, Page Attribute Table). Muen leverer ogs\u00e5 en fast cyklisk scheduler baseret p\u00e5 Intel VMX\u2019s preemptive timer, et kompakt runtime, der ikke p\u00e5virker ydeevnen, et system til overv\u00e5gning af nedbrud, en mekanisme til statisk tildeling af ressourcer baseret p\u00e5 regler, et system til behandling af begivenheder og kanaler til delt hukommelse til interaktion mellem de k\u00f8rte komponenter. <\/p>\n

Der underst\u00f8ttes k\u00f8rsel af komponenter p\u00e5 Muen med 64-bit maskinkode, 32- eller 64-bit virtual machines<\/a>, 64-bit applikationer p\u00e5 sprog som Ada og SPARK 2014, virtuelle maskiner med Linux og selvst\u00e6ndige «unikernel» baseret p\u00e5 MirageOS. <\/p>\n

De vigtigste nyskabelser introduceret i udgivelsen af Muen 1.0: <\/p>\n