De RISC-V Foundation heeft aangekondigd te hebben geverifieerd hoe de microkernel werkt seL4 in systemen met de instructieset architectuur RISC-V. Waarbij het verificatieproces wordt gereduceerd tot het wiskundige bewijs van de betrouwbaarheid van seL4, wat aangeeft dat volledig wordt voldaan aan de specificaties gespecificeerd in een formele taal.
Dankzij betrouwbaarheidstests kan seL4 worden gebruikt in bedrijfskritische systemen op basis van RISC-V-processors RV64, die een hogere mate van betrouwbaarheid vereist en geen uitval garandeert.
Softwareontwikkelaars die bovenop de seL4-kernel draaien, kunnen er volledig zeker van zijn dat in het geval van een storing in een deel van het systeem, deze storing zich niet verspreidt naar de rest van het systeem en in het bijzonder naar de kritieke onderdelen ervan.
Over seL4
De seL4-architectuur het valt op door het verwijderen van onderdelen om kernelbronnen in de gebruikersruimte te beheren en gebruik dezelfde methoden voor toegangscontrole voor dergelijke bronnen als voor gebruikersbronnen.
De microkernel biedt geen abstracties op hoog niveau al voorbereid om bestanden, processen, netwerkverbindingen, enz. te beheren, maar in plaats daarvan biedt slechts minimale mechanismen om de toegang tot de fysieke adresruimte te controleren, interrupts en processorbronnen.
Abstracties op hoog niveau en stuurprogramma's voor interactie met de computer worden afzonderlijk bovenop de microkernel geïmplementeerd in de vorm van taken die op gebruikersniveau worden uitgevoerd.
De toegang van dergelijke taken tot de bronnen die beschikbaar zijn in de microkernel wordt georganiseerd door middel van de definitie van regels.
RISC-V biedt een open en flexibel systeem van machine-instructies die maakt het mogelijk om microprocessors te maken voor willekeurige toepassingen, zonder aftrekposten en zonder gebruiksvoorwaarden op te leggen.
Met RISC-V kunt u volledig open processors en SoC's maken. Momenteel ontwikkelen verschillende bedrijven en gemeenschappen onder verschillende gratis licenties (BSD, MIT, Apache 2.0) op basis van de RISC-V-specificatie enkele tientallen varianten van reeds geproduceerde microprocessorkernen, SoC's en chips.
Ondersteuning voor RISC-V bestaat al sinds de uitgave van Glibc 2.27, binutils 2.30, gcc 7 en de Linux 4.15-kernel.
Over de seL4 microkernel-testen
Aanvankelijk was de microkernel seL4 is geverifieerd voor 32-bits ARM-processorsEn later voor x86 64-bits processors.
Opgemerkt wordt dat de combinatie van de RISC-V open hardware-architectuur met de open microkernel seL4 zal een nieuw beveiligingsniveau bereiken, aangezien toekomstige hardwarecomponenten ook volledig kunnen worden geverifieerd, wat onmogelijk is voor propriëtaire hardwarearchitecturen.
Wanneer we seL4 controleren, moeten we ervan uitgaan dat de hardware correct werkt (dwz zoals gespecificeerd). Dat veronderstelt in de eerste plaats dat er een eenduidige specificatie is, wat niet voor alle hardware het geval is.
Maar zelfs als een dergelijke specificatie bestaat, en deze is formeel (dat wil zeggen, ritten in een wiskundig formalisme dat wiskundig redeneren over zijn eigenschappen ondersteunt), hoe weten we dan dat deze het gedrag van de hardware daadwerkelijk vastlegt?
De realiteit is dat we er vrij zeker van kunnen zijn dat dit niet zo is. Hardware verschilt niet van software doordat beide bugs bevatten.
Maar het hebben van een open ISA heeft voordelen die verder gaan dan royaltyvrij zijn. Een daarvan is dat het open source hardware-implementaties mogelijk maakt.
Bij het controleren van seL4 wordt aangenomen dat de apparatuur werkt zoals aangegeven en dat de specificatie het gedrag van het systeem volledig beschrijft, maar in feite is de apparatuur niet foutloos, wat goed wordt aangetoond door problemen die regelmatig voorkomen in het speculatieve uitvoeringsmechanisme Instructies .
Open hardwareplatforms vereenvoudigen de integratie van wijzigingen met betrekking tot beveiliging, bijvoorbeeld om alle mogelijke lekkanalen via kanalen van derden te blokkeren, waarbij het veel efficiënter is om een probleem met hardware op te lossen dan om oplossingen te zoeken met software.
Als u er tenslotte meer over wilt weten, kunt u de notitie in het volgende link.
Voor mij is deze processor iets dat me veel oproept. Het blijft alleen voor een dikke computerhond om een computer te maken die we kunnen kopen.
Het ARM-probleem is iets dat me piept, je zag al wat er met Huawei is gebeurd met de sancties. Ik ben duidelijk dat het voor mijn RISC-V een veel betere oplossing is op alle niveaus. Op dit moment heeft Huawei het al in de gaten en wellicht zullen ze in de toekomst apparatuur hebben met deze micro. Als dat zo is, zullen er zeker meer bedrijven zijn die het adopteren en voor mij zou dat het ideaal zijn en vooral dat de distributies het ondersteunen en niet alleen ARM zoals het bij de meesten gebeurt.
+ 10