RISC-V, seL4 mikro çekirdeğini RV64 işlemcilerinde doğruladı

RISC-V Vakfı doğruladığını duyurdu mikro çekirdek nasıl çalışır seL4 ile sistemlerde komut seti mimarisi RISC-V. Doğrulama sürecinin, resmi bir dilde belirtilen şartnamelere tam uyumu gösteren SEL4'ün güvenilirliğinin matematiksel kanıtına indirgenmesi.

Güvenilirlik testi seL4'ün RISC-V işlemcilere dayalı kritik görev sistemlerinde kullanılmasını sağlar RV64daha yüksek düzeyde güvenilirlik gerektiren ve arızayı garanti etmeyen.

SEL4 çekirdeği üzerinde çalışan yazılım geliştiricileri, sistemin bir bölümünde bir arıza olması durumunda, bu arızanın sistemin geri kalanına ve özellikle kritik bölümlerine yayılmayacağından tamamen emin olabilirler. .

SeL4 hakkında

SeL4 mimarisi kullanıcı alanındaki çekirdek kaynaklarını yönetmek için parçaların kaldırılmasıyla dikkat çekicidir ve bu tür kaynaklar için kullanıcı kaynaklarıyla aynı erişim kontrol yöntemlerini kullanın.

Mikro çekirdek üst düzey soyutlamalar sağlamaz dosyaları, işlemleri, ağ bağlantılarını vb. yönetmek için zaten hazırlandı, ancak bunun yerine yalnızca fiziksel adres alanına erişimi kontrol etmek için minimum mekanizmalar sağlar, kesintiler ve işlemci kaynakları.

Bilgisayarla etkileşim için üst düzey soyutlamalar ve denetleyiciler, kullanıcı düzeyinde gerçekleştirilen görevler biçiminde mikro çekirdeğin üzerinde ayrı ayrı uygulanır.

Bu tür görevlerin mikro çekirdekte bulunan kaynaklara erişimi, kuralların tanımlanmasıyla düzenlenir.

RISC-V açık ve esnek bir sistem sağlar makine talimatlarının kesinti gerektirmeden rastgele uygulamalar için mikroişlemciler oluşturmaya izin verir ve kullanım koşulları empoze etmeden.

RISC-V, tamamen açık SoC'ler ve işlemciler oluşturmanıza olanak sağlar. Şu anda, RISC-V spesifikasyonu temelinde, çeşitli ücretsiz lisanslar (BSD, MIT, Apache 2.0) altında çeşitli şirketler ve topluluklar, halihazırda üretilmiş mikroişlemci çekirdekleri, SoC'ler ve yongaların birkaç düzine çeşidini geliştirmektedir.

RISC-V desteği, Glibc 2.27, binutils 2.30, gcc 7 ve Linux 4.15 çekirdeğinin piyasaya sürülmesinden bu yana var.

SeL4 mikro çekirdek testi hakkında

Başlangıçta mikro çekirdek seL4, 32 bit ARM işlemciler için doğrulandıVe x86 64 bit işlemciler için daha sonra.

RISC-V açık donanım mimarisinin açık mikro çekirdek ile kombinasyonunun seL4 yeni bir güvenlik düzeyine ulaşacakGelecekteki donanım bileşenleri de tam olarak doğrulanabildiğinden, bu, tescilli donanım mimarileri için elde edilmesi imkansızdır.

SeL4'ü kontrol ettiğimizde, donanımın düzgün çalıştığını (yani belirtildiği gibi) varsaymalıyız. Bu, ilk etapta, tüm donanımlar için geçerli olmayan, kesin bir spesifikasyon olduğunu varsayar. 

Ancak böyle bir belirtim var olduğunda ve biçimsel olduğunda (yani, özellikleri hakkında matematiksel akıl yürütmeyi destekleyen matematiksel bir biçimciliğe göre şekillendirilmiş) bile, donanımın davranışını gerçekten yakaladığını nereden biliyoruz? 

Gerçek şu ki, olmadığından oldukça emin olabiliriz. Donanım, her ikisinin de hatalı olması açısından yazılımdan farklı değildir.

Ancak açık bir ISA'ya sahip olmak, telifsiz olmanın ötesine geçen avantajlara sahiptir. Birincisi, açık kaynaklı donanım uygulamalarına izin vermesidir.

SEL4'ü kontrol ederken, ekipmanın belirtildiği gibi çalıştığı ve spesifikasyonun sistemin davranışını tam olarak tanımladığı varsayılır, ancak aslında ekipman hatasız değildir, bu da spekülatif yürütme mekanizmasında düzenli olarak ortaya çıkan problemlerle iyi bir şekilde gösterilmiştir. Talimatlar.

Açık donanım platformları, değişikliklerin entegrasyonunu basitleştirir güvenlikle ilgili, örneğin, olası tüm sızıntı kanallarını üçüncü taraf kanallar aracılığıyla bloke etmek, burada bir sorundan donanımla kurtulmanın yazılımla çözüm bulmaya çalışmaktan çok daha verimli olduğu.

Son olarak, hakkında daha fazla bilgi edinmek isterseniz, sayfadaki nota bakabilirsiniz. aşağıdaki bağlantı.