Фондация RISC-V обяви, че е проверила как работи микроядрото seL4 в системи с архитектурата на набора инструкции RISC-V. При което процесът на проверка се свежда до математически тест за надеждност на seL4, който показва пълно съответствие със спецификациите, посочени на официален език.
Тестовете за надеждност позволяват seL4 да се използва в критично важни системи, базирани на процесори RISC-V RV64, което изисква по-високо ниво на надеждност и не гарантира отказ.
Разработчиците на софтуер, работещи върху ядрото 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.
Относно тестването на микроядрото seL4
Първоначално микроядрото seL4 беше проверен за 32-битови ARM процесориИ по-късно за x86 64-битови процесори.
Забелязва се, че комбинацията от отворена хардуерна архитектура RISC-V с отвореното микроядро seL4 ще постигне ново ниво на сигурносттъй като хардуерните компоненти в бъдеще също могат да бъдат напълно проверени, което е невъзможно да се постигне за собствени хардуерни архитектури.
Когато проверяваме seL4, трябва да приемем, че хардуерът работи правилно (т.е. както е посочено). Това предполага, че на първо място има недвусмислена спецификация, което не е така за целия хардуер.
Но дори когато такава спецификация съществува и е формална (тоест, в математически формализъм, който поддържа математически разсъждения за нейните свойства), как да разберем, че тя всъщност улавя поведението на хардуера?
Реалността е, че можем да бъдем почти сигурни, че не е така. Хардуерът не се различава от софтуера по това, че и двата са бъги.
Но наличието на отворен ISA има предимства, които надхвърлят възможността да не се плаща безплатно. Едната е, че позволява хардуерни реализации с отворен код.
При проверка на seL4 се приема, че оборудването работи както е посочено и спецификацията напълно описва поведението на системата, но всъщност оборудването не е без грешки, което е добре демонстрирано от проблеми, които редовно възникват в инструкциите на спекулативния механизъм за изпълнение .
Отворените хардуерни платформи опростяват интегрирането на промените свързани със сигурността, например, за блокиране на всички възможни канали за изтичане през канали на трети страни, където е много по-ефективно да се отървете от проблема чрез хардуер, отколкото да се опитате да намерите решения чрез софтуер.
И накрая, ако искате да научите повече за това, можете да се запознаете с бележката в следваща връзка.