A fost efectuată o verificare formală a securității microkernelului seL4 pentru arhitectura AArch64
S-a încheiat lucrul la verificarea formală matematică a fiabilității și securității microkernel-ului seL4 pe sisteme cu arhitectură de seturi de comenzi AArch64. Verificarea se reduce la o dovadă matematică a corectitudinii funcționării seL4, care atestă conformitatea completă cu specificațiile date într-un limbaj formal. Dovada fiabilității permite utilizarea seL4 în sisteme critice bazate pe procesoare ARM64, care necesită un nivel sporit de securitate și […]
