seL4 mikroçekirdeğine giriş [PDF]

• seL4, çekirdek modunu en az miktarda kodla çalıştırarak donanım kaynaklarını kontrol eden ve güvenliği güçlendiren bir OS mikroçekirdeğidir
• L4 mikroçekirdek ailesine dahildir ve 1990'ların ortalarından beri geliştirilmektedir
• Hypervisor olarak çalışabildiği için Linux gibi misafir OS'lerin çalıştırılmasını destekler
• Dünyada işlevsel doğruluğu kanıtlanan ilk OS çekirdeğidir; kod düzeyinde matematiksel ispat tamamlanmıştır
• İnce taneli erişim denetimi için Capability tabanlı güvenlik modeli kullanır

seL4'ün yapısı ve hypervisor işlevi

• Monolithic kernel vs microkernel
  • Monolithic kernel (Linux vb.): Çekirdek kodu çok büyüktür, bu da daha fazla güvenlik açığı anlamına gelir → yaklaşık 20 milyon satır kod (20M SLOC)
  • Microkernel (seL4): En az miktarda çekirdek kodu kullanır → yaklaşık 10 bin satır kod (10K SLOC)
  • Çekirdek boyutunun küçülmesi → daha güçlü güvenlik ve daha küçük saldırı yüzeyi
• seL4 hypervisor rolünü üstlenir
  • VM içinde Linux gibi tam teşekküllü misafir OS'ler çalıştırılabilir
  • Her VM bağımsız olarak çalışır ve birbirini etkileyemez → güçlü yalıtım sağlar
  • Korumalı prosedür çağrısı (PPC) → VM'ler arasında güvenli iletişim mümkündür

seL4'ün doğrulaması ve güvenlik modeli

• İşlevsel doğruluk doğrulaması
  • seL4'ün işlevlerinin kod düzeyinde matematiksel olarak doğru olduğu kanıtlanmıştır
  • Çekirdeğin tüm davranışlarının belirtime uygun çalıştığını garanti eder
• Translation Validation
  • Derleyicinin ürettiği ikili kodun orijinal C koduyla tam olarak eşleştiği kanıtlanır
  • Otomatik araç zinciri üzerinden yürütülür
• Güvenlik özelliklerinin doğrulanması
  • Gizlilik: Veriye yalnızca açıkça izin verildiğinde erişilebilir
  • Bütünlük: Veri yalnızca açıkça izin verildiğinde değiştirilebilir
  • Kullanılabilirlik: Kaynaklar yalnızca açıkça izin verildiğinde kullanılabilir

Capability tabanlı güvenlik modeli

• Capability nedir?
  • Belirli bir nesneye erişim yetkisi veren bir güvenlik belirtecidir
  • Nesne referansı ile erişim haklarını birlikte kodlar
  • Ayrıntılı erişim denetimi mümkündür → en az ayrıcalık ilkesi (Principle of Least Privilege, POLA) uygulanır
• Capability'nin avantajları
  • İnce taneli erişim denetimi → yetkiler en aza indirilebilir
  • Yetki devri (Delegation) ve yetki iptali mümkündür
  • Güçlü güvenlik modeli → geleneksel erişim denetim modellerinden (ACL) daha üstündür
• Confused deputy sorununu çözer
  • Geleneksel ACL tabanlı sistemlerde güvenlik durumu, öznenin güvenlik kimliğine göre belirlenir
  • seL4'te güvenlik yetkilerini doğrudan Capability belirler → açık ve net yetki denetimi sağlanır

Gerçek zamanlı sistemler ve karma kritiklik düzeyine sahip sistem desteği

• Gerçek zamanlı sistem desteği
  • seL4, öncelik tabanlı zamanlamayı destekler
  • Tüm çekirdek işlemleri için en kötü durum yürütme süresi (WCET) analizi tamamlanmıştır → hard real-time garantisi
• Karma kritiklik düzeyine sahip sistemler (Mixed-Criticality System, MCS) desteği
  • CPU kaynakları, scheduling context temelinde tahsis edilir ve yalıtılır
  • Yüksek öncelikli görevlerin CPU'yu tek başına işgal etmemesi kontrol edilir
  • Kritik ve kritik olmayan görevler aynı anda çalıştırılabilir

Performans ve verimlilik

• En yüksek performanslı mikroçekirdek
  • Performansın önemli olduğu durumlarda bile güvenlikten ödün vermez
  • Sistem çağrısı ve IPC maliyeti en aza indirilmiştir → rakip sistemlere kıyasla 5 kattan fazla daha hızlıdır
• Rakip sistemlere kıyasla üstün performans
  • Fiasco.OC: seL4'ten yaklaşık 2 kat daha yavaş
  • Zircon: seL4'ten yaklaşık 9 kat daha yavaş
  • CertiKOS: seL4'ten yaklaşık 5 kat daha yavaş

Gerçek dünya uygulamaları ve siber retrofit

• Gerçek kullanım örnekleri

  • Boeing'in ULB'sinde (insansız helikopter) başarıyla uygulanmıştır
  • Güvenliğin güçlendiği ve sistem kararlılığının arttığı doğrulanmıştır

• Mevcut sistemlerin kademeli olarak güvenlik açısından güçlendirilmesi (Incremental Cyber Retrofit)

  • Mevcut sistemler VM içinde çalıştırılırken kademeli olarak modüler hale getirilir
  • Güvenlik artırılırken performans kaybı en aza indirilir

Sonuç

• seL4, işlevsel doğruluğu, güvenliği ve performansı kanıtlanmış, dünyadaki en güvenli mikroçekirdeklerden biridir
• Doğrulanmış güvenlik modeli ve karma kritiklik düzeyine sahip sistem desteği sayesinde birçok alanda pratik olarak kullanılabilir
• Mevcut sistemlerin güvenliğini artırma ve performansını iyileştirme imkanı sunar → güvenlik ile performans arasında denge kuran yenilikçi bir mikroçekirdektir