RISC-V o'zlarining RV4 protsessorlarida seL64 mikrokernelini tekshirdi

RISC-V Foundation tasdiqlanganligini e'lon qildi mikrokernel qanday ishlaydi tizimlarida seL4 ko'rsatmalar to'plami arxitekturasi RISC-V. Bunda tekshirish jarayoni seL4 ishonchliligining matematik isbotiga tushiriladi, bu rasmiy tilda ko'rsatilgan xususiyatlarga to'liq mos kelishini ko'rsatadi.

Ishonchlilik testi seL4-ni RISC-V protsessorlariga asoslangan muhim tizimlarda ishlatishga imkon beradi RV64, bu yuqori darajadagi ishonchlilikni talab qiladi va muvaffaqiyatsizlikka kafolat bermaydi.

SeL4 yadrosi ustida ishlaydigan dasturiy ta'minot ishlab chiqaruvchilari tizimning bir qismida nosozlik yuz berganda, bu nosozlik tizimning qolgan qismiga va xususan, uning muhim qismlariga tarqalmasligiga to'liq ishonishlari mumkin.

SeL4 haqida

SeL4 arxitekturasi foydalanuvchi makonidagi yadro resurslarini boshqarish uchun qismlarni olib tashlash bilan ajralib turadi va foydalanuvchi resurslari singari bunday manbalar uchun kirish huquqini boshqarish usullaridan foydalaning.

Mikrokernel yuqori darajadagi abstraktlarni taqdim etmaydi allaqachon fayllarni, jarayonlarni, tarmoq ulanishlarini va boshqalarni boshqarish uchun tayyorlangan, ammo buning o'rniga faqat jismoniy manzil maydoniga kirishni boshqarish uchun minimal mexanizmlarni taqdim etadi, uzilishlar va protsessor resurslari.

EHM bilan ishlash uchun yuqori darajadagi abstraktlar va kontrollerlar mikrokernelning yuqori qismida foydalanuvchi darajasida bajariladigan vazifalar shaklida alohida amalga oshiriladi.

Bunday vazifalarning mikrokernelda mavjud bo'lgan resurslarga kirishi qoidalarni aniqlash orqali tashkil etiladi.

RISC-V ochiq va moslashuvchan tizimni taqdim etadi mashina ko'rsatmalari ajratmalar talab qilmasdan, o'zboshimchalik bilan ishlaydigan dasturlar uchun mikroprotsessorlarni yaratishga imkon beradi va foydalanish shartlarini belgilamasdan.

RISC-V sizga to'liq ochiq protsessorlar va SoClarni yaratishga imkon beradi. Hozirgi vaqtda RISC-V spetsifikatsiyasi asosida turli xil bepul litsenziyalarga ega bo'lgan bir nechta kompaniyalar va jamoalar (BSD, MIT, Apache 2.0) allaqachon ishlab chiqarilgan mikroprotsessor yadrolari, SoC va chiplarning o'nlab variantlarini ishlab chiqmoqdalar.

RISC-V-ni qo'llab-quvvatlash Glibc 2.27, binutils 2.30, gcc 7 va Linux 4.15 yadrosi chiqarilgandan beri mavjud.

SeL4 mikrokernel sinovi haqida

Dastlab mikrokernel seL4 32 bitli ARM protsessorlari uchun tasdiqlanganva keyinchalik x86 64 bitli protsessorlar uchun.

RISC-V ochiq apparat arxitekturasining ochiq mikrokernel bilan kombinatsiyasi kuzatilmoqda seL4 yangi darajadagi xavfsizlikka erishadichunki kelajakda apparat tarkibiy qismlari ham to'liq tekshirilishi mumkin, bunga mulkiy apparat me'morchiligi uchun erishish mumkin emas.

Biz seL4-ni tekshirganimizda, uskuna to'g'ri ishlamoqda deb taxmin qilishimiz kerak (ya'ni ko'rsatilganidek). Bu birinchi navbatda aniq texnik xususiyat mavjudligini taxmin qiladi, bu barcha qo'shimcha qurilmalarda mavjud emas. 

Ammo bunday spetsifikatsiya mavjud bo'lsa ham va u rasmiy bo'lsa (ya'ni uning xususiyatlari haqida matematik fikr yuritishni qo'llab-quvvatlaydigan matematik formalizmga aylangan bo'lsa) ham, u aslida apparatning xatti-harakatlarini ushlab turishini qaerdan bilamiz? 

Haqiqat shundaki, biz bunday emasligiga amin bo'lishimiz mumkin. Apparatlarning dasturiy ta'minotdan farqi yo'q, chunki ikkalasi ham buggy.

Ammo ochiq ISAga ega bo'lish, royalti olishdan tashqari afzalliklarga ega. Ulardan biri ochiq manbali apparatni amalga oshirishga imkon beradi.

SeL4-ni tekshirganda, uskunalar ko'rsatilganidek ishlaydi va spetsifikatsiya tizimning ishlashini to'liq tavsiflaydi, deb o'ylashadi, lekin aslida uskunalar xatosiz emas, bu spekulyativ ijro mexanizmida muntazam ravishda yuzaga keladigan muammolar bilan yaxshi namoyon bo'ladi. .

Ochiq apparat platformalari o'zgarishlar integratsiyasini soddalashtiradi xavfsizlik bilan bog'liq, masalan, uchinchi tomon kanallari orqali barcha mumkin bo'lgan qochqin kanallarini blokirovka qilish, bu erda dasturiy ta'minot yordamida echimlarni topishga qaraganda, qo'shimcha qurilmalar yordamida muammodan xalos bo'lish ancha samarali.

Va nihoyat, agar siz bu haqda ko'proq bilmoqchi bo'lsangiz, undagi yozuvga murojaat qilishingiz mumkin quyidagi havola.


Maqolaning mazmuni bizning printsiplarimizga rioya qiladi muharrirlik etikasi. Xato haqida xabar berish uchun bosing bu erda.

2 ta sharh, o'zingizni qoldiring

Fikringizni qoldiring

Sizning email manzilingiz chop qilinmaydi.

*

*

  1. Ma'lumotlar uchun javobgardir: Migel Anxel Gaton
  2. Ma'lumotlarning maqsadi: SPAMni boshqarish, izohlarni boshqarish.
  3. Qonuniylashtirish: Sizning roziligingiz
  4. Ma'lumotlar haqida ma'lumot: qonuniy majburiyatlar bundan mustasno, ma'lumotlar uchinchi shaxslarga etkazilmaydi.
  5. Ma'lumotlarni saqlash: Occentus Networks (EU) tomonidan joylashtirilgan ma'lumotlar bazasi
  6. Huquqlar: istalgan vaqtda siz ma'lumotlaringizni cheklashingiz, tiklashingiz va o'chirishingiz mumkin.

  1.   ba'zilaridan biri dijo

    Men uchun bu protsessor meni juda ko'p chaqiradigan narsa. Biz sotib oladigan kompyuterni yasash ba'zi bir semiz kompyuter itlarida qoladi.

    ARM muammosi meni siqib chiqaradigan narsa, siz Huawei bilan sanksiyalar bilan nima bo'lganini allaqachon ko'rgansiz. Mening RISC-V uchun bu barcha darajalarda juda yaxshi echim ekanligiga aminman. Ayni paytda Huawei allaqachon unga e'tibor qaratgan va ehtimol kelajakda ularda ushbu mikroelektron uskunalar bo'ladi. Agar shunday bo'lsa, shubhasiz, uni qabul qiladigan ko'plab kompaniyalar bo'ladi va men uchun bu eng maqbul va eng avvalo tarqatish nafaqat ARMni qo'llab-quvvatlaydigan, balki aksariyat hollarda bo'lgani kabi.

    1.    Gregori ros dijo

      + 10