seL4 mikro çekirdeğine giriş [PDF]

 (sel4.systems)
1 puan yazan GN⁺ 2025-03-24 | 1 yorum | WhatsApp'ta paylaş
  • seL4, güvenlik ve emniyetin kritik olduğu gömülü ve siber-fiziksel sistemleri hedefleyen bir OS mikro çekirdeğidir; donanım kaynaklarını yalıtır ve çoğullar, ancak tam kapsamlı genel amaçlı bir OS değildir
  • Kernel mode kodunu yaklaşık 10 kSLOC düzeyine indirerek TCB’yi ve saldırı yüzeyini küçültür; dosya sistemi, ağ ve sürücüler gibi OS servislerini user mode’a taşır
  • Kod düzeyinde biçimsel doğrulamaya sahip dünyanın ilk OS çekirdeğidir; doğru yapılandırılmış sistemlerde kernel, gizlilik, bütünlük ve kullanılabilirlik gibi güvenlik özelliklerini de garanti eder
  • Capability tabanlı erişim denetimi, WCET analizi, karma kritiklikte gerçek zamanlı sistem desteği ve hypervisor işlevlerini bir araya getirerek ince taneli yalıtımı ve gerçek zamanlılığı birlikte ele alır
  • seL4 API’si çok düşük seviyelidir; bu yüzden karmaşık sistemleri doğrudan inşa etmek zordur. Statik mimarinin uygun olduğu durumlarda Microkit gibi framework’leri kullanmak gerçekçi yaklaşımdır

seL4’ün üstlendiği kapsam

  • seL4, işletim sisteminin düşük seviyeli çekirdek bölümü olan bir mikro çekirdektir
    • OS, işlemcinin daha yüksek ayrıcalıklı çalışma modu olan kernel mode içinde donanımı ve kaynakları kontrol eder
    • Uygulamalar user mode’da çalışır ve donanıma yalnızca OS’nin izin verdiği biçimde erişir
  • Mikro çekirdek, yüksek ayrıcalıkla çalışan kodu en aza indiren OS çekirdeğidir
    • seL4, kökleri 1990’ların ortasına uzanan L4 mikro çekirdek ailesine dahildir
    • seL4’ün seLinux ile ilgisi yoktur
  • seL4 tam kapsamlı bir OS değil, donanım kaynaklarını güvenli biçimde çoğullayan ve yalıtan düşük seviyeli bir çekirdektir
    • Dosya sistemi, ağ stack’i, aygıt sürücüleri gibi sıradan OS servisleri kernel’in içinde yer almaz
    • Bu servislerin user mode programları olarak sağlanması gerekir

Mikro çekirdek yapısı ve saldırı yüzeyinin küçültülmesi

  • Linux gibi monolitik kernel’ler dosya depolama ve ağ gibi OS servislerini kernel mode kodu olarak sunar
    • Kernel mode kodu sistem kaynaklarına sınırsız erişebilir; bu nedenle bir hata yetki yükseltmeye veya keyfi kod çalıştırmaya yol açarsa tüm sistem zarar görebilir
    • Linux kernel’i yaklaşık 20 MSLOC büyüklüğündedir ve on binlerce hata içerebileceği tahmin edilir
  • seL4 gibi iyi tasarlanmış bir mikro çekirdek, kernel mode kodunu yaklaşık 10 kSLOC seviyesine indirir
    • Bu, Linux kernel’inden üç basamak mertebesinde daha küçüktür
    • TCB küçüldükçe saldırı yüzeyi de birlikte küçülür
  • OS servislerinin çoğu kernel’in dışına çıkarılır ve mikro çekirdek, donanımın etrafındaki ince bir wrapper gibi davranır
    • Sağlanan temel işlevler, programlar arası yalıtım ve güvenli çağrı mekanizmasıdır
    • Servisler kernel içinde değil, ayrı sandbox’larda çalışan user mode programları hâline gelir
  • Bilinen Linux ihlal vakaları içindeki kritik vakaları analiz eden bir araştırmada, mikro çekirdek tasarımının bunların %29’unu tamamen ortadan kaldırabileceği, ek %55’ini ise artık kritik olarak sınıflandırılmayacak ölçüde hafifletebileceği görüldü

PPC, capability ve ince taneli yetki denetimi

  • seL4, korumalı prosedür çağrısı (PPC) mekanizması sağlar
    • Tarihsel nedenlerle IPC terimi kalmış olsa da IPC ifadesi yanlış anlaşılmalara yol açarak kötü tasarımlara neden olabilir
    • PPC, bir programın başka bir sandbox’taki programın fonksiyonunu güvenli biçimde çağırmasını sağlar
  • Mikro çekirdek, PPC’de girdileri ve çıktıları aktarır ve arayüzü zorunlu kılar
    • Uzak fonksiyon yalnızca dışa aktarılan giriş noktalarından çağrılabilir
    • Yalnızca uygun capability verilmiş, açıkça yetkilendirilmiş istemciler çağrı yapabilir
  • Capability, sistemdeki belirli bir kaynağa erişim sağlayan bir erişim token’ıdır
    • Hangi varlığın hangi kaynağa erişebileceğini çok ince taneli biçimde kontrol eder
    • En az ayrıcalık ilkesini veya least authority ilkesini (POLA) destekler
  • Linux veya Windows gibi ana akım sistemlerdeki erişim denetimi yaklaşımlarıyla bu düzeyde en az ayrıcalığa ulaşmak mümkün değildir
  • seL4, capability tabanlı ve biçimsel olarak doğrulanmış dünyadaki tek OS olarak değerlendirilir; bu birleşim sayesinde dünyanın en güvenli OS’si olduğu yönünde savunulabilir bir iddiaya sahiptir

Biçimsel doğrulama ve güvenlik garantileri

  • seL4, uygulama doğruluğuna ilişkin biçimsel, matematiksel ve makineyle doğrulanmış kanıt sunar
    • Bu kanıt, kernel’in belirtime göre çok güçlü bir anlamda “hatasız” olduğu anlamına gelir
    • seL4, kod düzeyinde böyle bir kanıta sahip dünyanın ilk OS çekirdeğidir
  • Uygulama doğruluğunun yanı sıra seL4, güvenlik yaptırımı için ek kanıtlar da sunar
    • Doğru yapılandırılmış seL4 tabanlı sistemlerde kernel gizlilik, bütünlük ve kullanılabilirliği garanti eder
  • Doğrulama zinciri, seL4’ün temel ayırt edici yönüdür
    • Güvenlik ve emniyet açısından kritik sistemlerde kernel’in güven temeli olabilmesi için uygulamaya ve güvenlik özelliklerine dair güçlü güvenceler gerekir

Gerçek zamanlılık ve karma kritiklikte sistemler

  • seL4, en kötü durum yürütme süresi (WCET) için eksiksiz ve sound bir analizden geçmiş bir OS çekirdeğidir
    • Kernel uygun şekilde yapılandırıldığında tüm kernel işlemleri zaman açısından sınırlıdır
    • Bu sınırlar da bilinmektedir
  • Bu özellik, hard real-time system kurmanın ön koşuludur
    • Kesin biçimde sınırlanmış süre içinde olaylara tepki verememenin kritik sonuçlar doğuracağı sistemleri hedefler
  • seL4, karma kritiklikte gerçek zamanlı sistemleri (MCS) de destekler
    • Daha düşük güvenilirlikteki kod aynı platformda birlikte çalışsa bile kritik faaliyetlerin zamanlamasının garanti edilmesi gereken ortamları hedefler
    • Mevcut MCS OS’lerin kullandığı katı ve esnek olmayan zaman/alan bölümlemesinin aksine seL4, kaynak kullanımını koruyan esnek bir model sunar

seL4’ü hypervisor olarak kullanmak

  • seL4 bir mikro çekirdek olmasının yanı sıra bir hypervisor’dır
    • seL4 üzerinde sanal makineler çalıştırılabilir
    • Sanal makinelerin içinde Linux gibi sıradan guest OS’ler çalıştırılabilir
  • Guest’ler ve uygulamalar, seL4’ün zorunlu kıldığı iletişim kanallarına göre birbirleriyle haberleşebilir
    • Native uygulamalarla da iletişim kurabilirler
  • Linux VM, sistem servisleri sağlamak için kullanılabilir
    • Örnek yapılandırmada ağ ve depolama gibi servisler, ayrı VM’lerde çalışan birden çok Linux instance’ından ödünç alınır

seL4 üzerinde sistem oluşturma yöntemi

  • seL4 API’si, diğer mikro çekirdeklere kıyasla bile çok düşük seviyelidir
    • Yalnızca donanımı güvenli biçimde yönetmek için gereken asgari soyutlamaları sağlar
    • seL4, “işletim sisteminin assembly dili”ne benzetilir
  • Karmaşık sistemleri doğrudan seL4 üzerinde inşa etmek uygun bir yaklaşım değildir
    • Daha yüksek seviyeli framework’lerin, servis uygulama koduna odaklanmayı sağlaması ve donanım karmaşıklığı ile sistem entegrasyonunu otomatikleştirmesi gerekir
  • seL4 için üç ana açık kaynak bileşen framework’ü vardır
    • Microkit: protection domain merkezli az sayıda soyutlamayla seL4 API’sini basitleştirir; ayrı derlenen modülleri ve kernel binary’sini birleştirerek boot edilebilir imaj oluşturan bir SDK sağlar
    • CAmkES: Microkit’in öncülüdür ve statik mimarili sistemler için bir bileşen framework’üdür; ancak SDK’sı olmadığı için build süreci daha zahmetlidir ve overhead’i daha yüksektir
    • Genode: Birden çok mikro çekirdeği destekler, x86 platformları için servis ve sürücüleri zengindir ve statik mimariyi zorunlu kılmaz; ancak seL4’ün tüm güvenlik ve emniyet özelliklerinden yararlanamaz ve güvence hikâyesi yoktur
  • Statik sistem mimarisi gereksinimlere uyduğu sürece, seL4 tabanlı sistemler oluşturmak için Microkit önerilir
    • Statik mimari, modül kümesini ve iletişim yapısını sistem yapılandırma anında tanımlayan bir modeldir
    • Bu modelin, otomobil ve uçak gibi karmaşık siber-fiziksel sistemler dahil çoğu gömülü sistem gereksinimine uyduğu kabul edilir

İlgili okumalar

1 yorum

 
GN⁺ 2025-03-24
Hacker News yorumları

  • seL4’nin kendisi eski bir konu; mikroçekirdeğin ötesinde yeni biçimsel olarak doğrulanmış katmanlar ya da bileşenler eklenip eklenmediğini merak ediyorum.
    Ayrıca “kanıt” kelimesini görünce duygusal olarak aşırı yüklenip düşünmeyi bırakan insanlar da var gibi görünüyor. Biçimsel doğrulama, güvenli BT gibi sonsuz bir problemi çözen her derde deva bir şey de değil, kusursuz yazılım üretmenin bir yolu da değil.
    Benim anladığım kadarıyla, belirli koşullar altında belirli gereksinimlerin karşılandığına dair bir kanıt; bu gereksinimler ve koşullar oldukça dar olabilir ve belirtimin dışındaki işlevler ve koşullar hakkında hiçbir şey söylemez. Kabaca doğru mu, merak ediyorum.
    Pratikte bir güvenlik uzmanının “biçimsel olarak doğrulanmış yazılım” gördüğünde ne beklediğini de merak ediyorum. Buradaki kilit bilgi, seL4’ün karşıladığı belirtimin ne olduğu değil mi?

    • Çeşitli kusurların bulunmadığı biçimsel olarak doğrulanmış olsa da seL4 bellek bozulması kusurlarına bağışık değildi. Birkaç yıl önce bir bellek bozulması kusuru bulundu; bunu düzelten commit ve seL4 kanıtını düzelten PR herkese açık.
      https://github.com/seL4/seL4/pull/243
      https://github.com/seL4/l4v/pull/453
      Issue izleyicisinde de bellekle ilgili birkaç hata var.
      https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
      İlginç biçimde, bellekteki “register clobbering”i düzelten PR’a bug etiketi konmamış; bu yüzden “bug” ile filtreleyince görünmüyor. Eskiden kanıt sayesinde seL4’ün bu tür sorunlara bağışık olduğunu düşünürdüm; bunu gördükten sonra kanıtın, topluluğun inandığı kadar kapsayıcı olmadığı kanaatine vardım. Yine de seL4 hâlâ çok etkileyici bir yazılım.
      Soruyu yanıtlamak gerekirse, seL4’ün karşıladığı belirtim GitHub’da herkese açık.
      https://github.com/seL4/l4v
    • Biçimsel olarak doğrulanmış katmanlar veya bileşenler sürekli ekleniyor. Yakın zamanda RISC-V gibi yeni mimari destekleri, karma kritiklikli zamanlama, Microkit ve Device Driver Framework eklendi.
      Karma kritiklikli zamanlama, CPU zamanı için capability tabanlı erişim, iş parçacığı yürütme üst sınırını sınırlama, yüksek kritiklikli işlerin önceliği ve kaynak erişimi garantisi, ayrıca çağıranın bağışladığı zamanlama süresiyle çalışan “passive servers” sunar.
      Microkit, seL4 üzerinde gerçek sistemler kurmayı çok daha kolaylaştıran doğrulanmış bir soyutlama katmanı; Device Driver Framework ise seL4’te yüksek performanslı giriş/çıkış için aygıt sürücüsü şablonları, kontrol/veri düzlemi uygulamaları, sürücü yazma ve aygıt sanallaştırma araçlarıdır.
      Biçimsel doğrulama, belirli koşullar altında belirli gereksinimlerin geçerli olduğunu garanti edebilir. Genel olarak bu tür gereksinimlerin ve koşulların dar olabileceği doğru; ancak seL4’ün kendisinde, bir çekirdekten beklenebilecek geniş bir özellik yelpazesini kapsayan çok sayıda kanıt var ve bu garantiler çok zayıf varsayımlar altında bile geçerli. C derleyicisinin doğruluğunu da varsaymıyor; derleyici çıktısına bakıp derlenmiş ikilinin istenen C semantiğine uygun davrandığını kanıtlayan ayrı bir araç var.
      seL4’ün karşıladığı gereksinimler arasında, seL4 çekirdeğinin ikili kodunun soyut belirtimde tarif edilen davranışı tam olarak uyguladığı ve bunun ötesinde hiçbir şey yapmadığı yer alır. Buffer overflow, bellek sızıntısı, pointer hatası, null pointer dereference, C kodunda tanımsız davranış, belirtimde listelenen açık yöntemler dışındaki çekirdek sonlandırmaları yoktur.
      Belirtim ve seL4 ikilisi bütünlük ve gizlilik güvenlik özelliklerini de karşılar. Bütünlük, bir sürecin açık yetkisi olmayan verileri değiştirmenin hiçbir yoluna sahip olmadığı anlamına gelir; gizlilik ise yetkisiz verilerin hiçbir şekilde okunamayacağı anlamına gelir. Belirli yan kanallar üzerinden verilerin dolaylı olarak çıkarılamayacağı da gösterilir. Güvenliğin yanında beklenen en kötü yürütme süresi garantileri ve zamanlama özellikleri de karşılanır.
    • seL4 geliştiricileri birkaç yıldır finansman sıkıntısı çekiyor. Çalışmaların çoğu uzaktan kumandalı dronlar için DARPA araştırmasıydı; ABD ordusu hack’lenemeyen dronları çok istiyor.
      Şu anki çalışma, daha geniş benimsenmeyi hedefleyen LionsOS tarafında: https://lionsos.org/
    • Örneğin buffer overflow, null pointer istisnası, use-after-free gibi şeyler yok. ARM ve RISCV64’te ikili için işlevsel doğruluk kanıtlandığından C derleyicisine bile güvenmek gerekmiyor. İşlevsel doğruluğun dışında daha fazla kanıt da var.
      https://docs.sel4.systems/projects/sel4/frequently-asked-que...
    • https://github.com/auxoncorp/ferros
      Kaynakları, donanım erişimini ve capability’leri derleme zamanında izlemek için tip düzeyi programlamayı yoğun biçimde kullanıyor. Runtime’da sorun bulup debug etmek çok kötü bir deneyim olduğundan, temel çekirdek garantilerinin bir kısmını derleyici tarafına taşımaya yönelik bir girişim.

  • Konuk monolitik çekirdek çalıştıran mikroçekirdek host yaklaşımını sevdiğim için, sunucular FreeBSD VM’in güvenlik katmanı ve yedeği olarak seL4 çalıştırıyor; onun içinde renderfarm, BEAM kümesi ve Jenkins için jail kullanıyorum.
    Üzücü olan, DragonflyBSD’nin threading’i ve süreç içi çekirdeği, yani hibrit çekirdek tasarımı için bir ARM portunun olmaması. Hayalim, OpenMoonRay’i 128 çekirdekli Ampere Altra üzerinde daha verimli çalıştırmak.

    • Sunucuda seL4’ü nasıl kullandığını daha ayrıntılı öğrenmek isterim. Bunun prodüksiyon ticari sunucusu olup olmadığını da merak ediyorum.
    • Bu yapılandırma uzun bir yazı olarak okunsa epey ilginç olurdu.

  • Artık mikroçekirdek lehine/aleyhine tartışmasının kendisi pek anlamlı olmaktan çıkıyor gibi. Yetkili servislere hızlı, verimli ve güvenli biçimde erişmenin tek yolu donanım azaltımları; yazılımın yapabileceklerinin bir sınırı var.
    Bu, 80286 ile 80386 arasındaki farka benziyor. İkincisi, birincide olmayan gerçek çoklu görev için donanım desteği eklemişti. Sonrasında hipervizörleri mümkün kılan türden donanım düzeyinde koruma mekanizmaları sürekli arttı.
    Özellikle Apple, SoC’lerine çekirdeği, sürücüleri ve bileşenleri çip düzeyinde koruyan; çalışan iş parçacıkları ve işaretçi kullanımı sırasında yetkileri zorunlu kılan pek çok özellik ekliyor. https://support.apple.com/guide/security/operating-system-in...
    Bu, işletim sisteminin aşılamaz olduğu anlamına gelmiyor; ama yetkileri yalnızca yazılımla yönetme stratejisinden çok daha etkili. Bu tür özelliklerden ya da benzerlerinden yararlanıldığında çekirdek mimarisi artık o kadar önemli değilmiş gibi görünüyor; yanılıyor muyum merak ediyorum.

    • Yanılıyorsun. İşletim sistemi araştırmaları alanında hâlâ yapılacak çok iş var; yeni donanımlar için yazılım arayüzleri ve API’ler gerekiyor.
      Daha bileştirilebilir mikro/hibrit sistemlerden de öğrenilecek çok şey var. Örneğin Plan 9, tek bir protokol olan 9P ile sistemdeki tüm nesneleri kullanıcı alanına sunan mükemmel bir hibrit sistemdir. IP veya TLS gibi bazı parçalar, sistem çağrısı ek yükünden kaçınmak için çekirdeğin içinde olduğundan hibrittir.
      Bir başka ilginç tasarım da çekirdek içi sürücülerin çoğunlukla donanım mantığına yönelik 9P arayüzü görevi gören asgari biçimde olmasıdır. Böylece işaretçiler veya kayıtlar gibi makine nesneleri gezilebilir dosyalara dönüştürülebilir, bu dosyalar standart Unix izinleriyle korunabilir ve bileşenler ağ üzerinden birden fazla makineye kolayca dağıtılabilir. Sonuçta sürücü mantığı güvenli biçimde kullanıcı alanı programlarına itilebilir.
      9P ağ ve mimari açısından şeffaftır; bu yüzden Arm, x86, mips gibi farklı makineler doğrudan birlikte çalışabilir. Plan 9’dan Linux/Unix ya da Windows’a dönünce insan üzülüyor ve bunalıyor. Esneklik neredeyse magmatik kaya düzeyinde; aynı işi, yani dosya/nesne sunmayı yapan sayısız protokolle özellikler birbirleriyle uyumsuz şekilde yamalanmış durumda.
    • Mikroçekirdeğin yararı, donanım/yazılım ortak tasarımından ayrı bir eksendir.
      Pratik mühendislik açısından monolitik çekirdek daha hızlı, daha kolay ve daha fazla kaynağa sahipti; güvenlik ise C ile mümkün olan düzeydeydi: yani en iyi çaba ve sayısız hata. Bu karmaşayı hafifletmek için çok sayıda donanım getirildi. Ama SeL4 söz konusuysa, süreçler arası yalıtım ve root düzeyi exploit bulunmaması konusunda güven çok yüksek olduğundan, teorik olarak bir güvenlik yardımcı işlemcisine ihtiyaç olmayabilir. Dolayısıyla donanım/yazılım ortak tasarımı önemlidir.
      Ancak SeL4 ekibi de donanımdaki yan kanalları ortadan kaldırmak için çok fazla mühendislik kaynağı harcamak zorunda kaldı. Gerçek dünya fizik simülasyonlarını umursamadığı için donanımda da kusurlar var.
      Burada mikroçekirdeğin avantajı, biçimsel doğrulamanın başa çıkabileceği kadar küçük olmasıdır. İspatın kendisi çekirdek boyutunun 10 katıdır. SeL4’ün bağlam değiştirmesi Linux’tan tek haneli katlar kadar daha hızlıdır; dolayısıyla performans etkisi ihmal edilebilir olmalı. Ama sihirli bir şekilde milyonlarca satırlık monolitik bir çekirdeği doğrulayabilseydiniz, bağlam değiştirmemek hâlâ daha hızlı olurdu. Nitekim SeL4 ekibi zamanlayıcıyı kullanıcı alanına taşımaya çalıştı, ancak performans maliyeti çok yüksek olduğu için onu çekirdekte bıraktı ve ispat yüküne ekledi.
    • 80286 ile 80386 karşılaştırmasının iyi bir benzetme olup olmadığından emin değilim. 286 da korumalı modda gerçek çoklu görevi destekliyordu ve çeşitli DOS dışı işletim sistemlerinde kullanıldı. 386’nın eklediği şeylerden biri sanal 8086 moduydu; bu da donanıma doğrudan erişen mevcut gerçek mod DOS uygulamalarının çoklu görev altında çalıştırılmasını mümkün kıldı.
    • Bu açıklama doğru görünmüyor. Güçlü donanım koruması olsa bile Linux’un güvenilir bilgi işlem tabanı bir mikroçekirdekle nasıl karşılaştırılabilir? Aynı koruma alanlarını yeniden üretmediğiniz sürece Linux’ta daha fazla zafiyet kalır.
      Aksine donanımın başlıca rolü verimliliği artırmaktır. Örneğin günümüzde mikroçekirdekler zaten MMU gibi donanımlardan iyi yararlandıkları için oldukça sağlamdır. Ardından mikroçekirdeğin küçük güvenilir bilgi işlem tabanı çekirdeğe güvenilirlik kazandırır; çekirdek ve donanım birlikte sağlam bir temel oluşturur.
      Sonuçta mesele, donanımla ne ölçüde “hileye” izin verileceğidir; ama genel olarak mikroçekirdekler koruma özelliklerinden daha iyi yararlanır. Ya da eksokernel’lere de bakabilirsiniz.

  • https://genode.org/index
    seL4 desteği olan bir işletim sistemi.

    • Genode’un kayda değer kullanım alanları var mı merak ediyorum

  • Yerel OWASP bölümünde SeL4 sunumu yapmıştım. Materyalleri bulabilir miyim bilmiyorum
    Bu proje gerçekten çok iyi yapılmış bir şey, ama özellikle genel amaçlı bilgi işlemde Linux’un yerine geçecek bir alternatif olarak görmekte tereddüt ediyorum. Bu, mikroçekirdeklerin genel amaçlı kullanımda genel olarak kötü olduğu anlamına gelmiyor. RedoxOS son dönemde bir miktar ilerleme kaydetmiş görünüyor ve Rust ile yazılmış bir mikroçekirdek kullanıyor

    • Sorun her zaman “ne kadar geniş kapsamlı bir ikameden söz ediyoruz” meselesi. Redox, POSIX birlikte çalışabilirliğini iyi korumaya çalışıyor gibi görünüyor; bu da doğal olarak tasarım kararlarını etkiliyor. Teknik yetkinliğe sahip olmak ile başarılı olmak arasında da büyük bir fark var
      Yine de Redox başarılı olursa, bu tek başına iyi bir ilerleme olur. seL4’te bu özellikler daha uç noktada. Teknik üstünlükleri çok güçlü, ancak şimdiye kadar olmadığı gibi muhtemelen gelecekte de ‘bir sonraki büyük şey’ olmak için gereken bir şeye sahip olmayacak gibi görünüyor. Siyasi değerlendirmeleri bir kenara bırakırsak mikroçekirdeklerin başarılı olacağını ve başarılı olması gerektiğini düşünüyorum
    • Linux’un yerine geçebilme ihtimali senaryoya bağlı. Elbette Linux ile çalışmak daha kolay, ama buna karşılık yalnızca seL4’ün karşılayabileceği gereksinimler de var
      seL4’ün pratikte faydalı olabilmesi için üzerinde çok şeye ihtiyaç var. Neyse ki bu alanda da çok sayıda açık kaynak çalışma yürütüldü ve birkaç yıl öncesine göre çok daha iyi bir konumda
      Statik senaryolar için LionsOS[0] var ve şimdiden oldukça kullanılabilir durumda
      Dinamik senaryolar için Provably Secure, General-Purpose Operating System[1] var; ancak hâlâ erken aşamada
      İkisi de seL4 web sitesinden bağlantı verilen trustworthy systems’in Projects sayfasında[2] bulunabilir
      [0] https://trustworthy.systems/projects/LionsOS/
      [1] https://trustworthy.systems/projects/smos/
      [2] https://trustworthy.systems/projects/

  • Bu çekirdeğin üzerinde çalışan OS’nin de güvenlik garantilerinin geçerli olması için biçimsel olarak doğrulanmış olması gerekip gerekmediğini merak ediyorum

    • Çekirdeğin sağladığı garantiler, üzerinde çalışan ayrıcalıksız süreçler tarafından bozulamaz
      Elbette tek başına çekirdek pek kullanışlı olmadığından, çekirdeğin üzerinde çalışan sürücülerin, dosya sistemi sunucularının ve diğer servislerin tasarımı hâlâ önemlidir
      Linux dahil diğer sistemlerin çoğu temel düzeyde kusurlu, ancak seL4’ün gerçekten güvenli ve güvenilir sistemler kurmayı mümkün kılması da önemli
    • Hayır. Avantajı, çekirdeğin izolasyonu garanti etmesi sayesinde çekirdeğe ve süreçlere güvenmek zorunda olmamanızdır
      Bu nedenle Linux çekirdeğini yüksek güvenlikli bir sürecin yanında çalıştırırken bile, izin verilen IPC dışında birbirlerinden izole olduklarına dair garantiye sahip olabilirsiniz
    • Hayır
      Ama sınırları var. DMA kapatılmalı ve yalnızca biçimsel olarak doğrulanmış sürücüler kullanılmalı
      seL4’ün çok çekirdekli çekirdeğinin henüz doğrulanmamış olması da önemli
    • Mutlak anlamda bakılırsa evet denebilir. Pratik düzeyde ise makalenin 7.2 bölümünde kısmi bir yanıt bulunabilir

  • Drew DeVault’un Helios Microkernel’ına da bakmaya değer. SeL4 tabanlı olduğu söyleniyor
    https://ares-os.org/docs/helios/

    • “Tabanlı” ile “esinlenmiş” arasında anlamlı bir fark var ve Helios ikincisine daha yakın görünüyor

  • Karlsruhe Üniversitesi’nde L4 popülerdi. Ayrıntılı olarak incelemiş değilim ama pratikte işe yarar bir şey yapmaktan çok, teorik fikirleri sınamaya odaklanan bir proje gibi görünüyordu.
    Bu 20 yıl önceydi ve bana kalırsa bugün de pek değişmiş değil. Hızlıca arayınca onun üzerinde işletim sistemi yapmaya yönelik girişimler var gibi görünüyor, ancak gerçek kullanımdan çok kavram kanıtına daha yakın duruyorlar.

    • https://en.wikipedia.org/wiki/L4_microkernel_family sayfasına bakınca L4’ün çeşitli yerlerde kullanıldığı, ağırlıklı olarak da gömülü ortamlarda kullanılmış olduğu görülüyor.
      “OKL4 sevkiyatları 2012 başında 1,5 milyar adedi aştı; bunların çoğu Qualcomm kablosuz modem çipleriydi. Diğer dağıtımlar arasında otomotiv bilgi-eğlence sistemleri de yer alıyor.”
      “A7’den başlayan Apple A serisi işlemcilerde, L4 işletim sistemi çalıştıran Secure Enclave yardımcı işlemcisi bulunur; bu OS, 2006’da NICTA’da geliştirilen L4-embedded çekirdeğini temel alan sepOS’tur. Bunun sonucunda L4, Apple silicon taşıyan Mac’ler dahil tüm modern Apple cihazlarında yer alır.”
    • Jochen Liedtke 1999’da Karlsruhe’de profesör oldu, ancak ne yazık ki 2001’de kısa süre sonra hayatını kaybetti. Halefi Bellosa’nın hâlâ L4 araştırması yapıp yapmadığını bilmiyorum. L4Ka projesi vardı ama tamamlanmış görünüyor. Bellosa’nın lisans düzeyi işletim sistemleri dersinde müfredatta yer almıyor.
      Bellosa’nın eski öğrencilerinden Rittinghaus, HN’de de birkaç kez tanıtılan Unikraft[0] ile ilgili ve unikernel teknolojisini kullanıyor.
      [0] https://unikraft.org/
    • iPhone’da bir L4 türevi kullanılıyor.
      “Secure Enclave Processor, Apple’ın özelleştirdiği bir L4 mikrokernel sürümünü çalıştırır.”
      https://support.apple.com/de-at/guide/security/sec59b0b31ff/...
    • Açık kaynak türevi L4Re, tüm id.X Volkswagen araçlarının merkezi “icas1” ECU’sunda çalışıyor ve Linux ile başka konukları barındırıyor.
      https://www.kernkonzept.com/kk_events/elektrobit-advances-au...
      Bana kalırsa L4Re çekirdeği de Elektrobit Safe Linux’un bir parçası.
    • Karlsruhe ekibinin L4Ka’da, özellikle Pistachio’da yaptığı işi ve izlediği yönü seviyorum. Tasarım temiz, basit ve anlaşılması kolaydı.
      Mezuniyet tezimde Pistachio tabanlı bir OS yapmıştım. Karlsruhe’de okusaydım muhtemelen OS araştırmasına yönelirdim diye hep düşünmüşümdür.

  • Benim de işletim sistemi tasarımına dair fikirlerim vardı ve düşündüğüm capability, seL4’teki gibi araya girme ve yetki devretme işlevlerini kullanıyordu. Orada yazanların dışında da avantajları var. Örneğin sese filtre uygulamak veya ağ şeffaflığı sağlamak için proxy capability kullanılabilir.
    Gerçek zamanlı özelliklerin isteğe bağlı bir implementasyon olarak izin verilebileceğini düşünüyordum. Benim fikrim tek bir implementasyondan çok bir spesifikasyona yakındı.
    Ayrıca istediğim bir özellik, tüm programların giriş/çıkış dışında deterministik çalışmasıydı. Giriş/çıkış olmadan tarih/saati ya da programın çalışma süresini bilemezsiniz; işlemci özelliklerini de kontrol edemezsiniz. Donanımın desteklemediği bir özellik kullanılırsa işletim sistemi bunu emüle edebilir.
    Bunu gerçekleştirmek için donanım desteği ile yazılım desteğini birlikte kullanmayı düşünüyordum. Belgede donanımda uygulanmış capability’lere yönelik saldırılarla ilgili bir not var, ancak referans belge elimde olmadığından o saldırının benim düşündüğüm yönteme de uygulanıp uygulanmadığını bilmiyorum.

  • Güvenlik açısından Linux çekirdeğindeki KVM gibi bir zafiyeti var gibi görünüyor. Hypervisor ring 0’daysa, bir VM’den başka bir VM’ye veya doğrudan host’a kaçış riski olur.
    Bu riskin nasıl azaltıldığını merak ediyorum.

    • seL4’ün sanallaştırma desteğinde VM istisnaları mesajlara dönüştürülür ve ayrıcalıksız modda çalışan bir görev olan VMM bunları işler.
      VMM, VM’in kendisinden daha fazla capability’ye sahip olmadığından, akademik anlam dışında VM’den kaçış değerli değildir.
      Orijinal PDF’in 8–10. sayfalarına bakılabilir.