Pekerjaan verifikasi matematis formal terhadap keandalan dan keamanan mikrokernel seL4 pada sistem dengan arsitektur set instruksi AArch64 telah selesai. Verifikasi terdiri dari bukti matematis tentang kebenaran operasi seL4, yang menunjukkan kepatuhan penuh terhadap spesifikasi yang didefinisikan dalam bahasa formal. Bukti keandalan ini memungkinkan penggunaan seL4 dalam sistem penting berbasis prosesor ARM64 yang membutuhkan tingkat keamanan tinggi dan menjamin tidak adanya kegagalan.
Mikrokernel seL4 awalnya diverifikasi untuk prosesor ARM 32-bit, dan kemudian untuk prosesor x86 dan RISC-V 64-bit. Verifikasi memastikan bahwa jika terjadi kegagalan di satu bagian sistem, kegagalan tersebut tidak akan menyebar ke bagian sistem lainnya dan komponen-komponen pentingnya. Dalam konteks keamanan, verifikasi menegaskan bahwa kernel menyediakan tingkat isolasi aplikasi yang sesuai, mencegah aplikasi mengakses informasi tanpa otorisasi, dan memastikan bahwa jika aplikasi sekunder dikompromikan, serangan tersebut tidak akan menyebar ke aplikasi-aplikasi penting.
Arsitektur mikrokernel seL4 terkenal karena pemindahan manajemen sumber daya kernel ke ruang pengguna dan penerapan mekanisme kontrol akses yang sama untuk sumber daya ini seperti untuk sumber daya pengguna. Mikrokernel tidak menyediakan abstraksi tingkat tinggi yang siap pakai untuk mengelola berkas, proses, koneksi jaringan, dan sebagainya; melainkan, hanya menyediakan mekanisme minimal untuk mengelola akses ke ruang alamat fisik, interupsi, dan sumber daya prosesor. Abstraksi tingkat tinggi dan driver untuk berinteraksi dengan perangkat keras diimplementasikan secara terpisah di atas mikrokernel sebagai tugas yang berjalan di tingkat pengguna. Akses ke sumber daya mikrokernel oleh tugas-tugas ini diatur melalui definisi aturan.
Sumber: opennet.ru
