МАТЕРИАЛИ
Свръхнадеждното микроядро seL4 беше пуснато за свободно ползване под GNU-лиценза GPLv2
Специализираната във разработването на високи технологии с военно предназначение компания General Dynamics C4 Systems в партньорство с Австралийския национален център за информационни и комуникационни технологии NICTA пуснаха свободно при условията на Версия 2 на GNU General Public License (GPLv2) изходния код на разработеното от тях свръхнадеждно микроядро Secure Embedded L4 (seL4). Част от помощните програми за работа с микроядрото seL4 съдържат компоненти под лиценза GPLv2 и такива под лиценза Berkeley Software Distribution (BSD), което позволява тяхното последващо затваряне.
Микроядрото seL4 е предназначено за изграждането на изключително надеждни операционни системи и поддържането на критично важни компютърни процеси в областта на военните технологии и сигурността, авиацията, енергетиката, медицината, електронното банкиране и други – където стабилността е от особена важност, а допускането на грешки от типа на препълване на буфери, блокиране на адресни блокове, неинициализирани променливи и други е наложително да се сведе до възможния технологичен минимум.
Основен източник на уязвимости при електронните системи е именно тяхната базовата архитектура и системното ядро, което управлява процесите на най-ниско ниво. Когато там бъде допуснат пробив, всички следващи слоеве от хардуерното и софтуерното осигуряване могат да бъдат засегнати фатално – независимо дали става дума за системи с вградени устройства с единично предназначение (например отваряне и затваряне на входната врата) или за сложни системи с мултипроцесорни сървъри (например спътникова навигация).
Създателите на seL4 обосновават неговата надеждност с математически способи и твърдят, че базираните на това микроядро решения могат да бъдат считани за най-надеждните в света. „Надеждността на системата има много общо с нейния размер – пишат разработчиците. – Дори и добре проектираният програмен код може да има до няколко дефекта в хилядите редове код. Следователно, по-голямата система [потенциално] има повече грешки, отколкото една по-малка система“. Надеждността е от особено значение за ядрото, тъй като то управлява хардуера на най-ниското ниво, където осигуряването с допълнителни защити е невъзможно (самото микроядро е отговорно за контролиране на механизмите за защита на хардуера). Ето защо дори минимална грешка в микроядрото може да се окаже фатална за системата.
Микроядрото seL4 е едно от най-малките ядра за общо приложение в света и това го прави подходящо при разработването на надежден софтуер – особено когато софтуерът ще поддържа критично важни системи. Надеждността му е обезпечена в рамките на проекта L4.verified, където са приложени процедури за разработване и официална проверка на изпълнението, съдържащи математическо проследяване на качествата на изходния код, дизайна на ядрото и организационните взаимовръзки при изграждането на разработката.
На разработчиците, които се интересуват от микроядрото seL4, се предлага комплект за разработка на софтуер CAmkES, позволяващ моделиране и създаване на системи, базирани на seL4. Включени са примери и прототипи. Поддържат се архитектурите ARMv6 (ARM11), ARMv7 (Cortex A8, A9, A15) и x86. Микроядрото позволява да бъде стартирано Linux-ядро, където seL4 изпълнява ролята на хипервайзор. Всеки желаещ може съгласно условията на свободния лиценз GPLv2 да свали свободно копие от изходния код на ядрото и да го използва за своите собствени разработки – без да е необходимо да получава изрично разрешение за това.
