Den australiska buggfria mikrokärnan SEL4 kan nu köras på RISC-V-processorer. Implementeringen är öppen källkod och kommer från den australiska forskningsorganisationen Csiro och University of New South Wales.
Hypervisorn och mikrokärnan SEL4 kan köras på 64-bitars RISC-V. Du kan testa den i CPU-simulatorn Spike. Det som saknas är stöd för flyttal.
Också processorarkitekturen RISC-V skyddas av en öppenkodslicens. Du kan implementera den, tillverka den och modifiera den utan att be någon om lov och utan att behöva betala pengar till någon.
Det finns en spännande poäng med att kombinationen av SEL4 och RISC-V är öppen källkod. Det betyder att den är mycket öppen för säkerhetsgranskning. Vem som helst kan undersöka om den innehåller bakdörrar, eller om det finns säkerhetshål av typen Meltdown eller Spectre.
SEL4 stöds sedan tidigare på ARM- och X86-processorer. Den används bland annat i Apple Iphone i implementationen av säkerhets-coprocessorn Security Enclave Security Coprocessor i de senaste modellerna.
Buggfri? Jo, det är bevisat faktiskt. En av nyckelpersonerna bakom SEL4 – professor Gernot Heiser – beskrev beviset i en artikel i Elektroniktidningen år 2010.
Kretsar med RISC-V har släpps eller kommer att släppas av bland annat SiFive och Greenwaves. Hårddisktillverkaren Western Digital är den som gått längst med att använde den kommersiellt. Företaget kommer snart att ha en årlig tillverkning av kretsar med sammanlagt en miljard RISC-V-kärnor.
Csiro tar plats i styrelsen för RISC-V-stiftelsen, bland annat för att bevaka att SEL4 får ett bra stöd i kommande versioner av RISC-V.