Ironclad – kernel OS keluarga Unix dengan dukungan real-time

• Ironclad adalah kernel keluarga Unix dengan dukungan real-time berbasis verifikasi formal untuk lingkungan umum dan embedded
  • Verifikasi formal: serangkaian proses dan pemeriksaan yang dilalui kode kernel untuk menjamin tidak adanya error saat runtime (AoRTE, Absence of Runtime Errors) serta ketepatan komponen
• Ditulis dengan SPARK dan Ada, serta tersusun dari 100% perangkat lunak bebas
• Mendukung antarmuka kompatibel POSIX, multitasking preemptive, mandatory access control (MAC), dan penjadwalan hard real-time
• Didistribusikan dengan lisensi GPLv3, sambil mempertahankan arsitektur open source sepenuhnya tanpa firmware blob
• Dapat diporting ke berbagai platform, dan ekosistemnya terus berkembang melalui distribusi seperti Gloire

---

Ikhtisar kernel sistem operasi Ironclad

• Ironclad adalah kernel keluarga UNIX dengan dukungan real-time yang menerapkan verifikasi formal secara parsial
  • Dirancang untuk sistem tujuan umum maupun embedded
  • Verifikasi formal: serangkaian proses dan pemeriksaan yang dilalui kode kernel untuk menjamin tidak adanya error saat runtime (AoRTE, Absence of Runtime Errors) serta ketepatan komponen
  • Untuk itu, proyek ini menggunakan SPARK, subset dari Ada
  • Seluruh kodenya tersusun dari perangkat lunak bebas
• Kernel ini menyediakan antarmuka kompatibel POSIX serta mendukung multitasking preemptive, mandatory access control (MAC), dan penjadwalan hard real-time
  • Memberikan pengalaman pengembangan yang mirip dengan lingkungan UNIX yang ada
  • Strukturnya cocok untuk sistem yang memerlukan kontrol real-time

Karakteristik sebagai perangkat lunak bebas

• Ironclad didistribusikan sebagai open source sepenuhnya di bawah lisensi GPLv3
  • Kernel tidak menyertakan firmware blob
  • Semua komponen dalam stack tersedia dalam bentuk open source

Verifikasi Formal

• Memanfaatkan fitur verifikasi formal pada bahasa SPARK untuk menjamin ketiadaan kesalahan dan ketepatan komponen utama
• SPARK memverifikasi konsistensi logis kode secara matematis dengan mendeskripsikan prasyarat (Pre), pascasyarat (Post), dependensi (Depends), dan lainnya pada kode Ada
  • Objek verifikasi mencakup modul kriptografi, sistem MAC, dan fitur terkait antarmuka pengguna

Portabilitas dan lingkungan pengembangan

• Ironclad telah diporting ke berbagai platform dan board, dan dirancang agar porting tambahan mudah dilakukan
  • Hanya bergantung pada toolchain GNU sehingga cross-compilation dapat dilakukan dengan mudah
  • Berkat kompatibilitas POSIX, porting perangkat lunak dan pengembangan menjadi lebih mudah

Distribusi dan ekosistem

• Proyek Ironclad menyediakan distribusi untuk beragam arsitektur dan board
  • Distribusi bebas dan open source yang representatif adalah Gloire
  • Menyediakan image distribusi dalam bentuk tarball yang dapat diunduh

Dukungan proyek dan keberlanjutan

• Ironclad dipertahankan sebagai proyek yang bebas digunakan, diteliti, dan dimodifikasi
  • Operasional proyek bergantung pada donasi dan hibah
  • Setiap kontribusi secara langsung memengaruhi perluasan dan perkembangan proyek