Pikeun dilebetkeun kana kernel Linux 5.20 (panginten cabangna bakal dinomerkeun 6.0), sakumpulan patch parantos diusulkeun kalayan palaksanaan mékanisme RV (Runtime Verification), anu mangrupikeun alat pikeun mariksa operasi anu leres dina sistem anu dipercaya pisan. anu ngajamin henteuna gagal. Validasi dipigawé dina runtime ku ngagantelkeun pawang ka tracepoints nu mariksa kamajuan sabenerna palaksanaan ngalawan model deterministik rujukan predetermined tina otomat anu nangtukeun kabiasaan ekspektasi sistem.
Inpormasi tina tracepoints mindahkeun modél ti hiji kaayaan ka kaayaan anu sanés, sareng upami kaayaan énggal henteu cocog sareng parameter modél, peringatan bakal dibangkitkeun atanapi kernel disimpen kana kaayaan "panik" (kahartos yén sistem anu dipercaya pisan bakal ngadeteksi kaayaan sapertos sareng ngabales aranjeunna). Modél otomat anu ngahartikeun transisi tina hiji kaayaan ka kaayaan anu sanés diékspor kana format "titik" (graphviz), saatos éta ditarjamahkeun nganggo utilitas dot2c kana perwakilan C, anu dimuat dina bentuk modul kernel anu ngalacak simpangan. tina kamajuan palaksanaan tina modél anu tos siap.
Pamariksaan modél run-time diposisikan salaku metode anu langkung énténg sareng gampang diimplementasikeun pikeun pariksa kabeneran palaksanaan dina sistem misi-kritis, ngalengkepan metodeu klasik pikeun verifikasi réliabilitas, sapertos pamariksaan modél sareng bukti matematis patuh kode sareng spésifikasi anu dipasihkeun. dina basa formal. Diantara kaunggulan RV nyaéta kamampuhan pikeun nyadiakeun verifikasi rigorous tanpa palaksanaan misah tina sakabéh sistem dina basa modeling, kitu ogé respon fléksibel kana acara teu kaduga, Contona, pikeun meungpeuk rambatan salajengna tina gagalna dina sistem kritis.
sumber: opennet.ru