RISC-V Foundation om verificering af mikrokerneoperativsystemet på systemer med RISC-V instruktionssætarkitektur. Verificeringen går ud på for pålideligheden af seL4, som viser fuld overensstemmelse med de specifikationer, der er angivet på formelt sprog. Beviset for pålidelighed seL4 i kritisk vigtige systemer baseret på RISC-V RV64-processorer, som kræver et højere niveau af pålidelighed og garanterer fravær af fejl. Softwarens udviklere, der arbejder ovenpå seL4-kerne, kan være helt sikre på, at i tilfælde af en fejl i en del af systemet vil denne fejl ikke sprede sig til resten af systemet, især ikke til dets kritiske dele.
Oprindeligt blev mikrokerne seL4 verificeret til 32-bit ARM-processorer, og senere til 64-bit x86-processorer. Det bemærkes, at kombinationen af den åbne hardwarearkitektur RISC-V med den åbne mikrokerne seL4 vil opnå et nyt sikkerhedsniveau, da hardwarekomponenter i fremtiden også kan blive fuldt verificeret, hvilket ikke er muligt med proprietære hardwarearkitekturer.
Ved verificering af seL4 antages det, at hardwaren fungerer som angivet, og at specifikationen fuldt ud beskriver systemets adfærd, men i praksis er hardwaren ikke fejlfri, som tydeligt demonstreres af de regelmæssigt opståede problemer i mekanismen for spekulativ udførelse af instruktioner. Åbne hardwareplatforme letter integrationen af sikkerhedsrelaterede ændringer — for eksempel for at blokere alle mulige lækkagekanaler, hvor det er betydeligt mere effektivt at løse hardwareproblemerne end at forsøge at finde softwareløsninger.
Lad os minde om, at arkitekturen seL4 udtræk af komponenter til styring af kerneressourcer i brugerens rum og anvendelse af de samme adgangsbegrænsningsmetoder for disse ressourcer som for brugeressourcer. Mikrokerne leverer ikke klar til brug højniveau-abstraktioner til håndtering af filer, processer, netværksforbindelser osv.; i stedet giver den kun minimale mekanismer til at styre adgangen til det fysiske adresseområde, afbrydelser og CPU-ressourcer. Højniveau-abstraktioner og drivere til interaktion med hardware implementeres separat oven på mikro-kernen i form af opgaver, der udføres på brugerens niveau. Adgangen for disse opgaver til de ressourcer, mikro-kernen har, organiseres gennem fastsættelse af regler.
RISC-V tilbyder et åbent og fleksibelt system af maskininstruktioner, der muliggør oprettelse af mikroprocessorer til vilkårlige anvendelser uden krav om afgifter og uden restriktioner for brugen. RISC-V muliggør oprettelse af helt åbne SoC'er og processorer. I øjeblikket er der adskillige virksomheder og samfund, der arbejder med RISC-V-specifikationen under forskellige åbne licenser (BSD, MIT, Apache 2.0). flere dusin varianter af mikroprocessor-kernene, SoC'er og allerede producerede chips. RISC-V-support findes fra versionerne Glibc 2.27, binutils 2.30, gcc 7 og Linux-kernen 4.15.
Kilde: opennet.ru
