seL4
Daha fazla bilgi
- Oluşturan
- NICTA (şimdiki CSIRO Data61)
- Yayın
- Tür
- Mikroçekirdek
- Lisans
- GPLv2
- Resmî site
- sel4.systems
L4 ailesinden bir mikroçekirdek; C kodunun belirtimin söylediğini tam olarak yaptığına dair makineyle denetlenmiş bir kanıtı var.
Avustralya’daki NICTA ekibi kanıtı 2009’da yayımladı: yaklaşık 8.700 satır C kodu, biçimsel bir belirtime karşı Isabelle/HOL kanıt asistanında doğrulandı. Yaklaşık 20 kişi-yıl sürdü — yani kodu yazmak için gereken emeğin yirmi katı. Sonraki kanıtlar derlenmiş ikilinin kaynakla eşleştiğini ve çekirdeğin bileşenler arasındaki yalıtımı zorunlu kıldığını gösterdi.
Çekirdeğin kendisi neredeyse hiçbir şey yapmaz — iş parçacıkları, adres uzayları, IPC ve yetenekler (capabilities) — geri kalan her şey yalıtılmış kullanıcı seviyesi süreçler olarak çalışır. Bu, bir hatanın doğrulamadan daha pahalıya geldiği sistemlere uygundur: DARPA’nın HACMS programında, bir kırmızı takımın ele geçirmeyi başaramadığı insansız bir helikopterde uçtu. Kod 2014’te açık kaynak yapıldı.