La nouvelle a récemment éclaté que une proposition a été faite pour être inclus dans le noyau de Linux 5.20 (ou peut-être que la branche sera numérotée 6.0, tout dépend de la décision de Linus Torvalds en raison de son commentaire qu'il a fait sur la version 5.19 du noyau).
La proposition faite concerne un ensemble de patchs avec la mise en place du mécanisme RV (Runtime Verification), qui est un moyen de vérifier le bon fonctionnement dans des systèmes hautement fiables qui garantissent l'absence de pannes.
validation fait au moment de l'exécution en attachant des gestionnaires aux points de trace qui vérifient la progression réelle de l'exécution par rapport à un modèle de référence déterministe prédéfini de l'automate qui détermine le comportement attendu du système.
Développeur Linux, Daniel Bristot de Oliveira mentionne :
Au cours des dernières années, j'ai exploré la possibilité de vérifier le comportement du noyau Linux à l'aide de Runtime Verification.
La vérification d'exécution (RV) est une méthode légère (mais rigoureuse) qui complète les techniques de vérification exhaustives classiques (telles que la vérification de modèles et la preuve de théorèmes) avec une approche plus pratique des systèmes complexes. Au lieu de s'appuyer sur un modèle détaillé d'un système (par exemple, une réimplémentation d'un niveau d'instruction), la réalité virtuelle fonctionne en analysant la trace d'exécution réelle du système, en la comparant à une spécification formelle du comportement du système.
L'utilisation d'automates déterministes pour la réalité virtuelle est une approche bien établie. Dans le cas spécifique du noyau Linux, vous pouvez apprendre à modéliser le comportement complexe du noyau Linux avec cet article :
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. *Vérification formelle efficace pour le noyau Linux.* Dans : Conférence internationale sur le génie logiciel et les méthodes formelles. Springer, Cham, 2019. p. 315-332.
Et quelle est l'efficacité de cette approche ici :
De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *Un modèle de synchronisation de threads pour le noyau Linux PREEMPT_RT.* Journal of Systems Architecture, 2020, 107 : 101729.
TLDR : Un comportement complexe peut être modélisé de manière modulaire, avec un surcoût acceptable (même pour les systèmes de production).
Il est mentionné que les informations sur les points de suivi déplacent le modèle d'un état à un autre, et si le nouvel état ne correspond pas aux paramètres du modèle, un avertissement est généré ou le noyau entre dans un état de "panique" (en supposant que des systèmes hautement fiables détecteront et répondront à de telles situations).
Le modèle de l'automate définit les transitions d'un état à un autre est exporté au format "dot" (graphviz), après quoi il est traduit à l'aide de l'utilitaire dot2c en une représentation C, qui est chargée sous la forme d'un module noyau qui suit les déviations. exécution à partir d'un modèle prédéfini.
La vérification des modèles à l'exécution se positionne comme une méthode plus légère et plus simple à mettre en œuvre pour vérifier l'exactitude de l'exécution dans les systèmes critiques, qui complète les méthodes classiques de vérification de la fiabilité, telles que la vérification des modèles et les tests mathématiques de conformité du code aux spécifications données dans un langage formel.
Le mainteneur du sous-système de suivi, Steven Rostedt, l'a résumé ainsi :
» C'est le plus gros changement pour cette pull request. Introduit la vérification d'exécution requise pour exécuter Linux sur des systèmes critiques pour la sécurité. Il permet d'insérer des modèles d'automates déterministes dans le noyau pour les attacher à des points de trace, où les informations sur ces points de trace feront passer le modèle d'un état à un autre.
Parmi les avantages mentionnés de RV, il y a la capacité de fournir une vérification rigoureuse sans implémentation séparée de l'ensemble du système dans un langage de modélisation, ainsi qu'une réponse flexible aux événements imprévus, par exemple, pour bloquer la propagation de la défaillance des systèmes critiques.
Enfin, si vous souhaitez en savoir plus, vous pouvez consulter les détails dans la lien suivant
source: https://www.phoronix.com/