RISC-V verifierade seL4-mikrokärnan på sina RV64-processorer

RISC-V Foundation meddelade att den har verifierat hur mikrokärnan fungerar seL4 i system med instruktionsuppsättningsarkitekturen Risc-v. I vilken verifieringsprocessen reduceras till det matematiska beviset på tillförlitligheten hos seL4, vilket indikerar fullständig överensstämmelse med specifikationerna som anges på ett formellt språk.

Pålitlighetstestning gör att seL4 kan användas i uppdragskritiska system baserade på RISC-V-processorer RV64, vilket kräver högre tillförlitlighet och inte garanterar fel.

Programvaruutvecklare som körs ovanpå seL4-kärnan kan vara helt säkra på att i händelse av ett fel i en del av systemet kommer detta fel inte att spridas till resten av systemet och i synnerhet till dess kritiska delar.

Om seL4

SeL4-arkitekturen är anmärkningsvärt för att ta bort delar för att hantera kärnresurser i användarutrymme och använda samma åtkomstkontrollmetoder för sådana resurser som för användarresurser.

Mikrokärnan ger inte abstraktioner på hög nivå redan redo att hantera filer, processer, nätverksanslutningar etc. men istället tillhandahåller endast minimala mekanismer för att kontrollera åtkomst till det fysiska adressutrymmet, avbryter och processorresurser.

Abstraktioner på hög nivå och styrenheter för interaktion med datorn implementeras separat ovanpå mikrokärnan i form av uppgifter som utförs på användarnivå.

Tillgången till sådana uppgifter till de resurser som finns i mikrokärnan organiseras genom definition av regler.

RISC-V erbjuder ett öppet och flexibelt system av maskininstruktioner som gör det möjligt att skapa mikroprocessorer för godtyckliga applikationer utan att det krävs avdrag och utan att införa användningsvillkor.

Med RISC-V kan du skapa helt öppna processorer och SoC. För närvarande, på grundval av RISC-V-specifikationen, utvecklar flera företag och samhällen under olika gratislicenser (BSD, MIT, Apache 2.0) flera dussin varianter av redan producerade mikroprocessorkärnor, SoC och chips.

RISC-V-stöd har funnits sedan lanseringen av Glibc 2.27, binutils 2.30, gcc 7 och Linux 4.15-kärnan.

Om seL4 mikrokernel testning

Inledningsvis mikrokärnan seL4 verifierades för 32-bitars ARM-processorerOch senare för x86 64-bitars processorer.

Det observeras att kombinationen av RISC-V öppen hårdvaruarkitektur med den öppna mikrokärnan seL4 kommer att uppnå en ny säkerhetsnivåeftersom hårdvarukomponenterna i framtiden också kan verifieras helt, vilket är omöjligt att uppnå för egna hårdvaruarkitekturer.

När vi kontrollerar seL4 måste vi anta att hårdvaran fungerar som den ska (det vill säga som specificerat). Det förutsätter att det finns en entydig specifikation i första hand, vilket inte är fallet för all hårdvara. 

Men även när en sådan specifikation existerar och den är formell (det vill säga ritad i en matematisk formalism som stöder matematisk resonemang om dess egenskaper), hur vet vi att den faktiskt fångar upp hårdvarans beteende? 

Verkligheten är att vi kan vara ganska säkra på att det inte är det. Maskinvara skiljer sig inte från programvara eftersom båda är buggiga.

Men att ha en öppen ISA har fördelar som går utöver att vara royaltyfri. En är att den möjliggör implementering av öppen källkod.

Vid kontroll av seL4 antas att utrustningen fungerar som angivet och specifikationen beskriver systemets beteende fullständigt, men faktiskt är utrustningen inte felfri, vilket demonstreras väl av problem som regelbundet uppstår i den spekulativa körmekanismens instruktioner.

Öppna maskinvaruplattformar förenklar integrationen av ändringar relaterad till säkerhet, till exempel för att blockera alla möjliga läckagekanaler via tredjepartskanaler, där det är mycket effektivare att bli av med ett problem med hårdvara än att försöka hitta lösningar med programvara.

Slutligen, om du vill veta mer om det, kan du läsa anteckningen i följande länk.