Mikrojadro seL4 matematicky verifikované pre architektúru RISC-V
Organizácia RISC-V Foundation oznámila overenie fungovania mikrojadra seL4 na systémoch s architektúrou sady príkazov RISC-V. Overenie spočíva v matematickom dôkaze spoľahlivosti fungovania seL4, ktorý potvrdzuje úplnú zhodu s požiadavkami zadávanými vo formálnych špecifikáciách. Dôkaz spoľahlivosti umožňuje využívať seL4 v kritických systémoch na báze procesorov RISC-V RV64, ktoré si vyžadujú zvýšenú úroveň spoľahlivosti a garantujú absenciu […]
