Vestea a spus asta recent a fost făcută o propunere pentru a fi inclusă în miezul de Linux 5.20 (sau poate că ramura va fi numerotată 6.0, totul depinde de decizia lui Linus Torvald datorită comentariului său pe care l-a făcut cu privire la lansarea Kernel 5.19).
Propunerea făcută este despre un set de patch-uri cu implementarea mecanismului RV (Runtime Verification), care este un mijloc de verificare a funcționării corecte în sisteme extrem de fiabile care garantează absența defecțiunilor.
validare realizat la runtime prin atașarea handlerelor la punctele de urmărire care verifică progresul real al execuției față de un model de referință determinist predefinit al automatului care determină comportamentul așteptat al sistemului.
Dezvoltator Linux, Daniel Bristot de Oliveira menționează:
În ultimii ani, am explorat posibilitatea de a verifica comportamentul nucleului Linux folosind Runtime Verification.
Runtime Verification (RV) este o metodă ușoară (dar riguroasă) care completează tehnicile clasice de verificare exhaustivă (cum ar fi verificarea modelului și demonstrarea teoremei) cu o abordare mai practică a sistemelor complexe. În loc să se bazeze pe un model detaliat al unui sistem (de exemplu, o reimplementare a unui nivel de instrucțiune), VR funcționează prin analizarea urmei efective de execuție a sistemului, comparând-o cu o specificație formală a comportamentului sistemului.
Utilizarea automatelor deterministe pentru VR este o abordare bine stabilită. În cazul specific al nucleului Linux, puteți afla cum să modelați comportamentul complex al nucleului Linux cu acest articol:
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. *Verificare formală eficientă pentru kernel-ul Linux.* În: Conferința Internațională despre Inginerie Software și Metode Formale. Springer, Cham, 2019. p. 315-332.
Și cât de eficientă este această abordare aici:
De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *Un model de sincronizare a firelor de execuție pentru kernel-ul Linux PREEMPT_RT.* Journal of Systems Architecture, 2020, 107: 101729.
TLDR: Comportamentul complex poate fi modelat într-un mod modular, cu supraîncărcare acceptabilă (chiar și pentru sistemele de producție).
Se menționează că informațiile despre punctul de urmărire mută modelul dintr-o stare în alta, iar dacă noua stare nu se potrivește cu parametrii modelului, se generează un avertisment sau nucleul intră într-o stare de „panică” (presupunând că sistemele foarte fiabile vor detecta și vor răspunde la astfel de situații).
Modelul automatului definește tranzițiile de la o stare la alta este exportat în format „punct”. (graphviz), după care este tradus folosind utilitarul dot2c într-o reprezentare C, care este încărcată sub forma unui modul kernel care urmărește abaterile. execuție dintr-un model predefinit.
Verificarea modelelor în timpul rulării este poziționată ca o metodă mai ușoară și mai ușoară să implementeze pentru a verifica corectitudinea execuției în sistemele critice de misiune, care completează metodele clasice de verificare a fiabilității, cum ar fi verificarea modelului și dovezile matematice ale conformității codului cu specificațiile date într-un limbaj formal.
Menținătorul subsistemului de urmărire Steven Rostedt a rezumat-o astfel:
» Aceasta este cea mai mare schimbare pentru această solicitare de extragere. Introduce verificarea timpului de execuție care este necesară pentru a rula Linux pe sisteme critice pentru securitate. Acesta permite ca modelele de automate deterministe să fie inserate în nucleu pentru a fi atașate la punctele de urmărire, unde informațiile despre aceste puncte de urmărire vor muta modelul de la o stare la alta.
Printre avantajele menționate ale RV se numără capacitatea de a oferi o verificare riguroasă fără o implementare separată a întregului sistem într-un limbaj de modelare, precum și un răspuns flexibil la evenimente neprevăzute, de exemplu, pentru a bloca propagarea defecțiunilor sistemelor critice.
În fine, dacă sunteți interesat să puteți afla mai multe despre acesta, puteți consulta detaliile în următorul link.
Fuente: https://www.phoronix.com/