Микроядрото seL4 е математически проверено за архитектурата RISC-V

Фондация RISC-V съобщава относно проверката на работата на микроядрото seL4 на системи с архитектура на набор от инструкции RISC-V. Проверката се свежда до математическо доказателство надеждност на работата на seL4, което показва пълно съответствие със спецификациите, посочени във официалния език. Доказателство за надеждност ви позволява да използвате seL4 в критични за мисията системи, базирани на процесори RISC-V RV64, които изискват повишено ниво на надеждност и гарантират липсата на повреди. Разработчиците на софтуер, работещ върху ядрото seL4, могат да бъдат напълно уверени, че ако има повреда в една част от системата, тази повреда няма да се разпространи в останалата част от системата и по-специално в нейните критични части.

Микроядрото seL4 първоначално беше проверено за 32-битови ARM процесори, а по-късно за 64-битови x86 процесори. Отбелязва се, че комбинацията от отворената хардуерна архитектура RISC-V с отвореното микроядро seL4 ще постигне ново ниво на сигурност, тъй като хардуерните компоненти също могат да бъдат напълно проверени в бъдеще, което е невъзможно да се постигне за частни хардуерни архитектури.

При проверката на seL4 се приема, че оборудването работи както е посочено и спецификацията описва напълно поведението на системата, но в действителност оборудването не е без грешки, което е ясно демонстрирано от редовно възникващи проблеми в механизма за спекулативно изпълнение на инструкции. Отворените хардуерни платформи улесняват интегрирането на промени, свързани със сигурността - например, за блокиране на всички възможни течове на странични канали, където е много по-ефективно да се отървете от проблема в хардуера, отколкото да се опитвате да намерите решения в софтуера.

Спомнете си, че архитектурата seL4 забележителен преместване на части за управление на ресурсите на ядрото в потребителското пространство и прилагане на същите средства за контрол на достъпа за такива ресурси, както за потребителските ресурси. Микроядрото не предоставя готови абстракции на високо ниво за управление на файлове, процеси, мрежови връзки и други подобни; вместо това предоставя само минимални механизми за контролиране на достъпа до физическо адресно пространство, прекъсвания и ресурси на процесора. Абстракциите на високо ниво и драйверите за взаимодействие с хардуера се изпълняват отделно върху микроядрото под формата на задачи на потребителско ниво. Достъпът на такива задачи до наличните ресурси на микроядрото се организира чрез дефиниране на правила.

RISC-V предоставя отворена и гъвкава система за машинни инструкции, която позволява изграждането на микропроцесори за произволни приложения, без да се изискват хонорари или низове, прикачени за използване. RISC-V ви позволява да създавате напълно отворени SoC и процесори. В момента се основава на спецификацията RISC-V от различни компании и общности под различни безплатни лицензи (BSD, MIT, Apache 2.0) се развива няколко десетки варианта на микропроцесорни ядра, SoC и вече произведени чипове. Поддръжката на RISC-V присъства от изданията на Glibc 2.27, binutils 2.30, gcc 7 и Linux ядрото 4.15.

Източник: opennet.ru