Pengenalan Mikrokernel seL4 [PDF]

• seL4 adalah mikrokernel OS yang menjalankan mode kernel dengan kode seminimal mungkin untuk mengendalikan sumber daya perangkat keras dan memperkuat keamanan
• Termasuk dalam keluarga mikrokernel L4 dan telah dikembangkan sejak pertengahan 1990-an
• Dapat berfungsi sebagai hypervisor sehingga mendukung menjalankan guest OS penuh seperti Linux
• Kernel OS pertama di dunia yang terbukti memiliki ketepatan fungsional, dengan pembuktian matematis hingga tingkat kode telah selesai
• Menggunakan model keamanan berbasis Capability untuk kontrol akses yang terperinci

Struktur seL4 dan fungsi hypervisor

• Kernel monolitik vs mikrokernel
  • Kernel monolitik (Linux, dll.): kode kernel sangat besar sehingga memiliki banyak kerentanan keamanan → sekitar 20 juta baris kode (20M SLOC)
  • Mikrokernel (seL4): menggunakan kode kernel seminimal mungkin → sekitar 10 ribu baris kode (10K SLOC)
  • Pengurangan ukuran kernel → keamanan lebih kuat dan permukaan serangan berkurang
• seL4 berperan sebagai hypervisor
  • Dapat menjalankan guest OS penuh seperti Linux di dalam VM
  • Setiap VM berjalan secara independen dan tidak dapat saling mengganggu → menjamin isolasi yang kuat
  • Protected Procedure Call (PPC) → memungkinkan komunikasi aman antar-VM

Verifikasi dan model keamanan seL4

• Verifikasi ketepatan fungsional
  • seL4 telah dibuktikan secara matematis benar secara fungsional pada tingkat kode
  • Menjamin semua perilaku kernel berjalan sesuai spesifikasi
• Validasi translasi (Translation Validation)
  • Membuktikan bahwa kode biner yang dihasilkan compiler benar-benar sesuai dengan kode C aslinya
  • Dijalankan melalui toolchain otomatis
• Verifikasi properti keamanan
  • Kerahasiaan: data hanya dapat diakses jika diizinkan secara eksplisit
  • Integritas: data hanya dapat diubah jika diizinkan secara eksplisit
  • Ketersediaan: sumber daya hanya dapat digunakan jika diizinkan secara eksplisit

Model keamanan berbasis Capability

• Apa itu Capability?
  • Token keamanan yang memberikan hak akses ke objek tertentu
  • Mengenkode referensi objek dan hak akses secara bersamaan
  • Memungkinkan kontrol akses yang rinci → menerapkan prinsip hak istimewa minimum (Principle of Least Privilege, POLA)
• Keunggulan Capability
  • Kontrol akses yang terperinci → memungkinkan minimisasi hak akses
  • Mendukung delegasi dan pencabutan hak akses
  • Model keamanan yang kuat → lebih unggul daripada model kontrol akses tradisional (ACL)
• Menyelesaikan masalah confused deputy
  • Dalam sistem tradisional berbasis ACL, status keamanan ditentukan oleh security ID milik subjek
  • Di seL4, Capability secara langsung menentukan hak keamanan → memungkinkan kontrol hak yang jelas

Dukungan sistem real-time dan sistem mixed-criticality

• Dukungan sistem real-time
  • seL4 mendukung penjadwalan berbasis prioritas
  • Analisis waktu eksekusi terburuk (WCET) untuk semua operasi kernel telah selesai → menjamin hard real-time
• Dukungan Mixed-Criticality System (MCS)
  • Mengalokasikan dan mengisolasi sumber daya CPU berdasarkan scheduling context
  • Mengendalikan agar tugas berprioritas tinggi tidak memonopoli CPU
  • Memungkinkan tugas kritis dan nonkritis berjalan secara bersamaan

Kinerja dan efisiensi

• Mikrokernel dengan kinerja tertinggi
  • Tidak menurunkan keamanan meski kinerja menjadi faktor penting
  • Biaya system call dan IPC diminimalkan → lebih dari 5 kali lebih cepat dibanding sistem pesaing
• Kinerja lebih unggul dibanding sistem pesaing
  • Fiasco.OC: sekitar 2 kali lebih lambat dibanding seL4
  • Zircon: sekitar 9 kali lebih lambat dibanding seL4
  • CertiKOS: sekitar 5 kali lebih lambat dibanding seL4

Penerapan di dunia nyata dan cyber retrofit

• Contoh penggunaan nyata

  • Berhasil diterapkan pada ULB (helikopter nirawak) milik Boeing
  • Terbukti memperkuat keamanan dan meningkatkan stabilitas sistem

• Penguatan keamanan bertahap pada sistem lama (Incremental Cyber Retrofit)

  • Menjalankan sistem lama di dalam VM sambil memodularisasinya secara bertahap
  • Memperkuat keamanan dan meminimalkan penurunan kinerja

Kesimpulan

• seL4 adalah mikrokernel paling aman di dunia yang telah terbukti dari sisi ketepatan fungsional, keamanan, dan kinerja
• Dengan model keamanan yang terverifikasi dan dukungan mixed-criticality, seL4 dapat digunakan secara praktis di berbagai bidang
• Dapat memperkuat keamanan sistem lama sekaligus meningkatkan kinerja → mikrokernel inovatif yang menyeimbangkan keamanan dan kinerja