Fitur tiket besar lainnya telah dibuat untuk kernel Linux 6.0: infrastruktur Verifikasi Runtime untuk menjalankan Linux pada sistem yang kritis terhadap keselamatan. Pengembang Linux Daniel Bristot de Oliveira telah menjelajahi Verifikasi Runtime untuk Linux selama beberapa tahun terakhir dan implementasinya akan digarisbawahi sebagai bagian dari pembaruan penelusuran di kernel berikutnya ini. Dia menyimpulkan fitur ini sebagai: Selama beberapa tahun terakhir, saya telah menjajaki kemungkinan memverifikasi perilaku kernel Linux menggunakan Verifikasi Runtime. Runtime Verification (RV) adalah metode ringan (namun ketat) yang melengkapi teknik verifikasi lengkap klasik (seperti pemeriksaan model dan pembuktian teorema) dengan pendekatan yang lebih praktis untuk sistem yang kompleks. Alih-alih mengandalkan model sistem yang halus (misalnya, implementasi ulang tingkat instruksi), RV bekerja dengan menganalisis jejak eksekusi aktual sistem, membandingkannya dengan spesifikasi formal dari perilaku sistem. Penggunaan otomat deterministik untuk RV adalah pendekatan yang mapan. Dalam kasus spesifik kernel Linux, Anda dapat memeriksa cara memodelkan perilaku kompleks kernel Linux dengan makalah ini: De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. *Verifikasi formal yang efisien untuk kernel Linux.* Dalam: Konferensi Internasional tentang Rekayasa Perangkat Lunak dan Metode Formal. Springer, Cham, 2019. hal. 315-332. Dan seberapa efisien pendekatan ini di sini: De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *Model sinkronisasi utas untuk kernel PREEMPT_RT Linux.* Jurnal Arsitektur Sistem, 2020, 107: 101729. TLDR: dimungkinkan untuk memodelkan perilaku kompleks dengan cara modular, dengan overhead yang dapat diterima (bahkan untuk sistem produksi). dokumentasi dasar tentang Verifikasi Runtime (RV) ini bagi mereka yang tertarik dengan penggunaan Linux pada sistem real-time yang kritis terhadap keamanan. Linux menjadi semakin banyak digunakan dalam sistem kritis keamanan. Pemelihara subsistem
Tracing Steven Rostedt menyimpulkannya sebagai, "Ini adalah perubahan terbesar untuk permintaan tarik ini. Ini memperkenalkan verifikasi runtime yang diperlukan untuk menjalankan Linux pada sistem kritis keamanan. Ini memungkinkan untuk model automata deterministik untuk dimasukkan ke dalam kernel yang akan dilampirkan ke tracepoint, dimana informasi pada tracepoint ini akan memindahkan model dari state ke state. Jika ditemui state yang bukan milik model, maka akan mengaktifkan reaktor yang diberikan , yang hanya dapat memberi tahu pengguna atau bahkan membuat panik kernel (yang akan dideteksi dan dipulihkan oleh sistem kritis keamanan)."
Dukungan Runtime Verification adalah bagian dari pull request yang tertunda ini.
Above juga merupakan presentasi Red Hat Research tentang upaya Verifikasi Runtime dan dek slide PDF yang menyertainya.
Itulah berita seputar Linux 6.0 Menambahkan Verifikasi Run-Time Untuk Berjalan Pada Sistem Kritis Keselamatan, semoga bermanfaat. Disadur dari Phoronix.com.
