A RISC-V ellenőrizte a seL4 mikrokernelt RV64 processzoraikon

A RISC-V Alapítvány bejelentette, hogy ellenőrizte hogyan működik a mikrokernel seL4 a rendszerekkel az utasításkészlet architektúrája RISC-V. Ennek során az ellenőrzési folyamat a seL4 megbízhatóságának matematikai tesztjére redukálódik, amely azt jelzi, hogy teljes mértékben megfelelnek a hivatalos nyelven megadott előírásoknak.

A megbízhatósági teszt lehetővé teszi a seL4 használatát a RISC-V processzorokon alapuló, kritikus fontosságú rendszerekben RV64, amely magasabb szintű megbízhatóságot igényel és nem garantálja a kudarcot.

A seL4 kernel tetején futó szoftverfejlesztők teljesen biztosak lehetnek abban, hogy a rendszer egyik részének meghibásodása esetén ez a hiba nem terjed át a rendszer többi részére és különösen annak kritikus részeire. .

A seL4-ről

A seL4 architektúra figyelemre méltó az alkatrészek eltávolításával a rendszermag erőforrásainak kezeléséhez a felhasználói térben és ugyanazokat a hozzáférés-vezérlési módszereket használja az ilyen erőforrásokhoz, mint a felhasználói erőforrásokhoz.

A mikrokernel nem nyújt magas szintű absztrakciókat már felkészült a fájlok, folyamatok, hálózati kapcsolatok stb. kezelésére, de ehelyett csak minimális mechanizmusokat biztosít a fizikai címtérhez való hozzáférés ellenőrzésére, megszakítja és a processzor erőforrásait.

A számítógéppel való interakcióhoz szükséges magas szintű absztrakciókat és vezérlőket külön megvalósítják a mikrorendszer tetején, felhasználói szinten végrehajtott feladatok formájában.

Az ilyen feladatok hozzáférését a mikrokernelben elérhető erőforrásokhoz a szabályok meghatározása határozza meg.

A RISC-V nyílt és rugalmas rendszert biztosít a gépi utasítások közül lehetővé teszi mikroprocesszorok létrehozását tetszőleges alkalmazásokhoz, levonások nélkül és a felhasználási feltételek előírása nélkül.

A RISC-V lehetővé teszi teljesen nyitott processzorok és SoC-k létrehozását. Jelenleg a RISC-V specifikáció alapján több vállalat és közösség különféle ingyenes licencek (BSD, MIT, Apache 2.0) alapján a már gyártott mikroprocesszoros magok, SoC-k és chipek több tucat változatát fejleszti.

A RISC-V támogatás a Glibc 2.27, a binutils 2.30, a gcc 7 és a Linux 4.15 kernel kiadása óta létezik.

A seL4 mikrokernel teszteléséről

Kezdetben a mikrokernel A seL4-et 32 ​​bites ARM processzoroknál ellenőrizték, És később x86 64 bites processzorokhoz.

Megfigyelték, hogy a RISC-V nyílt hardverarchitektúra és a nyílt mikrokernel kombinációja A seL4 új biztonsági szintet fog elérni, mivel a jövőben a hardverkomponensek is teljes mértékben ellenőrizhetők, amit a saját fejlesztésű hardverarchitektúrák esetében lehetetlen elérni.

A seL4 ellenőrzésénél feltételeznünk kell, hogy a hardver megfelelően működik (vagyis a megadott módon). Ez feltételezi, hogy elsősorban egyértelmű specifikáció van, ami nem minden hardver esetében áll fenn. 

De még akkor is, ha létezik ilyen specifikáció, és formális (vagyis matematikai formalizmussá alakítva, amely támogatja a tulajdonságainak matematikai érvelését), honnan tudjuk, hogy valóban megragadja a hardver viselkedését? 

A valóság az, hogy egészen biztosak lehetünk abban, hogy nem az. A hardver abban nem különbözik a szoftvertől, hogy mindkettő hibás.

De a nyitott ISA-nak vannak olyan előnyei, amelyek túlmutatnak a jogdíjmentességen. Az egyik az, hogy lehetővé teszi a nyílt forráskódú hardveres megvalósításokat.

A seL4 ellenőrzésénél feltételezzük, hogy a berendezés az előírt módon működik, és a specifikáció teljes mértékben leírja a rendszer viselkedését, de valójában a berendezés nem hibamentes, amit jól mutatnak a spekulatív végrehajtási mechanizmusban rendszeresen felmerülő problémák Utasítás.

A nyílt hardverplatformok egyszerűsítik a változások integrálását a biztonsághoz kapcsolódóan például az összes lehetséges szivárgási csatorna blokkolása harmadik féltől származó csatornákon keresztül, ahol sokkal hatékonyabb hardvertől megszabadulni a problémától, mint szoftveresen megoldásokat keresni.

Végül, ha többet szeretne megtudni róla, olvassa el a jegyzetet a következő link.