AArch64 ko'rsatmalar to'plami arxitekturasiga ega tizimlarda seL4 mikroyadrosining ishonchliligi va xavfsizligini rasmiy matematik tekshirish bo'yicha ishlar yakunlandi. Tekshirish seL4 ishlashining to'g'riligini matematik isbotlashdan iborat bo'lib, bu rasmiy tilda belgilangan texnik xususiyatlarga to'liq muvofiqligini ko'rsatadi. Ishonchlilikning ushbu isboti yuqori darajadagi xavfsizlikni talab qiladigan va nosozliklar yo'qligini kafolatlaydigan ARM64 protsessorlariga asoslangan muhim tizimlarda seL4 dan foydalanish imkonini beradi.
seL4 mikroyadrosi dastlab 32-bitli ARM protsessorlari uchun, keyinchalik esa 64-bitli x86 va RISC-V protsessorlari uchun tekshirildi. Tekshirish tizimning bir qismida nosozlik yuzaga kelsa, u tizimning qolgan qismiga va uning muhim komponentlariga tarqalmasligini ta'minlaydi. Xavfsizlik nuqtai nazaridan, tekshirish yadro tegishli darajadagi ilovalarni izolyatsiya qilishini, ularning avtorizatsiyasiz ma'lumotlarga kirishiga to'sqinlik qilishini va ikkilamchi ilovalar buzilgan taqdirda hujum muhim ilovalarga tarqalmasligini ta'minlaydi.
seL4 mikroyadrosi arxitekturasi yadro resurslarini foydalanuvchi maydoniga boshqarish uchun qismlarni ko'chirish va foydalanuvchi resurslari kabi resurslarga kirishni boshqarish vositalaridan foydalanish bilan ajralib turadi. Mikroyadro fayllarni, jarayonlarni, tarmoq ulanishlarini va shunga o'xshashlarni boshqarish uchun tayyor yuqori darajadagi abstraktsiyalarni ta'minlamaydi, aksincha, u jismoniy manzil maydoniga, uzilishlar va protsessor resurslariga kirishni boshqarishning minimal mexanizmlarini taqdim etadi. Yuqori darajadagi abstraktsiyalar va apparat bilan o'zaro ta'sir qilish uchun drayverlar foydalanuvchi darajasidagi vazifalar shaklida mikroyadroning tepasida alohida amalga oshiriladi. Bunday vazifalarning mikroyadroda mavjud bo'lgan resurslarga kirishi qoidalarni aniqlash orqali tashkil etiladi.
Manba: opennet.ru
