Organisatie RISC-V Foundation over de verificatie van de werking van het microkernelsysteem op systemen met de RISC-V instructieset. De verificatie komt neer op van de betrouwbaarheid van seL4, wat aantoont dat het volledig voldoet aan de specificaties die in formele taal zijn vastgesteld. Het bewijs van betrouwbaarheid seL4 in kritieke systemen gebaseerd op RISC-V RV64-processoren te gebruiken, die een hoger niveau van betrouwbaarheid vereisen en garant staan voor het ontbreken van fouten. Ontwikkelaars van software die bovenop de seL4-kernel draait, kunnen er volledig op vertrouwen dat in het geval van een storing in een deel van het systeem, deze storing zich niet zal verspreiden naar de rest van het systeem en, met name, naar de kritieke delen ervan.
Oorspronkelijk werd de seL4 microkernelsysteem geverifieerd voor 32-bits ARM-processoren en later voor 64-bits x86-processoren. Het wordt opgemerkt dat de combinatie van de open hardwarearchitectuur RISC-V met de open seL4 microkernel een nieuw niveau van veiligheid zal bereiken, aangezien de hardwarecomponenten in de toekomst ook volledig kunnen worden geverifieerd, wat niet mogelijk is met propriƫtaire hardwarearchitecturen.
Bij de verificatie van seL4 wordt verondersteld dat de hardware werkt zoals verklaard en dat de specificatie het gedrag van het systeem volledig beschrijft, maar in werkelijkheid is de hardware niet vrij van fouten, wat goed wordt aangetoond door de regelmatig opdoemende problemen in de mechanismen voor speculatieve uitvoering van instructies. Open hardwareplatforms vergemakkelijken de integratie van beveiligingsgerelateerde wijzigingen ā bijvoorbeeld om alle mogelijke kanalen van informatielekkage via zijkanalen te blokkeren, wat veel effectiever kan worden opgelost met hardware dan door te proberen softwarematige workarounds te vinden.
Ter herinnering, de architectuur van seL4 de onderdelen voor het beheer van de kernresources naar de gebruikersruimte te verplaatsen en dezelfde toegangsbeheermethoden voor deze resources toe te passen als voor gebruikersresources. Het microkern biedt geen kant-en-klare high-level abstraheringen voor het beheer van bestanden, processen, netwerkverbindingen, enzovoort; in plaats daarvan biedt het alleen minimale mechanismen voor toegang tot de fysieke adresruimte, onderbrekingen en CPU-resources. High-level abstraheringen en drivers voor interactie met hardware worden separaat bovenop het microkern geĆÆmplementeerd in de vorm van taken die op gebruikersniveau worden uitgevoerd. De toegang van deze taken tot de resources van het microkern wordt georganiseerd via het definiĆ«ren van regels.
RISC-V biedt een open en flexibele set van machine-instructies die het mogelijk maakt om microprocessors te creƫren voor verschillende toepassingsgebieden, zonder royalties te vereisen en zonder voorwaarden voor gebruik. RISC-V maakt het mogelijk om volledig open SoC's en processors te ontwikkelen. Momenteel zijn er op basis van de RISC-V specificatie verschillende bedrijven en gemeenschappen bezig met de ontwikkeling van meerdere open licenties (BSD, MIT, Apache 2.0). een paar tientallen varianten van microprocessor-kernen, SoC's en al geproduceerde chips. Ondersteuning voor RISC-V is aanwezig sinds de release van Glibc 2.27, binutils 2.30, gcc 7 en de Linux-kern 4.15.
Bron: opennet.ru
