Недавно в новостях сообщили, что поступило предложение о включении ядро Linux 5.20 (или, может быть, ветка будет иметь номер 6.0, все зависит от решения Линуса Торвальдса из-за его комментария к выпуску ядра 5.19).
Внесенное предложение касается набор патчей с реализацией механизма RV (Runtime Verification), которая является средством проверки правильности работы в высоконадежных системах, гарантирующим отсутствие сбоев.
Проверка делается во время выполнения путем присоединения обработчиков к точкам трассировки которые проверяют фактический ход выполнения по предопределенной детерминированной эталонной модели автомата, которая определяет ожидаемое поведение системы.
Linux-разработчик, Даниэль Бристо де Оливейра упоминает:
Последние несколько лет я изучал возможность проверки поведения ядра Linux с помощью Runtime Verification.
Проверка во время выполнения (RV) — это упрощенный (но строгий) метод, который дополняет классические исчерпывающие методы проверки (такие как проверка моделей и доказательство теорем) более практическим подходом к сложным системам. Вместо того, чтобы полагаться на подробную модель системы (например, повторную реализацию уровня инструкций), VR работает, анализируя фактическую трассировку выполнения системы, сравнивая ее с формальной спецификацией поведения системы.
Использование детерминированных автоматов для виртуальной реальности — хорошо зарекомендовавший себя подход. Для конкретного случая ядра Linux вы можете узнать, как смоделировать сложное поведение ядра Linux, из этой статьи:
Де Оливейра, Даниэль Бристо; Кучинотта, Томмазо; Де Оливейра, Ромуло Силва. *Эффективная формальная проверка ядра Linux.* В: Международная конференция по программной инженерии и формальным методам. Спрингер, Чам, 2019. с. 315-332.
И насколько эффективен этот подход здесь:
Де Оливейра, Даниэль Б .; Де Оливейра, Ромуло С.; Кучинотта, Томмазо. *Модель синхронизации потоков для ядра Linux PREEMPT_RT.* Journal of Systems Architecture, 2020, 107: 101729.
TLDR: сложное поведение может быть смоделировано модульным способом с приемлемыми накладными расходами (даже для производственных систем).
Упоминается, что информация о точках отслеживания перемещает модель из одного состояния в другое, и если новое состояние не соответствует параметрам модели, генерируется предупреждение или ядро переходит в состояние «паники» (при условии, что высоконадежные системы будут обнаруживать такие ситуации и реагировать на них).
Модель автомата определяет переходы из одного состояния в другое экспортируется в "точечный" формат (graphviz), после чего с помощью утилиты dot2c транслируется в C-представление, которое загружается в виде модуля ядра, отслеживающего отклонения. выполнение по заранее заданной модели.
Проверка моделей во время выполнения позиционируется как более легкий и простой метод. реализовать проверку правильности выполнения в критически важных системах, что дополняет классические методы проверки надежности, такие как проверка моделей и математические доказательства соответствия кода спецификациям, заданным на формальном языке.
Специалист по сопровождению подсистемы слежения Стивен Ростедт резюмировал это следующим образом:
» Это самое большое изменение для этого запроса на вытягивание. Вводит проверку во время выполнения, которая необходима для запуска Linux в критически важных с точки зрения безопасности системах. Он позволяет вставлять модели детерминированных автоматов в ядро и привязывать их к точкам трассировки, где информация об этих точках трассировки будет перемещать модель из одного состояния в другое.
Среди упомянутых достоинств РВ — возможность обеспечить строгую проверку без отдельной реализации всей системы на языке моделирования, а также гибкая реакция на непредвиденные события, например, блокировать распространение отказа критических систем.
Наконец, если вы заинтересованы в том, чтобы узнать больше об этом, вы можете ознакомиться с подробностями в по следующей ссылке.
источник: https://www.phoronix.com/