Stichting RISC-V over het verifiëren van de werking van de microkernel op systemen met RISC-V-instructiesetarchitectuur. Verificatie komt neer op betrouwbaarheid van de seL4-werking, wat duidt op volledige overeenstemming met de specificaties gespecificeerd in de formele taal. Bewijs van betrouwbaarheid seL4 in bedrijfskritische systemen op basis van RISC-V RV64-processors die een hoger betrouwbaarheidsniveau vereisen en de afwezigheid van storingen garanderen. Ontwikkelaars van software die bovenop de seL4-kernel draait, kunnen er volledig op vertrouwen dat als er een fout optreedt in één deel van het systeem, deze fout zich niet zal verspreiden naar de rest van het systeem en in het bijzonder naar de kritieke delen ervan.
De seL4-microkernel werd aanvankelijk geverifieerd voor 32-bits ARM-processors en later voor 64-bit x86-processors. Opgemerkt wordt dat de combinatie van de open RISC-V-hardwarearchitectuur met de open seL4-microkernel een nieuw beveiligingsniveau zal bereiken, aangezien de hardwarecomponenten in de toekomst ook volledig kunnen worden geverifieerd, wat onmogelijk te bereiken is voor propriëtaire hardware-architecturen.
Bij het verifiëren van seL4 wordt aangenomen dat de apparatuur werkt zoals aangegeven en dat de specificatie het gedrag van het systeem volledig beschrijft, maar in werkelijkheid is de apparatuur niet vrij van fouten, wat duidelijk wordt aangetoond door regelmatig opduikende problemen in het mechanisme van speculatieve uitvoering van instructies. Open hardwareplatforms maken het gemakkelijker om beveiligingsgerelateerde veranderingen te integreren, bijvoorbeeld om alle mogelijke zijkanaallekken te blokkeren, waarbij het veel efficiënter is om het probleem in de hardware op te lossen dan te proberen oplossingen te vinden in de software.
Bedenk dat de seL4-architectuur het verplaatsen van delen voor het beheren van kernelbronnen naar de gebruikersruimte en het toepassen van dezelfde toegangscontrolemiddelen voor dergelijke bronnen als voor gebruikersbronnen. De microkernel biedt geen kant-en-klare abstracties op hoog niveau voor het beheren van bestanden, processen, netwerkverbindingen en dergelijke; in plaats daarvan biedt het slechts minimale mechanismen voor het controleren van de toegang tot fysieke adresruimte, interrupts en processorbronnen. Abstracties op hoog niveau en stuurprogramma's voor interactie met hardware worden afzonderlijk bovenop de microkernel geïmplementeerd in de vorm van taken op gebruikersniveau. De toegang van dergelijke taken tot de bronnen die beschikbaar zijn voor de microkernel wordt georganiseerd door het definiëren van regels.
RISC-V biedt een open en flexibel machine-instructiesysteem waarmee microprocessors kunnen worden gebouwd voor willekeurige toepassingen zonder dat er royalty's of verplichtingen aan verbonden zijn. Met RISC-V kunt u volledig open SoC's en processors maken. Momenteel gebaseerd op de RISC-V-specificatie door verschillende bedrijven en gemeenschappen onder verschillende gratis licenties (BSD, MIT, Apache 2.0) enkele tientallen varianten van microprocessorkernen, SoC's en reeds geproduceerde chips. RISC-V-ondersteuning is aanwezig sinds de releases van Glibc 2.27, binutils 2.30, gcc 7 en de Linux-kernel 4.15.
Bron: opennet.ru