RISC-V Foundation iwwer d'Verifizéierung vun der Operatioun vum Mikrokernel op Systemer mat RISC-V Instruktiounsset Architektur. Verifikatioun kënnt erof op Zouverlässegkeet vun seL4 Operatioun, déi voll Konformitéit mat de Spezifikatioune an der formell Sprooch uginn. Beweis vun Zouverlässegkeet seL4 a Missiounskritesch Systemer baséiert op RISC-V RV64 Prozessoren déi e verstäerkte Zouverlässegkeet erfuerderen an d'Feele vu Feeler garantéieren. D'Entwéckler vu Software déi uewen um seL4 Kernel lafen, kënne ganz zouversiichtlech sinn datt wann et e Feeler an engem Deel vum System gëtt, gëtt dësen Echec net op de Rescht vum System verbreet a besonnesch seng kritesch Deeler.
De seL4 Mikrokernel gouf ufanks fir 32-Bit ARM Prozessoren verifizéiert, a spéider fir 64-Bit x86 Prozessoren. Et gëtt bemierkt datt d'Kombinatioun vun der oppener RISC-V Hardwarearchitektur mat dem oppene seL4 Mikrokernel en neie Sécherheetsniveau erreechen wäert, well d'Hardwarekomponenten och an der Zukunft voll verifizéiert kënne ginn, wat onméiglech ass fir propriétaire Hardwarearchitekturen z'erreechen.
Beim Verifizéierung vun seL4 gëtt ugeholl datt d'Ausrüstung funktionnéiert wéi uginn an d'Spezifikatioun beschreift d'Behuele vum System voll, awer an der Realitéit ass d'Ausrüstung net fräi vu Feeler, wat kloer bewisen gëtt duerch regelméisseg entstanen Probleemer am Mechanismus vun der spekulativer Ausféierung vun Uweisungen. Open Hardware Plattformen maachen et méi einfach d'Sécherheetsrelatéiert Ännerungen z'integréieren - zum Beispill fir all méiglech Säit-Kanal-Leaks ze blockéieren, wou et vill méi effizient ass de Problem an der Hardware lass ze ginn wéi ze probéieren Léisungen an der Software ze fannen.
Erënneren, datt d'seL4 Architektur bewegt Deeler fir d'Gestioun vun Kernelressourcen an de Benotzerraum an d'Applikatioun déiselwecht Zougangskontrollmëttel fir sou Ressourcen wéi fir Benotzerressourcen. De Mikrokernel bitt keng fäerdeg High-Level Abstraktioune fir d'Gestioun vun Dateien, Prozesser, Netzwierkverbindungen an dergläiche; amplaz bitt et nëmme minimal Mechanismen fir den Zougang zu kierperlechen Adressraum, Ënnerbriechungen a Prozessorressourcen ze kontrolléieren. Héichniveau Abstraktiounen a Chauffeuren fir mat Hardware interagéieren ginn separat uewen um Mikrokernel a Form vun User-Niveau Aufgaben ëmgesat. Den Zougang vun esou Aufgaben op d'Ressourcen, déi dem Mikrokernel verfügbar sinn, gëtt duerch d'Definitioun vu Regelen organiséiert.
RISC-V bitt en oppenen a flexibelen Maschinninstruktiounssystem deen et erlaabt datt Mikroprozessoren fir arbiträr Uwendungen gebaut ginn ouni Loyalitéiten oder Strings ze benotzen. RISC-V erlaabt Iech komplett oppe SoCs a Prozessoren ze kreéieren. De Moment baséiert op der RISC-V Spezifizéierung vu verschiddene Firmen a Gemeinschaften ënner verschiddene gratis Lizenzen (BSD, MIT, Apache 2.0) e puer Dosen Varianten vu Mikroprozessorkären, SoCs a scho produzéiert Chips. RISC-V Support ass präsent zënter de Verëffentlechunge vu Glibc 2.27, Binutils 2.30, gcc 7, an dem Linux Kernel 4.15.
Source: opennet.ru