RISC-V Foundation om at verificere mikrokernens funktion på systemer med RISC-V instruktionssætarkitektur. Verifikation kommer ned til pålideligheden af seL4-drift, hvilket indikerer fuld overensstemmelse med specifikationerne specificeret på det formelle sprog. Bevis for pålidelighed seL4 i missionskritiske systemer baseret på RISC-V RV64-processorer, der kræver et øget niveau af pålidelighed og garanterer fravær af fejl. Udviklere af software, der kører oven på seL4-kernen, kan være helt sikre på, at hvis der er en fejl i en del af systemet, vil denne fejl ikke sprede sig til resten af systemet og især dets kritiske dele.
seL4-mikrokernen blev oprindeligt verificeret til 32-bit ARM-processorer og senere til 64-bit x86-processorer. Det bemærkes, at kombinationen af den åbne RISC-V hardwarearkitektur med den åbne seL4 mikrokerne vil opnå et nyt sikkerhedsniveau, da hardwarekomponenterne også kan verificeres fuldt ud i fremtiden, hvilket er umuligt at opnå for proprietære hardwarearkitekturer.
Ved verificering af seL4 antages det, at udstyret fungerer som angivet, og at specifikationen fuldt ud beskriver systemets opførsel, men i virkeligheden er udstyret ikke fri for fejl, hvilket tydeligt demonstreres ved regelmæssigt opståede problemer i mekanismen for spekulativ udførelse af instruktioner. Åbne hardwareplatforme gør det nemmere at integrere sikkerhedsrelaterede ændringer – for eksempel at blokere alle mulige sidekanallækager, hvor det er meget mere effektivt at slippe af med problemet i hardware end at forsøge at finde løsninger i software.
Husk at seL4-arkitekturen bevægelige dele til styring af kerneressourcer ind i brugerrummet og anvendelse af de samme adgangskontrolmidler for sådanne ressourcer som for brugerressourcer. Mikrokernen giver ikke færdige abstraktioner på højt niveau til styring af filer, processer, netværksforbindelser og lignende; i stedet giver den kun minimale mekanismer til at kontrollere adgang til fysisk adresserum, afbrydelser og processorressourcer. Abstraktioner på højt niveau og drivere til interaktion med hardware er implementeret separat oven på mikrokernen i form af opgaver på brugerniveau. Adgang til sådanne opgaver til de ressourcer, der er tilgængelige for mikrokernen, organiseres gennem definition af regler.
RISC-V giver et åbent og fleksibelt maskininstruktionssystem, der gør det muligt at bygge mikroprocessorer til vilkårlige applikationer uden at kræve royalties eller strenge knyttet til brug. RISC-V giver dig mulighed for at oprette helt åbne SoC'er og processorer. I øjeblikket baseret på RISC-V-specifikationen af forskellige virksomheder og samfund under forskellige gratis licenser (BSD, MIT, Apache 2.0) flere dusin varianter af mikroprocessorkerner, SoC'er og allerede producerede chips. RISC-V-understøttelse har været til stede siden udgivelserne af Glibc 2.27, binutils 2.30, gcc 7 og Linux-kernen 4.15.
Kilde: opennet.ru