RISC-V Fondu mikrokernelin işini yoxlamaq haqqında RISC-V təlimat dəsti arxitekturasına malik sistemlərdə. Doğrulama aşağı düşür seL4 əməliyyatının etibarlılığı, rəsmi dildə göstərilən spesifikasiyalara tam uyğunluğunu göstərir. Etibarlılığın sübutu seL4, artan etibarlılıq səviyyəsini tələb edən və nasazlıqların olmamasını təmin edən RISC-V RV64 prosessorlarına əsaslanan kritik sistemlərdə. seL4 nüvəsinin üstündə işləyən proqram təminatının tərtibatçıları tam əmin ola bilərlər ki, sistemin bir hissəsində nasazlıq olarsa, bu nasazlıq sistemin qalan hissəsinə və xüsusən də onun kritik hissələrinə yayılmayacaq.
seL4 mikrokerneli əvvəlcə 32 bitlik ARM prosessorları, daha sonra isə 64 bitlik x86 prosessorları üçün yoxlanıldı. Qeyd olunur ki, açıq RISC-V aparat arxitekturasının açıq seL4 mikrokerneli ilə birləşməsi yeni təhlükəsizlik səviyyəsinə nail olacaq, çünki gələcəkdə aparat komponentləri də tam yoxlanıla bilər ki, buna özəl aparat arxitekturaları üçün nail olmaq mümkün deyil.
SeL4-ü yoxlayarkən, avadanlığın göstərildiyi kimi işlədiyi və spesifikasiyanın sistemin davranışını tam təsvir etdiyi güman edilir, lakin əslində avadanlıq səhvlərdən azad deyildir, bu, spekulyativ icra mexanizmində müntəzəm olaraq ortaya çıxan problemlər tərəfindən aydın şəkildə nümayiş etdirilir. təlimatlar. Açıq aparat platformaları təhlükəsizliklə bağlı dəyişiklikləri inteqrasiya etməyi asanlaşdırır - məsələn, bütün mümkün yan kanal sızmalarını bloklamaq, burada proqram təminatında həll yollarını tapmaqdansa, aparatdakı problemdən xilas olmaq daha səmərəlidir.
Xatırladaq ki, seL4 arxitekturası kernel resurslarını istifadəçi məkanına idarə etmək üçün hissələrin hərəkəti və istifadəçi resursları üçün olduğu kimi resurslar üçün eyni girişə nəzarət vasitələrinin tətbiqi. Mikrokernel faylları, prosesləri, şəbəkə bağlantılarını və sairləri idarə etmək üçün hazır yüksək səviyyəli abstraksiyaları təmin etmir, bunun əvəzinə o, fiziki ünvan məkanına, kəsilmələrə və prosessor resurslarına girişi idarə etmək üçün yalnız minimal mexanizmləri təmin edir. Yüksək səviyyəli abstraksiyalar və hardware ilə qarşılıqlı əlaqə üçün drayverlər istifadəçi səviyyəsində tapşırıqlar şəklində mikro nüvənin üstündə ayrıca həyata keçirilir. Bu cür tapşırıqların mikrokerneldə mövcud olan resurslara çıxışı qaydaların müəyyən edilməsi yolu ilə təşkil edilir.
RISC-V açıq və çevik maşın təlimat sistemini təmin edir ki, bu da istifadə üçün əlavə ödəniş və ya sətir tələb etmədən ixtiyari proqramlar üçün mikroprosessorların qurulmasına imkan verir. RISC-V sizə tamamilə açıq SoC və prosessorlar yaratmağa imkan verir. Hal-hazırda müxtəlif pulsuz lisenziyalar (BSD, MIT, Apache 2.0) altında müxtəlif şirkətlər və icmalar tərəfindən RISC-V spesifikasiyasına əsaslanır. mikroprosessor nüvələrinin, SoC-lərin və artıq istehsal edilmiş çiplərin bir neçə onlarla variantı. RISC-V dəstəyi Glibc 2.27, binutils 2.30, gcc 7 və Linux nüvəsi 4.15 buraxılışlarından bəri mövcuddur.
Mənbə: opennet.ru