Pre Linux bol navrhnutý mechanizmus na overenie správneho fungovania jadra

Na zahrnutie do linuxového jadra 5.20 (možno vetva bude mať číslo 6.0) sa navrhuje sada opráv s implementáciou mechanizmu RV (Runtime Verification), ktorý poskytuje nástroje na kontrolu správnej činnosti na vysoko spoľahlivých systémoch, ktoré zaručujú absencia porúch. Overenie sa vykonáva za behu tak, že sa k bodom sledovania pripájajú obslužné programy, ktoré kontrolujú skutočný priebeh vykonávania oproti vopred určenému referenčnému deterministickému modelu automatu, ktorý definuje očakávané správanie systému.

Informácie zo sledovacích bodov posúvajú model z jedného stavu do druhého a ak nový stav nezodpovedá parametrom modelu, vygeneruje sa varovanie alebo sa jadro dostane do stavu „panika“ (od systémov s vysokou spoľahlivosťou sa očakáva, že zistia a reagovať na takéto situácie). Model automatu, ktorý definuje prechody z jedného stavu do druhého, sa exportuje do formátu „dot“ (graphviz), potom sa pomocou pomôcky dot2c preloží do reprezentácie C, ktorá sa načíta vo forme modulu jadra, ktorý sleduje odchýlky postupu vykonávania od preddefinovaného modelu.

Pre Linux bol navrhnutý mechanizmus na overenie správneho fungovania jadra

Kontrola modelu za chodu je umiestnená ako ľahšia a ľahšie implementovateľná metóda overovania správneho vykonávania na kritických systémoch, ktorá dopĺňa klasické metódy overovania spoľahlivosti, ako je kontrola modelu a matematické dôkazy zhody kódu so špecifikáciami uvedenými vo formálnom Jazyk. Medzi výhody RV patrí možnosť prísnej verifikácie bez samostatnej implementácie celého systému v modelovacom jazyku, ako aj flexibilná reakcia na nepredvídané udalosti, napríklad blokovanie ďalšieho šírenia poruchy v kritických systémoch.

Zdroj: opennet.ru

Pridať komentár