Микрокернелот 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