RISC-V Vakfı mikro çekirdeğin çalışmasını doğrulama hakkında RISC-V komut seti mimarisine sahip sistemlerde. Doğrulama şuraya gelir: resmi dilde belirtilen spesifikasyonlara tam uyumu gösteren seL4 işleminin güvenilirliği. Güvenilirlik kanıtı Daha yüksek düzeyde güvenilirlik gerektiren ve arıza yokluğunu garanti eden RISC-V RV4 işlemcilerini temel alan kritik görev sistemlerinde seL64. 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 de kritik parçalarına yayılmayacağından tamamen emin olabilirler.
SeL4 mikro çekirdeği başlangıçta 32 bit ARM işlemciler için ve daha sonra 64 bit x86 işlemciler için doğrulandı. Açık RISC-V donanım mimarisinin açık seL4 mikro çekirdeği ile kombinasyonunun, donanım bileşenlerinin gelecekte tamamen doğrulanabileceğinden, özel donanım mimarileri için bunu başarmanın imkansız olması nedeniyle yeni bir güvenlik düzeyi elde edeceği belirtiliyor.
SeL4 doğrulanırken, ekipmanın belirtildiği gibi çalıştığı ve spesifikasyonun sistemin davranışını tam olarak tanımladığı varsayılır, ancak gerçekte ekipman hatalardan arınmış değildir; bu, spekülatif uygulama mekanizmasında düzenli olarak ortaya çıkan problemlerle açıkça gösterilmiştir. talimatlar. Açık donanım platformları, güvenlikle ilgili değişiklikleri entegre etmeyi kolaylaştırır; örneğin, tüm olası yan kanal sızıntılarını engellemek için; donanımdaki sorundan kurtulmanın, yazılımda geçici çözümler bulmaya çalışmaktan çok daha verimli olduğu durumlarda.
seL4 mimarisini hatırlayın çekirdek kaynaklarını yönetmeye yönelik parçaları kullanıcı alanına taşımak ve bu tür kaynaklar için kullanıcı kaynakları için olduğu gibi aynı erişim kontrolü araçlarını uygulamak. Mikro çekirdek, dosyaları, işlemleri, ağ bağlantılarını ve benzerlerini yönetmek için hazır üst düzey soyutlamalar sağlamaz; bunun yerine, fiziksel adres alanına, kesintilere ve işlemci kaynaklarına erişimi kontrol etmek için yalnızca minimum mekanizmalar sağlar. Donanımla etkileşime yönelik üst düzey soyutlamalar ve sürücüler, kullanıcı düzeyinde görevler biçiminde mikro çekirdeğin üzerinde ayrı olarak uygulanır. Bu tür görevlerin mikro çekirdeğin kullanabileceği kaynaklara erişimi, kuralların tanımlanması yoluyla düzenlenir.
RISC-V, mikroişlemcilerin telif ücreti veya kullanım için ek süreler gerektirmeden keyfi uygulamalar için oluşturulmasına olanak tanıyan açık ve esnek bir makine talimat sistemi sağlar. RISC-V tamamen açık SoC'ler ve işlemciler oluşturmanıza olanak tanır. Şu anda çeşitli ücretsiz lisanslar (BSD, MIT, Apache 2.0) kapsamında farklı şirketler ve topluluklar tarafından RISC-V spesifikasyonuna dayanmaktadır. birkaç düzine mikroişlemci çekirdeği çeşidi, SoC'ler ve halihazırda üretilmiş çipler. RISC-V desteği Glibc 2.27, binutils 2.30, gcc 7 ve Linux çekirdeği 4.15 sürümlerinden beri mevcuttur.
Kaynak: opennet.ru