Ironclad – kernel OS keluarga Unix dengan dukungan real-time

 (ironclad-os.org)
1 poin oleh GN⁺ 2025-11-10 | 1 komentar | Bagikan ke WhatsApp
  • 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
Iklan

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
    Iklan

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

Bacaan terkait

1 komentar

 
GN⁺ 2025-11-10
Komentar Hacker News

  • Proyek yang menarik. Saya penasaran dengan batasan verifikasi formal untuk worst-case execution time (WCET)
    Ada juga kernel terverifikasi lain seperti seL4 dan atmosphere, dan lapisan kompatibilitas POSIX juga bisa ditumpuk seperti genode
    Ada pula kernel yang sepenuhnya kompatibel dan matang seperti QNX atau VxWorks, jadi verifikasi penuh mungkin tidak menambah banyak nilai
    Namun, saya hampir tidak pernah melihat contoh yang sekaligus memiliki WCET + verifikasi formal + kompatibilitas POSIX
    Pada tahap saat ini, sulit mengatakan bahwa tingkat kematangannya sudah cukup tinggi untuk langsung dipakai pada use case real-time seperti yang disebutkan di dokumentasi

    • Di dunia sekarang, pemerintah mana pun bisa mendapatkan RCE pada OS. Karena itu, verifikasi formal untuk isolasi proses benar-benar penting
      seL4 jauh lebih cepat daripada Linux, tetapi ini sepertinya akan lambat. POSIX pada dasarnya punya cacat, dan MAC terlalu rumit sehingga sulit dipakai dalam praktik
    • Ini masih di level stone, tetapi ke depannya tampaknya bisa juga mendapatkan sertifikasi resmi. OS yang diverifikasi secara formal adalah kemajuan besar untuk peningkatan keamanan

  • Ada termasuk bahasa keluarga Wirth (keluarga Pascal). Sejauh ini, saya hanya tahu TUNIS sebagai kernel mirip Unix yang ditulis dengan bahasa keluarga Wirth
    TUNIS diimplementasikan dengan Concurrent Euclid

    • Ada juga SPIN yang dikembangkan di University of Washington pada tahun 90-an. Itu adalah sistem berbasis mikrokernel yang ditulis dengan Modula-3 dan mendukung antarmuka system call Digital UNIX
      Selain itu, Sol dari INRIA pada tahun 80-an diimplementasikan dengan dialek Pascal dan menyediakan lingkungan yang kompatibel dengan Unix, lalu berlanjut menjadi Chorus

  • Ada juga perusahaan terkait NDA bernama Ironclad. Perlu hati-hati soal masalah merek dagang
    Meski begitu, upaya seperti ini benar-benar menyenangkan untuk dilihat. Namun dalam kenyataannya, mata rantai terlemah dalam keamanan adalah lapisan firmware
    Impian saya adalah perangkat keras seperti komputer Framework memiliki firmware EFI yang terverifikasi serta firmware tiap komponen yang diaudit

    • Ironclad juga merupakan nama library kriptografi utama untuk Common Lisp (ironclad GitHub)
    • MNT Research juga layak dilihat. Mereka membuat laptop yang bisa diperbaiki, dan membuka sumber perangkat keras maupun perangkat lunaknya (mnt.re)
    • Verifikasi firmware memerlukan kernel tersendiri. Sekarang bagian seperti ini seharusnya sudah dikelola pada tingkat regulasi
    • Merek dagang tidak masalah meski namanya sama jika berada di bidang industri yang berbeda. Misalnya seperti kasus Apple Computer dan Apple Music milik Beatles (xkcd 386)

  • Membuat OS baru benar-benar langkah yang ambisius. Baru-baru ini Radiant Computer juga sempat muncul, jadi saya penasaran apakah ada proyek menarik serupa lainnya

    • Asterinas (kernel kompatibel Linux) dan Redox OS tampak menjanjikan
    • Ada juga SerenityOS
    • Ini memang alternatif lama, tetapi Haiku OS masih tetap menarik
    • Saya juga punya ide OS. Saya sedang membayangkan beberapa komponen, termasuk perangkat keras, kernel, dan program pengguna
    • ReactOS juga terus berkembang. Memang bukan OS yang sepenuhnya baru, tetapi menurut saya tetap terasa baru

  • Saya berharap suatu hari nanti kernel yang sepenuhnya diverifikasi secara formal menjadi umum
    Memverifikasi seluruh Linux mungkin tidak mungkin, tetapi seL4 tampaknya bisa mendapat peluang di pasar seperti smartphone

  • Kalau melihat roadmap verifikasi mereka, menyebutnya “verifikasi formal” terasa berlebihan
    Tidak ada pembuktian atas properti kernel yang inti, dan levelnya belum menyamai kernel seperti seL4 atau Tock

  • CuBit adalah OS lain yang ditulis dengan SPARK/Ada
    Kode sumbernya bisa dilihat di GitHub

  • Dari sudut pandang pengguna umum, kernel saja tidak ada gunanya
    Contoh OS yang menggunakan kernel Ironclad adalah Gloire

  • Dokumentasi terkait MAC tersusun dengan baik (Mandatory Access Control)

  • Melihat tulisan “hubungi untuk harga” pada SPARK, ini tampaknya ‘free’ dalam arti lain, bukan ‘perangkat lunak bebas’

    • Sebagian besar tautan GitHub di atas juga mengenakan biaya untuk dukungan komersial. Meminta orang menghubungi untuk harga adalah prosedur umum, jadi tidak ada yang terlalu aneh
    • Pada akhirnya, pengembang juga harus mencari nafkah, dan itu hal yang wajar