Mikrojehë seL4 e verifikuar matematikisht për arkitekturën RISC-V
Organizata RISC-V Foundation njoftoi verifikimin e funksionimit të mikroarkitekturës seL4 në sisteme me arkitekturën e setit të komandave RISC-V. Verifikimi përmbledh provimin matematikor të besueshmërisë së funksionimit të seL4, i cili vërteton përputhjen e plotë me specifikimet e caktuara në një gjuhë formale. Prova e besueshmërisë lejon përdorimin e seL4 në sisteme kritike të bazuara në procesorët RISC-V RV64, që kërkojnë një nivel të lartë besueshmërie dhe garantojnë mungesën e […]
