- Ironclad, genel kullanım ve gömülü ortamlar için biçimsel doğrulamaya dayalı, gerçek zamanlı destekli Unix benzeri bir çekirdek
- Biçimsel doğrulama (Formal verification): çalışma zamanı hatalarının yokluğu (AoRTE, Absence of Runtime Errors) ve bileşenlerin doğruluğunu güvence altına almak için çekirdek kodunun geçtiği bir dizi süreç ve denetim
- SPARK ve Ada ile yazılmıştır ve %100 özgür yazılımdan oluşur
- POSIX uyumlu arayüz, preemptive multitasking, zorunlu erişim denetimi (MAC) ve hard real-time scheduling desteği sunar
- GPLv3 lisansı ile dağıtılır ve firmware blob içermeyen tamamen açık kaynaklı bir yapıyı korur
- Birden çok platforma taşınabilir ve Gloire gibi dağıtımlar aracılığıyla ekosistemini genişletmektedir
Ironclad işletim sistemi çekirdeğine genel bakış
- Ironclad, biçimsel doğrulamayı (formal verification) kısmen uygulayan, gerçek zamanlı destekli UNIX benzeri bir çekirdektir
- Hem genel amaçlı hem de gömülü sistemler hedeflenerek tasarlanmıştır
- Biçimsel doğrulama (Formal verification): çalışma zamanı hatalarının yokluğu (AoRTE, Absence of Runtime Errors) ve bileşenlerin doğruluğunu güvence altına almak için çekirdek kodunun geçtiği bir dizi süreç ve denetim
- Bunun için Ada'nın bir alt kümesi olan SPARK kullanılır
- Tüm kod tabanı özgür yazılımdan oluşur
- Çekirdek, POSIX uyumlu arayüz sağlar ve preemptive multitasking, zorunlu erişim denetimi (MAC) ve hard real-time scheduling destekler
- Mevcut UNIX ortamlarına benzer bir geliştirme deneyimi sunar
- Gerçek zamanlı denetim gerektiren sistemler için uygun bir yapıya sahiptir
Özgür yazılım olarak özellikleri
- Ironclad, GPLv3 lisansı altında tamamen açık kaynak olarak dağıtılır
- Çekirdekte firmware blob bulunmaz
- Yığının tüm bileşenleri açık kaynak biçiminde sunulur
Biçimsel doğrulama (Formal Verification)
- SPARK dilinin biçimsel doğrulama özellikleri kullanılarak temel bileşenlerde hata yokluğu ve doğruluk güvence altına alınır
- SPARK, Ada kodunda ön koşullar (Pre), son koşullar (Post), bağımlılıklar (Depends) gibi tanımlamalar yaparak kodun mantıksal tutarlılığını matematiksel olarak doğrular
- Doğrulama kapsamına kriptografi modülleri, MAC sistemi ve kullanıcı arayüzüyle ilgili işlevler dahildir
Taşınabilirlik ve geliştirme ortamı
- Ironclad, çeşitli platformlara ve kartlara port edilmiştir ve ek taşımaları kolaylaştıracak şekilde tasarlanmıştır
- Yalnızca GNU toolchain'e bağımlı olduğundan kolay cross-compilation mümkündür
- POSIX uyumluluğu sayesinde yazılım portlama ve geliştirme kolaydır
Dağıtımlar ve ekosistem
- Ironclad projesi, farklı mimariler ve kartlar için çeşitli dağıtımlar (distribution) sunar
- Öne çıkan özgür ve açık kaynak dağıtımlardan biri Gloire'dır
- İndirilebilir tarball biçiminde dağıtım imajları sağlar
Proje desteği ve sürdürülebilirlik
- Ironclad, kullanım, araştırma ve değiştirme özgürlüğü sunan bir proje olarak sürdürülmektedir
- Projenin işletimi bağışlara ve hibelere dayanır
- Yapılan tüm katkılar, projenin genişlemesi ve gelişimi üzerinde doğrudan etki yaratır
1 yorum
Hacker News görüşleri
İlginç bir proje. En kötü çalışma süresi (WCET) için biçimsel doğrulamanın sınırlarını merak ediyorum
seL4, atmosphere gibi başka doğrulanmış çekirdekler de var ve genode gibi bir POSIX uyumluluk katmanı da eklenebilir
QNX ve VxWorks gibi tamamen uyumlu ve olgunlaşmış çekirdekler de olduğundan, tam doğrulama çok büyük bir ek değer katmıyor olabilir
Ama WCET + biçimsel doğrulama + POSIX uyumluluğunu bir arada sunan örnekleri neredeyse hiç görmedim
Şu anki aşamada, belgelerde geçen gerçek zamanlı kullanım alanlarında doğrudan kullanılabilecek kadar olgunluk seviyesinin yüksek olduğunu söylemek zor
seL4, Linux'tan çok daha hızlı ama bunun yavaş olacağını düşünüyorum. POSIX doğası gereği kusurlu ve MAC pratikte kullanılmayacak kadar karmaşık
Ada, Wirth ailesi dillere (Pascal ailesi) aittir. Şimdiye kadar Wirth ailesi bir dille yazılmış Unix benzeri tek çekirdek olarak yalnızca TUNIS'i biliyordum
TUNIS, Concurrent Euclid ile uygulanmıştı
Ayrıca 80'lerde INRIA'nın Sol sistemi, bir Pascal lehçesiyle uygulanmıştı ve Unix uyumlu bir ortam sunuyordu; daha sonra bu çalışma Chorus'a uzandı
Ironclad adını taşıyan, NDA ile ilgili bir şirket de var. Ticari marka sorunlarına dikkat etmek gerekir
Yine de bu tür girişimleri görmek gerçekten sevindirici. Ama pratikte güvenliğin en zayıf halkası firmware katmanı
Benim hayalim, Framework Computer benzeri donanımların doğrulanmış EFI firmware ve bileşen bazında denetlenmiş firmware ile gelmesi
Yeni bir OS yapmak gerçekten iddialı bir iş. Kısa süre önce Radiant Computer da paylaşılmıştı; buna benzer başka ilginç projeler var mı diye merak ediyorum
Bir gün tamamen biçimsel olarak doğrulanmış çekirdeklerin yaygınlaşmasını umuyorum
Linux'un tamamını doğrulamak imkânsız olabilir ama seL4, akıllı telefon gibi pazarlarda fırsat yakalayabilir gibi görünüyor
Onların doğrulama yol haritasına bakınca, buna “biçimsel doğrulama” demek abartılı kalıyor
Çekirdeğin kritik özelliklerine dair kanıtlar yok ve seL4 ya da Tock gibi çekirdeklerin seviyesine ulaşmıyor
CuBit, SPARK/Ada ile yazılmış başka bir OS
Kaynak kodu GitHub'da görülebilir
Sıradan kullanıcı açısından bakıldığında, yalnızca çekirdek tek başına işe yaramaz
Ironclad çekirdeğini kullanan bir OS örneği Gloire
MAC ile ilgili belgeler iyi düzenlenmiş (Mandatory Access Control)
SPARK'ın “fiyat için iletişime geçin” ifadesine bakınca, burada kastedilen ‘free’ daha çok ‘özgür yazılım’ değil başka bir anlamdaki free gibi duruyor