To su nedavno objavile vijesti dat je prijedlog za uključivanje jezgro od Linux 5.20 (ili će možda grana biti označena brojem 6.0, sve zavisi od odluke Linusa Torvaldsa zbog njegovog komentara koji je dao na izdanje Kernel 5.19).
Prijedlog je o set zakrpa sa implementacijom RV mehanizma (Runtime Verification), što je sredstvo za verifikaciju ispravnog rada u visoko pouzdanim sistemima koji garantuju odsustvo kvarova.
validacija urađeno u vrijeme izvođenja pričvršćivanjem rukovalaca na tačke praćenja koji provjeravaju stvarni napredak izvršenja u odnosu na unaprijed definirani deterministički referentni model automata koji određuje očekivano ponašanje sistema.
Linux programer, Daniel Bristot de Oliveira spominje:
Proteklih nekoliko godina istražujem mogućnost provjere ponašanja Linux kernela pomoću Runtime Verifikacije.
Runtime Verification (RV) je lagana (ali rigorozna) metoda koja dopunjuje klasične tehnike iscrpne verifikacije (kao što su provjera modela i dokazivanje teorema) s praktičnijim pristupom složenim sistemima. Umjesto da se oslanja na detaljan model sistema (na primjer, ponovna implementacija nivoa instrukcija), VR radi tako što analizira stvarni trag izvršenja sistema, upoređujući ga sa formalnom specifikacijom ponašanja sistema.
Upotreba determinističkih automata za VR je dobro uspostavljen pristup. Za konkretan slučaj Linux kernela, možete naučiti kako modelirati složeno ponašanje Linux kernela u ovom članku:
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. *Efikasna formalna verifikacija za Linux kernel.* U: Međunarodna konferencija o softverskom inženjerstvu i formalnim metodama. Springer, Cham, 2019. str. 315-332.
I koliko je ovaj pristup efikasan ovdje:
De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *Model sinhronizacije niti za PREEMPT_RT Linux kernel.* Journal of Systems Architecture, 2020, 107: 101729.
TLDR: Složeno ponašanje se može modelirati na modularan način, sa prihvatljivim troškovima (čak i za proizvodne sisteme).
To se spominje informacije o tački praćenja pomiču model iz jednog stanja u drugo, i ako novo stanje ne odgovara parametrima modela, generira se upozorenje ili kernel ulazi u stanje "panike" (pod pretpostavkom da će visoko pouzdani sistemi otkriti i odgovoriti na takve situacije).
Model automata definira prelaze iz jednog stanja u drugo se izvozi u "tačkasti" format (graphviz), nakon čega se prevodi pomoću dot2c uslužnog programa u C reprezentaciju, koja se učitava u obliku kernel modula koji prati odstupanja. izvođenje iz unaprijed definiranog modela.
Provjera modela u vrijeme rada pozicionirana je kao lakša i lakša metoda implementirati za verifikaciju ispravnosti izvršavanja u kritičnim sistemima, što dopunjuje klasične metode verifikacije pouzdanosti, kao što su verifikacija modela i matematički dokazi usklađenosti koda sa specifikacijama datim na formalnom jeziku.
Održavač podsistema za praćenje Steven Rostedt sažeo je to ovako:
» Ovo je najveća promjena za ovaj zahtjev za povlačenjem. Uvodi verifikaciju vremena izvođenja koja je potrebna za pokretanje Linuxa na sigurnosnim kritičnim sistemima. Omogućava da se deterministički modeli automata umetnu u jezgro i prikače na tačke praćenja, gdje će informacije o tim tačkama praćenja premjestiti model iz jednog stanja u drugo.
Među pomenutim prednostima RV-a je i mogućnost da se obezbedi rigorozna verifikacija bez odvojene implementacije celog sistema u jeziku modeliranja, kao i fleksibilan odgovor na nepredviđene događaje, na primer, da se blokira širenje kvara kritičnih sistema.
Konačno, ako ste zainteresovani da saznate više o tome, možete pogledati detalje u sljedeći link.
Izvor: https://www.phoronix.com/