Безбеден оперативен систем со отворен код на Google KataOS

Google го објави откривањето на развојот на настаните поврзани со проектот KataOS, чија цел е создавање безбеден оперативен систем за вграден хардвер. Компонентите на системот KataOS се напишани во Rust и работат на врвот на микрокернелот seL4, за што е обезбеден математички доказ за веродостојноста на системите RISC-V, што покажува дека кодот целосно е во согласност со спецификациите наведени во формалниот јазик. Проектниот код е отворен под лиценцата Apache 2.0.

Системот обезбедува поддршка за платформи базирани на архитектури RISC-V и ARM64. За да се симулира работата на seL4 и околината KataOS на врвот на хардверот, рамката Renode се користи за време на процесот на развој. Како референтна имплементација, предложен е софтверскиот и хардверскиот комплекс Sparrow, кој комбинира KataOS со безбедни чипови базирани на платформата OpenTitan. Предложеното решение ви овозможува да комбинирате логично потврдено јадро на оперативниот систем со доверливи хардверски компоненти (RoT, Root of Trust), изградени со користење на платформата OpenTitan и архитектурата RISC-V. Покрај кодот KataOS, во иднина се планира да се отворат и сите други компоненти на Sparrow, вклучувајќи ја и хардверската компонента.

Платформата се развива со цел примена во специјализирани чипови дизајнирани да работат апликации за машинско учење и обработка на доверливи информации, кои бараат посебно ниво на заштита и потврда за отсуство на дефекти. Примери за такви апликации вклучуваат системи кои манипулираат со слики од луѓе и гласовни снимки. Употребата на KataOS за проверка на доверливоста осигурува дека ако еден дел од системот не успее, дефектот нема да се прошири на остатокот од системот и, особено, на јадрото и критичните делови.

Архитектурата seL4 е забележлива по подвижните делови за управување со ресурсите на кернелот во корисничкиот простор и примената на истите алатки за контрола на пристап за такви ресурси како и за корисничките ресурси. Микрокернелот не обезбедува готови апстракции на високо ниво за управување со датотеки, процеси, мрежни врски и слично, наместо тоа, тој обезбедува само минимални механизми за контролирање на пристапот до физичкиот адресен простор, прекините и ресурсите на процесорот. Апстракциите на високо ниво и двигателите за интеракција со хардверот се имплементирани посебно на врвот на микрокернелот во форма на задачи на ниво на корисник. Пристапот до таквите задачи до ресурсите достапни на микрокернелот е организиран преку дефинирање на правила.

За дополнителна заштита, сите компоненти освен микрокернелот се природно развиени во Rust користејќи безбедни техники за програмирање кои ги минимизираат грешките во меморијата што доведуваат до проблеми како што се пристап до меморијата по ослободувањето, дереференции на нула покажувач и пречекорувања на баферот. Во Rust беа напишани вчитувач на апликации во околината seL4, системски услуги, рамка за развој на апликации, API за пристап до системски повици, менаџер на процеси, механизам за динамична распределба на меморијата итн. Потврденото склопување го користи комплетот алатки CAmkES, развиен од проектот seL4. Компонентите за CAmkES може да се креираат и во Rust.

Rust ја наметнува безбедноста на меморијата во времето на компајлирање преку проверка на референци, сопственост на објектот и следење на животниот век на објектот (обеми) и со проценка на исправноста на пристапите до меморијата при извршување. Rust, исто така, обезбедува заштита од прелевање на цели броеви, бара вредностите на променливите да се иницијализираат пред употреба, стандардно го користи концептот на непроменливи референци и променливи и нуди силно статичко пишување за да се минимизираат логичките грешки.

Извор: opennet.ru