Lajmi u bë i ditur së fundmi është bërë një propozim për t'u përfshirë bërthama e Linux 5.20 (ose ndoshta dega do të numërohet 6.0, gjithçka varet nga vendimi i Linus Torvalds për shkak të komentit të tij që bëri në lëshimin e Kernel 5.19).
Propozimi i bërë ka të bëjë me një grup arnash me zbatimin e mekanizmit RV (Runtime Verification), i cili është një mjet për të verifikuar funksionimin e saktë në sisteme shumë të besueshme që garantojnë mungesën e dështimeve.
vërtetimi bëhet në kohën e ekzekutimit duke i bashkangjitur mbajtësit në pikat e gjurmës që kontrollojnë ecurinë aktuale të ekzekutimit kundrejt një modeli referimi të paracaktuar përcaktues të automatit që përcakton sjelljen e pritshme të sistemit.
Zhvillues Linux, Daniel Bristot de Oliveira përmend:
Për vitet e fundit, unë kam eksploruar mundësinë e verifikimit të sjelljes së kernelit Linux duke përdorur Verifikimin në kohëzgjatje.
Verifikimi në kohëzgjatje (RV) është një metodë e lehtë (por rigoroze) që plotëson teknikat klasike shteruese të verifikimit (të tilla si kontrolli i modelit dhe vërtetimi i teoremës) me një qasje më praktike ndaj sistemeve komplekse. Në vend që të mbështetet në një model të detajuar të një sistemi (për shembull, një rizbatim i një niveli instruksioni), VR funksionon duke analizuar gjurmën aktuale të ekzekutimit të sistemit, duke e krahasuar atë me një specifikim formal të sjelljes së sistemit.
Përdorimi i automatave përcaktuese për VR është një qasje e mirëpërcaktuar. Për rastin specifik të kernelit Linux, mund të mësoni se si të modeloni sjelljen komplekse të kernelit Linux me këtë artikull:
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. *Verifikim efektiv zyrtar për kernelin Linux.* Në: Konferenca Ndërkombëtare për Inxhinierinë e Softuerit dhe Metodat Formale. Springer, Çam, 2019. f. 315-332.
Dhe sa efikase është kjo qasje këtu:
De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *Një model sinkronizimi i fijeve për kernelin PREEMPT_RT Linux.* Journal of Systems Architecture, 2020, 107: 101729.
TLDR: Sjellja komplekse mund të modelohet në një mënyrë modulare, me shpenzime të larta të pranueshme (madje edhe për sistemet e prodhimit).
Përmendet se informacioni i pikës së gjurmës e zhvendos modelin nga një gjendje në tjetrën, dhe nëse gjendja e re nuk përputhet me parametrat e modelit, gjenerohet një paralajmërim ose kerneli hyn në një gjendje "paniku" (duke supozuar se sistemet shumë të besueshme do të zbulojnë dhe reagojnë ndaj situatave të tilla).
Modeli i automatit përcakton kalimet nga një gjendje në tjetrën eksportohet në formatin "pik". (graphviz), pas së cilës përkthehet duke përdorur mjetin dot2c në një paraqitje C, e cila ngarkohet në formën e një moduli kernel që gjurmon devijimet. ekzekutimi nga një model i paracaktuar.
Kontrollimi i modeleve në kohën e ekzekutimit pozicionohet si një metodë më e lehtë dhe më e lehtë të zbatohet për të verifikuar korrektësinë e ekzekutimit në sistemet kritike të misionit, i cili plotëson metodat klasike të verifikimit të besueshmërisë, të tilla si verifikimi i modelit dhe provat matematikore të përputhshmërisë së kodit me specifikimet e dhëna në një gjuhë zyrtare.
Mbajtësi i nënsistemit të gjurmimit Steven Rostedt e përmblodhi kështu:
» Ky është ndryshimi më i madh për këtë kërkesë tërheqëse. Prezanton verifikimin e kohës së funksionimit që kërkohet për të ekzekutuar Linux në sistemet kritike për sigurinë. Ai lejon që modelet përcaktuese të automatave të futen në kernel për t'u bashkangjitur në pikat e gjurmës, ku informacioni rreth këtyre pikave të gjurmës do të lëvizë modelin nga një gjendje në tjetrën.
Ndër avantazhet e përmendura të RV është aftësia për të siguruar verifikim rigoroz pa një zbatim të veçantë të të gjithë sistemit në një gjuhë modelimi, si dhe një përgjigje fleksibël ndaj ngjarjeve të paparashikuara, për shembull, për të bllokuar përhapjen e dështimit të sistemeve kritike.
Së fundi, nëse jeni të interesuar të jeni në gjendje të dini më shumë rreth tij, mund të konsultoni detajet në lidhja vijuese.
Fuente: https://www.phoronix.com/