RISC-V Foundation om att verifiera mikrokärnan på system med RISC-V instruktionsuppsättningsarkitektur. Verifiering handlar om tillförlitligheten för seL4-drift, vilket indikerar full överensstämmelse med specifikationerna som anges på det formella språket. Bevis på tillförlitlighet seL4 i verksamhetskritiska system baserade på RISC-V RV64-processorer som kräver en ökad nivå av tillförlitlighet och garanterar frånvaro av fel. Utvecklare av programvara som körs ovanpå seL4-kärnan kan vara helt övertygade om att om det finns ett fel i en del av systemet, kommer detta fel inte att sprida sig till resten av systemet och i synnerhet dess kritiska delar.
seL4-mikrokärnan verifierades initialt för 32-bitars ARM-processorer och senare för 64-bitars x86-processorer. Det noteras att kombinationen av den öppna RISC-V-hårdvaruarkitekturen med den öppna seL4-mikrokärnan kommer att uppnå en ny säkerhetsnivå, eftersom hårdvarukomponenterna också kan verifieras fullt ut i framtiden, vilket är omöjligt att uppnå för proprietära hårdvaruarkitekturer.
Vid verifiering av seL4 antas det att utrustningen fungerar som angivet och att specifikationen fullständigt beskriver systemets beteende, men i verkligheten är utrustningen inte fri från fel, vilket tydligt visas av regelbundet uppkommande problem i mekanismen för spekulativt utförande av instruktioner. Öppna hårdvaruplattformar gör det lättare att integrera säkerhetsrelaterade förändringar – till exempel att blockera alla möjliga sidokanalläckor, där det är mycket effektivare att bli av med problemet i hårdvaran än att försöka hitta lösningar i mjukvara.
Kom ihåg att seL4-arkitekturen rörliga delar för att hantera kärnresurser till användarutrymme och tillämpa samma åtkomstkontrollorgan för sådana resurser som för användarresurser. Mikrokärnan tillhandahåller inte färdiga abstraktioner på hög nivå för hantering av filer, processer, nätverksanslutningar och liknande, utan tillhandahåller endast minimala mekanismer för att kontrollera åtkomst till fysiskt adressutrymme, avbrott och processorresurser. Abstraktioner på hög nivå och drivrutiner för interaktion med hårdvara implementeras separat ovanpå mikrokärnan i form av uppgifter på användarnivå. Tillgång till sådana uppgifter till de resurser som är tillgängliga för mikrokärnan organiseras genom definition av regler.
RISC-V tillhandahåller ett öppet och flexibelt maskininstruktionssystem som gör att mikroprocessorer kan byggas för godtyckliga applikationer utan att kräva royalties eller strängar för användning. RISC-V låter dig skapa helt öppna SoC:er och processorer. För närvarande baserad på RISC-V-specifikationen av olika företag och gemenskaper under olika fria licenser (BSD, MIT, Apache 2.0) flera dussin varianter av mikroprocessorkärnor, SoCs och redan producerade chips. RISC-V-stöd har funnits sedan versionerna av Glibc 2.27, binutils 2.30, gcc 7 och Linux-kärnan 4.15.
Källa: opennet.ru