Компанията General Dynamics C4 Systems и австралийският изследователски център NICTA откриха със свободен лиценз сорс-кодовете на микроядрото seL4 (Secure Embedded L4). Това ядро е предназначено за създаване на изключително надеждни операционни системи. Сорсът на seL4 е достъпен с GPLv2 лиценз, а помощните програми за работа с него съдържат компоненти както с лиценз GPLv2, така и с BSD.
Според много онлайн-източници, коректността на микроядрото seL4 е доказана по математичен път, което предполага, че софтуерните решения, базирани на seL4 могат да бъдат считани за най-надеждните в света. Микроядрото seL4 изцяло покрива заложените в него спецификации и не допуска грешки от типа на препълване на буфера, блокиране на адресни блокове, неинициализирани променливи и други. Ядрото е предназначено за създаване на критично важни компютърни системи, използвани в авиацията, медицината, финансовия сектор, енергетиката и други области, за които се гарантира, че няма да има непредвидени прекъсвания и грешки.
На програмистите се предлага комплектът за разработка на софтуер CAmkES, позволяващ моделиране и създаване на системи, базирани на seL4. Включени са примери и прототипи. Поддържат се архитектурите ARMv6 (ARM11), ARMv7 (Cortex A8, A9, A15) и x86.
Върху микроядрото seL4 може да бъде стартирано Linux-ядро, като в този случай seL4 изпълнява ролята на хипервайзор.
Всичко важно от света на технологиите, директно в пощата ти.
С абонирането приемате нашите Условия и Политика за поверителност. Може да се отпишете с един клик по всяко време.
Коментирайте статията в нашите Форуми. За да научите първи най-важното, харесайте страницата ни във Facebook, и ни последвайте в Google Новини, TikTok, Telegram и Viber или изтеглете приложението на Kaldata.com за Android, iPhone, Huawei, Google Chrome, Microsoft Edge и Opera!
