Pengantar Mikrokernel seL4 [PDF]

 (sel4.systems)
1 poin oleh GN⁺ 2025-03-24 | 1 komentar | Bagikan ke WhatsApp
  • seL4 adalah mikrokernel OS yang ditujukan untuk sistem tertanam dan sistem siber-fisik yang keamanan dan keselamatannya kritis. Ia mengisolasi dan memultipleks sumber daya hardware, tetapi bukan OS serbaguna yang lengkap
  • Dengan memangkas kode kernel mode menjadi sekitar 10 kSLOC, seL4 mengurangi TCB dan attack surface; layanan OS seperti sistem berkas, jaringan, dan driver didorong ke user mode
  • Kernel OS pertama di dunia yang memiliki verifikasi formal pada level kode, dan pada sistem yang dikonfigurasi dengan benar, kernel menjamin hingga properti keamanan seperti kerahasiaan, integritas, dan ketersediaan
  • Menggabungkan kontrol akses berbasis capability, analisis WCET, dukungan sistem real-time dengan mixed criticality, dan fungsi hypervisor untuk menangani isolasi granular sekaligus real-time behavior
  • Karena API seL4 berada pada level sangat rendah, sistem kompleks sulit dibuat langsung; jika arsitektur statis cocok, pendekatan realistis adalah memakai framework seperti Microkit

Cakupan yang ditangani seL4

  • seL4 adalah mikrokernel, bagian inti level rendah dari sistem operasi
    • OS mengendalikan hardware dan sumber daya dalam kernel mode, mode eksekusi prosesor dengan privilege lebih tinggi
    • Aplikasi berjalan di user mode dan hanya mengakses hardware dengan cara yang diizinkan OS
  • Mikrokernel adalah inti OS yang meminimalkan kode yang berjalan dengan privilege tinggi
    • seL4 termasuk dalam keluarga mikrokernel L4 yang sejarahnya berawal dari pertengahan 1990-an
    • seL4 tidak terkait dengan seLinux
  • seL4 bukan OS lengkap, melainkan kernel level rendah yang secara aman memultipleks dan mengisolasi sumber daya hardware
    • Layanan OS umum seperti sistem berkas, network stack, dan device driver tidak berada di dalam kernel
    • Layanan semacam ini harus disediakan sebagai program user mode

Struktur mikrokernel dan pengurangan attack surface

  • Kernel monolitik seperti Linux menyediakan layanan OS seperti penyimpanan berkas dan networking sebagai kode kernel mode
    • Kode kernel mode dapat mengakses sumber daya sistem tanpa batas; jika bug berujung pada privilege escalation atau eksekusi kode arbitrer, seluruh sistem dapat terdampak
    • Kernel Linux berukuran sekitar 20 MSLOC, dan diperkirakan dapat mengandung puluhan ribu bug
  • Mikrokernel yang dirancang dengan baik seperti seL4 memangkas kode kernel mode menjadi sekitar 10 kSLOC
    • Ini lebih kecil beberapa orde ratusan kali dibanding kernel Linux
    • Saat TCB mengecil, attack surface juga ikut berkurang
  • Sebagian besar layanan OS keluar dari kernel, dan mikrokernel bertindak seperti wrapper tipis di sekitar hardware
    • Fungsi inti yang disediakan adalah isolasi antarkomponen program dan mekanisme pemanggilan yang aman
    • Layanan menjadi program user mode yang berjalan di sandbox terpisah, bukan di dalam kernel
  • Dalam sebuah studi yang menganalisis kasus kompromi Linux yang diketahui dan bersifat fatal, desain mikrokernel dapat sepenuhnya menghilangkan 29% kasus dan memitigasi tambahan 55% sehingga tidak lagi diklasifikasikan sebagai fatal

PPC, capability, dan kontrol hak akses granular

  • seL4 menyediakan mekanisme protected procedure call (PPC)
    • Karena alasan historis, istilah IPC masih digunakan, tetapi ungkapan IPC dapat menimbulkan salah paham dan mengarah ke desain yang buruk
    • PPC memungkinkan satu program memanggil fungsi program lain yang berada di sandbox berbeda secara aman
  • Mikrokernel meneruskan input dan output dalam PPC serta menegakkan interface
    • Fungsi remote hanya dapat dipanggil melalui entry point yang diekspor
    • Hanya klien yang secara eksplisit diizinkan dan menerima capability yang sesuai yang dapat memanggilnya
  • Capability adalah token akses yang memungkinkan akses ke sumber daya tertentu dalam sistem
    • Ia mengontrol dengan sangat granular entitas mana yang dapat mengakses sumber daya mana
    • Mendukung prinsip least privilege atau prinsip otoritas paling minimal (POLA)
  • Dengan model kontrol akses pada sistem arus utama seperti Linux atau Windows, tingkat least privilege seperti ini tidak dapat dicapai
  • seL4 dinilai sebagai satu-satunya OS di dunia yang berbasis capability sekaligus terverifikasi formal; kombinasi ini memberinya klaim yang dapat dipertahankan sebagai OS paling aman di dunia

Verifikasi formal dan jaminan keamanan

  • seL4 menyediakan bukti formal, matematis, dan terverifikasi mesin atas correctness implementasi
    • Bukti ini berarti kernel “bebas bug” dalam makna yang sangat kuat terkait spesifikasinya
    • seL4 adalah kernel OS pertama di dunia yang memiliki bukti semacam ini pada level kode
  • Selain correctness implementasi, seL4 menyediakan bukti tambahan atas enforcement keamanan
    • Pada sistem berbasis seL4 yang dikonfigurasi dengan benar, kernel menjamin kerahasiaan, integritas, dan ketersediaan
  • Rantai verifikasi adalah pembeda inti seL4
    • Agar kernel menjadi dasar kepercayaan dalam sistem yang keamanan dan keselamatannya kritis, diperlukan jaminan kuat atas implementasi dan properti keamanannya

Real-time dan sistem mixed criticality

  • seL4 adalah kernel OS yang telah melalui analisis lengkap dan sound atas worst-case execution time (WCET)
    • Jika kernel dikonfigurasi dengan tepat, semua operasi kernel memiliki batas waktu
    • Batas tersebut juga diketahui
  • Karakteristik ini merupakan prasyarat untuk membangun sistem hard real-time
    • Ditujukan untuk sistem yang dapat berakibat fatal jika gagal merespons event dalam waktu yang dibatasi secara ketat
  • seL4 juga mendukung sistem real-time dengan mixed criticality (MCS)
    • Ditujukan untuk lingkungan yang harus menjamin timing aktivitas penting meski kode dengan tingkat kepercayaan rendah berjalan bersama pada platform yang sama
    • Berbeda dari partisi waktu dan ruang yang kaku dan tidak fleksibel pada OS MCS yang ada, seL4 menyediakan model fleksibel yang tetap mempertahankan pemanfaatan sumber daya

Menggunakan seL4 sebagai hypervisor

  • seL4 adalah mikrokernel sekaligus hypervisor
    • Virtual machine dapat dijalankan di atas seL4
    • Di dalam virtual machine, guest OS umum seperti Linux dapat dijalankan
  • Guest dan aplikasi dapat saling berkomunikasi sesuai kanal komunikasi yang ditegakkan seL4
    • Komunikasi dengan aplikasi native juga dimungkinkan
  • Linux VM dapat dimanfaatkan sebagai sarana penyedia layanan sistem
    • Dalam contoh konfigurasi, layanan seperti networking dan storage dipinjam dari beberapa instance Linux yang berjalan di VM terpisah

Cara membangun sistem di atas seL4

  • API seL4 berada pada level sangat rendah bahkan dibandingkan mikrokernel lain
    • Hanya menyediakan abstraksi minimum yang diperlukan untuk mengelola hardware secara aman
    • seL4 dianalogikan sebagai “bahasa assembly untuk sistem operasi”
  • Membangun sistem kompleks langsung di atas seL4 bukan pendekatan yang tepat
    • Framework level lebih tinggi harus memungkinkan fokus pada kode implementasi layanan, sekaligus mengotomatiskan kompleksitas hardware dan integrasi sistem
  • seL4 memiliki tiga framework komponen open source utama
    • Microkit: menyederhanakan API seL4 dengan sedikit abstraksi berpusat pada protection domain, serta menyediakan SDK untuk mengintegrasikan modul hasil kompilasi terpisah dan binary kernel menjadi image yang dapat di-boot
    • CAmkES: pendahulu Microkit dan merupakan framework komponen untuk sistem berarsitektur statis, tetapi tanpa SDK sehingga proses build lebih merepotkan dan overhead lebih besar
    • Genode: mendukung berbagai mikrokernel, kaya layanan dan driver untuk platform x86, serta tidak memaksakan arsitektur statis, tetapi tidak dapat memanfaatkan semua fitur keamanan dan keselamatan seL4 dan tidak memiliki cerita jaminan
  • Selama arsitektur sistem statis cocok dengan kebutuhan, Microkit direkomendasikan untuk membangun sistem berbasis seL4
    • Arsitektur statis adalah model yang mendefinisikan kumpulan modul dan struktur komunikasi pada saat konfigurasi sistem
    • Model ini dianggap sesuai dengan kebutuhan sebagian besar sistem tertanam, termasuk sistem siber-fisik kompleks seperti mobil dan pesawat

Bacaan terkait

1 komentar

 
GN⁺ 2025-03-24
Pendapat di Hacker News

  • seL4 sendiri sudah cerita lama, tetapi saya penasaran apakah ada lapisan atau komponen yang telah diverifikasi secara formal yang baru ditambahkan di luar mikrokernel
    Selain itu, saat melihat kata “bukti”, tampaknya ada orang-orang yang secara emosional menjadi kewalahan sampai berhenti berpikir. Verifikasi formal bukan obat mujarab untuk menyelesaikan masalah tak terbatas bernama IT yang aman, juga bukan cara untuk menghasilkan perangkat lunak yang sempurna tanpa cacat
    Sejauh yang saya pahami, ini adalah bukti bahwa persyaratan tertentu dipenuhi dalam kondisi tertentu, dan persyaratan serta kondisi itu bisa cukup sempit; artinya, ia tidak mengatakan apa pun tentang fungsi dan kondisi di luar spesifikasi. Saya penasaran apakah kira-kira begitu
    Secara praktis, saya juga penasaran apa yang diharapkan pakar keamanan ketika melihat “perangkat lunak yang diverifikasi secara formal”. Rasanya informasi kunci di sini adalah spesifikasi apa yang dipenuhi oleh seL4

    • Meski telah diverifikasi secara formal bebas dari berbagai cacat, seL4 tidak kebal terhadap cacat korupsi memori. Beberapa tahun lalu ditemukan cacat korupsi memori, dan commit yang memperbaikinya serta PR yang memperbaiki bukti seL4 tersedia secara publik
      https://github.com/seL4/seL4/pull/243
      https://github.com/seL4/l4v/pull/453
      Di issue tracker juga ada beberapa bug terkait memori
      https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
      Menariknya, PR yang memperbaiki “register clobbering” pada memori tidak diberi label bug, sehingga tidak muncul jika difilter dengan “bug”. Dulu saya mengira berkat bukti tersebut seL4 kebal terhadap masalah semacam ini, tetapi setelah melihat ini saya jadi menilai bahwa buktinya tidak seluas yang telah dipercaya komunitas. Meski begitu, seL4 tetap perangkat lunak yang sangat mengesankan
      Untuk menjawab pertanyaannya, spesifikasi yang dipenuhi seL4 tersedia di GitHub
      https://github.com/seL4/l4v
    • Lapisan atau komponen yang diverifikasi secara formal terus ditambahkan. Baru-baru ini masuk dukungan arsitektur baru seperti RISC-V, penjadwalan mixed-criticality, Microkit, dan Device Driver Framework
      Penjadwalan mixed-criticality menyediakan akses berbasis capability terhadap waktu CPU, pembatasan batas atas eksekusi thread, prioritas tugas berkepentingan tinggi serta jaminan akses sumber daya, dan “passive servers” yang berjalan dengan waktu penjadwalan yang didonasikan pemanggil
      Microkit adalah lapisan abstraksi terverifikasi di atas seL4 yang membuat pembangunan sistem nyata jauh lebih mudah, sedangkan Device Driver Framework adalah template driver perangkat untuk I/O berperforma tinggi di seL4, implementasi control/data plane, serta alat untuk menulis driver dan virtualisasi perangkat
      Verifikasi formal dapat menjamin bahwa persyaratan tertentu berlaku dalam kondisi tertentu. Secara umum benar bahwa persyaratan dan kondisi semacam itu bisa sempit, tetapi seL4 sendiri memiliki banyak bukti yang mencakup rentang luas properti yang layak diharapkan dari sebuah kernel, dan jaminan itu berlaku bahkan di bawah asumsi yang sangat lemah. Kebenaran compiler C pun tidak diasumsikan; ada alat terpisah yang melihat output compiler dan membuktikan bahwa binary hasil kompilasi berperilaku sesuai semantik C yang disyaratkan
      Persyaratan yang dipenuhi seL4 mencakup bahwa kode binary kernel seL4 mengimplementasikan secara tepat perilaku yang dideskripsikan dalam spesifikasi abstrak dan tidak melakukan lebih dari itu. Tidak ada buffer overflow, kebocoran memori, kesalahan pointer, dereferensi pointer null, perilaku tak terdefinisi dalam kode C, maupun terminasi kernel selain melalui cara eksplisit yang dicantumkan dalam spesifikasi
      Spesifikasi dan binary seL4 juga memenuhi properti keamanan integritas dan kerahasiaan. Integritas berarti proses sama sekali tidak punya cara untuk mengubah data yang tidak memiliki izin eksplisit, dan kerahasiaan berarti data tanpa izin tidak dapat dibaca dengan cara apa pun. Bahkan ditunjukkan bahwa data tidak dapat disimpulkan secara tidak langsung melalui side channel tertentu. Selain keamanan, jaminan worst-case execution time yang diperkirakan dan properti penjadwalan juga dipenuhi
    • Para pengembang seL4 sudah bertahun-tahun mengalami kesulitan pendanaan. Sebagian besar pekerjaannya adalah riset DARPA untuk drone yang dikendalikan jarak jauh, dan militer AS sangat menginginkan drone yang tidak bisa diretas
      Pekerjaan saat ini mengarah ke LionsOS untuk adopsi yang lebih luas: https://lionsos.org/
    • Misalnya, tidak ada buffer overflow, exception pointer null, use-after-free, dan sejenisnya. Di ARM dan RISCV64, correctness fungsional telah dibuktikan terhadap binary, sehingga bahkan compiler C tidak perlu dipercaya. Selain correctness fungsional, ada lebih banyak bukti lagi
      https://docs.sel4.systems/projects/sel4/frequently-asked-que...
    • https://github.com/auxoncorp/ferros
      Banyak menggunakan pemrograman tingkat tipe untuk melacak sumber daya, akses hardware, dan capability pada waktu kompilasi. Karena menemukan masalah di runtime lalu men-debug-nya terlalu buruk, ini adalah upaya untuk mengangkat sebagian jaminan kernel dasar ke sisi compiler

  • Saya menyukai host mikrokernel yang menjalankan kernel monolitik tamu, jadi server-server menjalankan seL4 sebagai lapisan keamanan dan backup untuk VM FreeBSD, dan di dalamnya saya memakai jail untuk renderfarm, klaster BEAM, dan Jenkins
    Yang disayangkan adalah tidak adanya port ARM untuk threading DragonflyBSD dan kernel internal prosesnya, yakni desain kernel hibrida. Impiannya adalah menjalankan OpenMoonRay dengan lebih efisien di Ampere Altra 128-core

    • Saya ingin tahu lebih detail bagaimana seL4 dipakai di server. Dan saya juga penasaran apakah ini server komersial produksi
    • Konfigurasi itu sepertinya akan cukup menarik jika dibaca dalam bentuk tulisan panjang

  • Kini tampaknya perdebatan pro-kontra microkernel itu sendiri sudah tidak terlalu bermakna. Satu-satunya cara untuk mengakses layanan berprivilege secara cepat, efisien, dan aman adalah mitigasi perangkat keras, dan ada batas pada apa yang bisa dilakukan perangkat lunak
    Mirip dengan perbedaan antara 80286 dan 80386. Yang terakhir menambahkan dukungan perangkat keras untuk multitasking sungguhan yang tidak dimiliki yang pertama. Setelah itu, mekanisme proteksi tingkat perangkat keras seperti yang memungkinkan hypervisor terus bertambah
    Khususnya Apple banyak memasukkan fitur ke dalam SoC untuk melindungi kernel, driver, dan komponen di tingkat chip, serta menegakkan privilege saat thread yang sedang berjalan dan pointer digunakan. https://support.apple.com/guide/security/operating-system-in...
    Bukan berarti OS tidak bisa ditembus, tetapi ini jauh lebih efektif daripada strategi mengelola privilege hanya dengan perangkat lunak. Jika memanfaatkan fitur semacam ini atau yang serupa, struktur kernel tampaknya tidak lagi begitu penting; saya penasaran apakah saya keliru

    • Keliru. Masih banyak yang harus dikerjakan dalam ranah riset OS, dan diperlukan antarmuka perangkat lunak serta API untuk perangkat keras baru
      Ada banyak hal yang bisa dipelajari juga dari sistem mikro/hybrid yang lebih mudah dikomposisikan. Misalnya, Plan 9 adalah sistem hybrid yang luar biasa, yang menyediakan semua objek sistem ke ruang pengguna melalui satu protokol, 9P. Disebut hybrid karena beberapa bagian seperti IP atau TLS berada di dalam kernel untuk menghindari overhead system call
      Desain menarik lainnya adalah bahwa driver internal kernel pada umumnya berbentuk minimal, hanya berperan sebagai antarmuka 9P untuk logika perangkat keras. Dengan begitu, objek mesin seperti pointer atau record diubah menjadi berkas yang bisa dijelajahi, berkas tersebut dilindungi dengan permission Unix standar, dan komponen dapat dengan mudah didistribusikan ke banyak mesin melalui jaringan. Hasilnya, logika driver bisa didorong dengan aman menjadi program ruang pengguna
      9P transparan terhadap jaringan dan arsitektur, sehingga berbagai mesin seperti Arm, x86, mips, dan lainnya bisa langsung bekerja bersama. Kembali dari Plan 9 ke Linux/Unix atau Windows terasa menyedihkan dan menjengkelkan. Fleksibilitasnya nyaris sekeras batuan beku, dan berbagai fitur ditambal secara tidak kompatibel lewat segudang protokol yang melakukan hal yang sama: menyediakan file/objek
    • Kegunaan microkernel adalah sumbu yang terpisah dari ko-desain perangkat keras/perangkat lunak
      Dari sudut pandang rekayasa praktis, kernel monolitik lebih cepat, lebih mudah, dan memiliki lebih banyak sumber daya; keamanannya sebatas apa yang mungkin dengan C, yaitu upaya terbaik dan segudang bug. Banyak perangkat keras diperkenalkan untuk memitigasi kekacauan itu. Namun dengan SeL4, tingkat kepercayaan terhadap isolasi antarproses dan ketiadaan exploit tingkat root sangat tinggi, sehingga secara teori koprosesor keamanan mungkin tidak diperlukan. Jadi ko-desain perangkat keras/perangkat lunak itu penting
      Namun, tim SeL4 juga harus menghabiskan banyak sumber daya rekayasa untuk menghilangkan side channel pada perangkat keras. Dunia nyata tidak peduli pada simulasi fisika, sehingga perangkat keras pun punya cacat
      Di sini keunggulan microkernel adalah ukurannya cukup kecil untuk ditangani oleh verifikasi formal. Buktinya sendiri berukuran 10 kali ukuran kernel. Context switch SeL4 lebih cepat satu digit kali lipat daripada Linux, jadi dampak performanya semestinya bisa diabaikan. Namun jika secara ajaib kita bisa memverifikasi kernel monolitik berjuta-juta baris, tidak melakukan context switch tetap lebih cepat. Faktanya, tim SeL4 pernah mencoba memindahkan scheduler ke ruang pengguna, tetapi biaya performanya terlalu besar sehingga tetap dipertahankan di dalam kernel dan ditambahkan ke beban pembuktian
    • Saya tidak yakin perbandingan 80286 dan 80386 adalah analogi yang bagus. 286 juga mendukung multitasking sungguhan dalam protected mode, dan digunakan oleh berbagai sistem operasi non-DOS. Salah satu hal yang ditambahkan 386 adalah mode virtual 8086, yang memungkinkan aplikasi DOS real mode lama yang mengakses perangkat keras secara langsung untuk dijalankan secara multitasking
    • Penjelasan itu tampaknya tidak tepat. Bahkan dengan proteksi perangkat keras yang kuat, bagaimana trusted computing base Linux bisa dibandingkan dengan microkernel? Kecuali domain proteksi yang sama direproduksi, Linux tetap memiliki lebih banyak kerentanan
      Justru peran utama perangkat keras adalah meningkatkan efisiensi. Misalnya, microkernel modern sudah memanfaatkan perangkat keras seperti MMU dengan baik sehingga cukup tangguh. Lalu trusted computing base microkernel yang kecil memberi keandalan pada kernel, dan kernel bersama perangkat keras membentuk fondasi yang kokoh
      Pada akhirnya ini soal sejauh mana perangkat keras membolehkan semacam “jalan pintas”, tetapi secara umum microkernel memanfaatkan fitur proteksi dengan lebih baik. Atau bisa juga melihat exokernel

  • https://genode.org/index
    Ini adalah sistem operasi dengan dukungan seL4

    • Saya penasaran apakah ada penggunaan Genode yang menonjol

  • Saya pernah memberikan presentasi tentang SeL4 di chapter OWASP lokal. Entah apakah materinya masih bisa ditemukan
    Proyek ini benar-benar dibuat dengan sangat baik, tetapi khususnya untuk komputasi serbaguna, saya ragu menyebutnya sebagai pengganti Linux. Bukan berarti microkernel secara umum buruk untuk penggunaan serbaguna. RedoxOS tampaknya belakangan ini mengalami sejumlah kemajuan, dan menggunakan microkernel yang ditulis dengan Rust

    • Masalahnya selalu “seberapa luas penggantian yang dimaksud”. Redox tampaknya berusaha menjaga interoperabilitas POSIX dengan baik, dan itu secara alami memengaruhi keputusan desain. Ada juga perbedaan besar antara memiliki kemampuan teknis dan meraih keberhasilan
      Meski begitu, jika Redox berhasil, itu saja sudah merupakan kemajuan yang baik. Pada seL4, karakteristik seperti ini lebih ekstrem. Keunggulan teknisnya sangat luar biasa, tetapi hingga kini, dan mungkin juga ke depannya, tampaknya tidak memiliki sesuatu yang diperlukan untuk menjadi ‘hal besar berikutnya’. Jika pertimbangan politik dikesampingkan, saya rasa microkernel akan berhasil, dan memang seharusnya begitu
    • Kemungkinan menggantikan Linux bergantung pada skenarionya. Tentu saja Linux lebih mudah ditangani, tetapi sebaliknya ada juga persyaratan yang hanya dapat dipenuhi oleh seL4
      Agar seL4 benar-benar berguna, dibutuhkan banyak hal di atasnya. Untungnya, banyak pekerjaan open source juga telah berjalan di bagian itu, dan posisinya jauh lebih baik dibanding beberapa tahun lalu
      Untuk skenario statis ada LionsOS[0], dan itu sudah cukup layak digunakan
      Untuk skenario dinamis ada Provably Secure, General-Purpose Operating System[1], tetapi masih dalam tahap awal
      Keduanya dapat ditemukan di halaman Projects milik trustworthy systems[2] yang ditautkan dari situs web seL4
      [0] https://trustworthy.systems/projects/LionsOS/
      [1] https://trustworthy.systems/projects/smos/
      [2] https://trustworthy.systems/projects/

  • Saya penasaran apakah OS yang berjalan di atas kernel ini juga harus diverifikasi secara formal agar jaminan keamanannya berlaku

    • Jaminan yang diberikan kernel tidak dapat dipatahkan oleh proses tak berprivilege yang berjalan di atasnya
      Tentu saja kernel saja tidak terlalu berguna, sehingga desain driver, server filesystem, dan layanan lain yang berjalan di atas kernel tetap penting
      Hal yang juga penting adalah bahwa sebagian besar sistem lain, termasuk Linux, memiliki cacat pada tingkat fundamental, sedangkan seL4 benar-benar memungkinkan pembuatan sistem yang aman dan tepercaya
    • Tidak. Keuntungannya adalah kernel menjamin isolasi, sehingga tidak perlu memercayai kernel dan proses
      Jadi, Anda bisa menjalankan kernel Linux di samping proses berkeamanan tinggi, sambil tetap memiliki jaminan bahwa keduanya terisolasi satu sama lain kecuali IPC yang diizinkan
    • Tidak
      Namun ada batasannya. DMA harus dimatikan, dan driver juga harus hanya menggunakan yang telah diverifikasi secara formal
      Penting juga bahwa kernel multicore seL4 belum diverifikasi
    • Dalam arti absolut, bisa dibilang begitu. Pada tingkat praktis, jawaban parsial dapat ditemukan di bagian 7.2 makalah tersebut

  • Helios Microkernel karya Drew DeVault juga layak dilihat. Katanya berbasis SeL4
    https://ares-os.org/docs/helios/

    • Ada perbedaan bermakna antara “berbasis” dan “terinspirasi oleh”, dan Helios tampaknya lebih dekat ke yang kedua

  • Di Universitas Karlsruhe, L4 cukup populer. Saya tidak pernah menelaahnya secara mendalam, tetapi kelihatannya seperti proyek yang lebih tertarik menguji ide-ide teoretis daripada membuat sesuatu yang berguna secara praktis
    Itu 20 tahun lalu, dan menurut saya sampai sekarang pun tidak banyak berubah. Dari pencarian cepat, tampaknya ada beberapa upaya membuat OS di atasnya, tetapi terlihat lebih dekat ke pembuktian konsep daripada penggunaan nyata

    • Jika melihat https://en.wikipedia.org/wiki/L4_microkernel_family, L4 digunakan di berbagai tempat, dan tampaknya terutama dipakai di lingkungan embedded
      “Pengiriman OKL4 melampaui 1,5 miliar unit pada awal 2012, sebagian besar berupa chip modem nirkabel Qualcomm. Penerapan lainnya mencakup sistem infotainment otomotif”
      “Prosesor Apple A-series mulai dari A7 menyertakan koprosesor Secure Enclave yang menjalankan sistem operasi L4; OS ini adalah sepOS yang berbasis kernel L4-embedded yang dikembangkan di NICTA pada 2006. Akibatnya, L4 terpasang di semua perangkat Apple modern, termasuk Mac yang memakai Apple silicon”
    • Jochen Liedtke menjadi profesor di Karlsruhe pada 1999, tetapi sayangnya meninggal dunia tidak lama kemudian pada 2001. Saya tidak tahu apakah penggantinya, Bellosa, masih melakukan riset L4. Ada proyek L4Ka, tetapi tampaknya sudah selesai. Dalam kuliah sistem operasi tingkat sarjana Bellosa, topik ini tidak termasuk dalam kurikulum
      Rittinghaus, alumnus Bellosa, terlibat dalam Unikraft[0], yang beberapa kali juga muncul di HN, dan menggunakan teknologi unikernel
      [0] https://unikraft.org/
    • iPhone menggunakan varian L4
      “Secure Enclave Processor menjalankan versi mikrokernel L4 yang dikustomisasi oleh Apple”
      https://support.apple.com/de-at/guide/security/sec59b0b31ff/...
    • Turunan open source, L4Re, berjalan pada ECU pusat “icas1” di semua kendaraan id.X Volkswagen, dan memuat Linux serta guest lainnya
      https://www.kernkonzept.com/kk_events/elektrobit-advances-au...
      Menurut saya, kernel L4Re juga merupakan bagian dari Elektrobit Safe Linux
    • Saya menyukai pekerjaan dan arah tim Karlsruhe pada L4Ka, khususnya Pistachio. Desainnya rapi, sederhana, dan mudah dipahami
      Untuk tesis kelulusan, saya membuat OS berbasis Pistachio. Saya selalu berpikir bahwa jika saya kuliah di Karlsruhe, mungkin saya akan masuk ke riset OS

  • Saya juga pernah punya ide desain sistem operasi, dan capability yang saya pertimbangkan menggunakan fungsi interposisi dan delegasi seperti seL4. Selain yang tertulis di sana, ada juga keunggulan lain. Misalnya, capability proxy dapat dipakai untuk menerapkan filter pada audio atau mewujudkan transparansi jaringan
    Saya pikir fungsi real-time bisa diizinkan sebagai implementasi opsional. Ide saya lebih dekat ke spesifikasi, bukan satu implementasi tunggal
    Fitur lain yang saya inginkan adalah semua program berperilaku deterministik kecuali untuk input/output. Tanpa input/output, program tidak bisa mengetahui tanggal/waktu atau waktu eksekusi program, dan juga tidak bisa memeriksa fitur prosesor. Jika menggunakan fitur yang tidak didukung perangkat keras, sistem operasi dapat mengemulasikannya
    Untuk mengimplementasikannya, saya berpikir memakai campuran dukungan perangkat keras dan dukungan perangkat lunak. Dalam dokumen itu ada catatan tentang serangan terhadap capability yang diimplementasikan di perangkat keras, tetapi karena saya tidak memiliki dokumen referensinya, saya tidak tahu apakah serangan itu juga berlaku pada cara yang saya pikirkan

  • Dari sudut pandang keamanan, ini tampaknya menunjukkan kegagalan yang sama seperti KVM pada kernel Linux. Jika hypervisor berada di ring 0, ada risiko escape dari satu VM ke VM lain atau ke host itu sendiri
    Saya penasaran bagaimana risiko itu dimitigasi

    • Dalam dukungan virtualisasi seL4, eksepsi VM diubah menjadi pesan, lalu ditangani oleh VMM, yaitu tugas yang berjalan dalam mode non-privileged
      VMM tidak memiliki capability lebih banyak daripada VM itu sendiri, sehingga selain dalam arti akademis, escape dari VM tidak bernilai
      Lihat halaman 8–10 pada PDF aslinya