RISC-V verificerede seL4 microkernel på deres RV64-processorer

RISC-V Foundation meddelte, at den har verificeret hvordan mikrokernen fungerer seL4 i systemer med instruktionssættets arkitektur RISC-V. I hvilken verificeringsprocessen reduceres til det matematiske bevis for pålideligheden af ​​seL4, hvilket indikerer fuld overensstemmelse med specifikationerne specificeret på et formelt sprog.

Pålidelighedstest muliggør, at seL4 kan bruges i missionskritiske systemer baseret på RISC-V-processorer RV64, som kræver et højere niveau af pålidelighed og ikke garanterer fiasko.

Softwareudviklere, der kører oven på seL4-kernen, 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 og især til dets kritiske dele.

Om seL4

SeL4-arkitekturen er bemærkelsesværdig for fjernelse af dele for at administrere kerneressourcer i brugerrummet og bruge de samme adgangskontrolmetoder til sådanne ressourcer som til brugerressourcer.

Microkernel giver ikke abstraktioner på højt niveau allerede klar til at styre filer, processer, netværksforbindelser osv., men i stedet giver kun minimale mekanismer til at kontrollere adgangen til det fysiske adresseområde, afbryder og processorressourcer.

Abstraktioner på højt niveau og controllere til interaktion med computeren implementeres separat oven på mikrokernen i form af opgaver, der udføres på brugerniveau.

Adgangen til sådanne opgaver til de ressourcer, der er tilgængelige i microkernel, er organiseret gennem definition af regler.

RISC-V giver et åbent og fleksibelt system af maskininstruktioner, der gør det muligt at oprette mikroprocessorer til vilkårlige applikationer uden at kræve fradrag og uden at pålægge brugsbetingelser.

RISC-V giver dig mulighed for at oprette helt åbne processorer og SoC'er. På nuværende tidspunkt udvikler flere virksomheder og samfund under forskellige gratis licenser (BSD, MIT, Apache 2.0) på basis af RISC-V-specifikationen flere dusin varianter af allerede producerede mikroprocessorkerner, SoC'er og chips.

RISC-V-support har eksisteret siden frigivelsen af ​​Glibc 2.27, binutils 2.30, gcc 7 og Linux 4.15-kernen.

Om seL4 microkernel test

Oprindeligt mikrokernel seL4 blev verificeret til 32-bit ARM-processorer, Og senere til x86 64-bit processorer.

Det observeres, at kombinationen af ​​RISC-V åben hardware-arkitektur med den åbne mikrokerne seL4 opnår et nyt sikkerhedsniveauda hardwarekomponenterne i fremtiden også kan verificeres fuldt ud, hvilket er umuligt at opnå for proprietære hardwarearkitekturer.

Når vi kontrollerer seL4, skal vi antage, at hardwaren fungerer korrekt (dvs. som specificeret). Det antager, at der er en entydig specifikation i første omgang, hvilket ikke er tilfældet for al hardware. 

Men selv når en sådan specifikation eksisterer, og den er formel (det vil sige ritten i en matematisk formalisme, der understøtter matematisk ræsonnement om dens egenskaber), hvordan ved vi, at den faktisk fanger hardwareens opførsel? 

Virkeligheden er, at vi kan være temmelig sikre på, at det ikke er tilfældet. Hardware adskiller sig ikke fra software, idet begge er buggy.

Men at have en åben ISA har fordele, der går ud over at være royaltyfri. Den ene er, at den tillader open source-hardwareimplementeringer.

Ved kontrol af seL4 antages det, at udstyret fungerer som angivet, og specifikationen beskriver systemets opførsel fuldt ud, men faktisk er udstyret ikke fejlfrit, hvilket godt demonstreres af problemer, der regelmæssigt opstår i instruktionerne til den spekulative udførelsesmekanisme.

Åbne hardwareplatforme forenkler integrationen af ​​ændringer relateret til sikkerhed, for eksempel at blokere alle mulige lækagekanaler gennem tredjepartskanaler, hvor det er meget mere effektivt at slippe af med et problem end hardware end at forsøge at finde løsninger med software.

Endelig, hvis du vil vide mere om det, kan du se noten i følgende link.