Nedávno to prelomila správa bol predložený návrh, ktorý sa má zahrnúť jadro Linux 5.20 (alebo možno bude mať vetva číslo 6.0, všetko závisí od rozhodnutia Linusa Torvaldsa vzhľadom na jeho komentár k vydaniu jadra 5.19).
Predložený návrh je o súbor záplat s implementáciou mechanizmu RV (Runtime Verification), čo je prostriedok na overenie správnej činnosti vo vysoko spoľahlivých systémoch, ktoré zaručujú absenciu porúch.
validácia vykonávané za behu pripojením obslužných programov k bodom sledovania ktoré kontrolujú skutočný priebeh vykonávania oproti vopred definovanému deterministickému referenčnému modelu automatu, ktorý určuje očakávané správanie systému.
Linuxový vývojár, Daniel Bristot de Oliveira spomína:
Posledných pár rokov som skúmal možnosť overenia správania sa linuxového jadra pomocou Runtime Verification.
Runtime Verification (RV) je nenáročná (ale dôsledná) metóda, ktorá dopĺňa klasické vyčerpávajúce overovacie techniky (ako je kontrola modelov a overovanie teorémov) s praktickým prístupom ku komplexným systémom. Namiesto spoliehania sa na podrobný model systému (napríklad reimplementácia úrovne inštrukcií), VR funguje tak, že analyzuje aktuálnu stopu vykonávania systému a porovnáva ju s formálnou špecifikáciou správania systému.
Použitie deterministických automatov pre VR je dobre zavedený prístup. Pre konkrétny prípad linuxového jadra sa v tomto článku môžete naučiť, ako modelovať komplexné správanie linuxového jadra:
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. *Efektívne formálne overenie pre jadro Linuxu.* In: International Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. s. 315-332.
A aký efektívny je tento prístup tu:
De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *Model synchronizácie vlákien pre linuxové jadro PREEMPT_RT.* Journal of Systems Architecture, 2020, 107: 101729.
TLDR: Komplexné správanie je možné modelovať modulárnym spôsobom s prijateľnou réžiou (aj pre produkčné systémy).
Je to spomenuté informácie o bode trasy presúvajú model z jedného stavu do druhéhoa ak nový stav nezodpovedá parametrom modelu, vygeneruje sa varovanie alebo jadro prejde do stavu „panika“ (za predpokladu, že vysoko spoľahlivé systémy takéto situácie zaznamenajú a zareagujú na ne).
Model automatu definuje prechody z jedného stavu do druhého sa exportuje do „bodkového“ formátu (graphviz), po ktorom sa preloží pomocou utility dot2c do reprezentácie C, ktorá sa načíta vo forme modulu jadra, ktorý sleduje odchýlky. prevedenie z preddefinovaného modelu.
Kontrola modelov za behu je umiestnená ako ľahšia a jednoduchšia metóda implementovať na overenie správnosti vykonávania v kritických systémoch, ktoré dopĺňa klasické metódy overovania spoľahlivosti, ako je overenie modelu a matematické dôkazy zhody kódu so špecifikáciami uvedenými vo formálnom jazyku.
Správca subsystému sledovania Steven Rostedt to zhrnul takto:
» Toto je najväčšia zmena pre túto požiadavku na stiahnutie. Zavádza verifikáciu runtime, ktorá je potrebná na spustenie Linuxu na systémoch kritických z hľadiska bezpečnosti. Umožňuje vložiť modely deterministických automatov do jadra na pripojenie k sledovacím bodom, kde informácie o týchto sledovacích bodoch presunú model z jedného stavu do druhého.
Medzi spomínané výhody RV patrí schopnosť zabezpečiť dôslednú verifikáciu bez samostatnej implementácie celého systému v modelovacom jazyku, ako aj flexibilná reakcia na nepredvídané udalosti, napríklad blokovanie šírenia zlyhania kritických systémov.
Nakoniec, ak máte záujem dozvedieť sa o ňom viac, podrobnosti si môžete prečítať v nasledujúci odkaz.
Fuente: https://www.phoronix.com/