Для Linux запропоновано механізм верифікації коректності роботи ядра

Для включення до складу ядра Linux 5.20 (можливо, гілка отримає номер 6.0) запропоновано набір патчів з реалізацією механізму RV (Runtime Verification), що є засобом для перевірки коректності роботи на високонадійних системах, що гарантують відсутність збоїв. Перевірка проводиться під час виконання через прикріплення обробників до точок трасування, що звіряють фактичний хід виконання із заздалегідь визначеною еталонною детермінованою моделлю автомата, що визначає очікувану поведінку системи.

Інформація від точок трасування переводить модель з одного стану в інший, і якщо новий стан не відповідає параметрам моделі, генерується попередження або ядро ​​переводиться в стан panic (маю на увазі, що високонадійні системи будуть визначати подібні ситуації і реагувати на них). Модель автомата, що визначає переходи з одного стану в інший, експортується у формат «dot» (graphviz), після чого транслюється за допомогою утиліти dot2c у виставу мовою Сі, яке завантажується у формі модуля ядра, що відстежує відхилення ходу виконання від певної моделі.

Для Linux запропоновано механізм верифікації коректності роботи ядра

Звірка з моделлю під час виконання позиціонується як більш легкий та простий для реалізації на практиці спосіб підтвердження коректності виконання на критично важливих системах, що доповнює класичні методи підтвердження надійності, такі як перевірка моделі та математичні докази відповідності коду специфікаціям, заданим формальною мовою. З переваг RV називається можливість забезпечити сувору верифікацію без окремої реалізації всієї системи мовою моделювання, а також гнучке реагування на непередбачувані події, наприклад, для блокування подальшого поширення збою в критично важливих системах.

Джерело: opennet.ru

Додати коментар або відгук