Il microkernel seL4 è matematicamente verificato per l'architettura RISC-V
L'organizzazione RISC-V Foundation ha annunciato la verifica del funzionamento del microkernel seL4 su sistemi con architettura di set di istruzioni RISC-V. La verifica consiste in una dimostrazione matematica dell'affidabilità del funzionamento di seL4, che testimonia la piena conformità alle specifiche definite in un linguaggio formale. La dimostrazione dell'affidabilità consente l'uso di seL4 in sistemi critici basati su processori RISC-V RV64, che richiedono un elevato livello di affidabilità e garantiscono l'assenza di […]
