{"id":104790,"date":"2022-08-07T21:36:50","date_gmt":"2022-08-07T19:36:51","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra"},"modified":"2022-08-07T21:36:50","modified_gmt":"2022-08-07T19:36:51","slug":"dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","status":"publish","type":"post","link":"https:\/\/prohoster.info\/fr\/blog\/news\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","title":{"rendered":"Un m\u00e9canisme de v\u00e9rification de l'int\u00e9grit\u00e9 du noyau a \u00e9t\u00e9 propos\u00e9 pour Linux.","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Pour l'inclusion dans le noyau Linux 5.20 (il est possible que la branche porte le num\u00e9ro 6.0), un ensemble de patches a \u00e9t\u00e9 propos\u00e9 pour la mise en \u0153uvre du m\u00e9canisme RV (Runtime Verification), repr\u00e9sentant des moyens pour v\u00e9rifier la pr\u00e9cision du fonctionnement sur des syst\u00e8mes tr\u00e8s fiables, garantissant l'absence de d\u00e9faillances. La v\u00e9rification est effectu\u00e9e lors de l'ex\u00e9cution par l'attachement de gestionnaires \u00e0 des points de tra\u00e7age, comparant le d\u00e9roulement r\u00e9el de l'ex\u00e9cution avec un mod\u00e8le d\u00e9terministe de r\u00e9f\u00e9rence pr\u00e9alablement d\u00e9fini, qui d\u00e9termine le comportement attendu du syst\u00e8me. <\/p>\n
Les informations des points de tra\u00e7age transforment le mod\u00e8le d'un \u00e9tat \u00e0 un autre, et si le nouvel \u00e9tat ne correspond pas aux param\u00e8tres du mod\u00e8le, un avertissement est g\u00e9n\u00e9r\u00e9 ou le noyau est transf\u00e9r\u00e9 dans un \u00e9tat \u00ab panic \u00bb (il est sous-entendu que les syst\u00e8mes hautement fiables identifieront de telles situations et y r\u00e9agiront). Le mod\u00e8le de l'automate, qui d\u00e9finit les transitions d'un \u00e9tat \u00e0 un autre, est export\u00e9 au format \u00ab dot \u00bb (graphviz), puis traduit \u00e0 l'aide de l'outil dot2c en une repr\u00e9sentation en langage C, qui est charg\u00e9e sous la forme d'un module de noyau surveillant les \u00e9carts d'ex\u00e9cution par rapport au mod\u00e8le pr\u00e9d\u00e9fini.
<\/center> <\/p>\n
La v\u00e9rification avec le mod\u00e8le lors de l'ex\u00e9cution est positionn\u00e9e comme une m\u00e9thode plus l\u00e9g\u00e8re et plus facile \u00e0 mettre en \u0153uvre dans la pratique, permettant de confirmer la pr\u00e9cision de l'ex\u00e9cution sur des syst\u00e8mes critiques, compl\u00e9tant les m\u00e9thodes classiques de validation de la fiabilit\u00e9, telles que la v\u00e9rification du mod\u00e8le et les preuves math\u00e9matiques de conformit\u00e9 du code aux sp\u00e9cifications d\u00e9finies dans un langage formel. Parmi les avantages du RV, on mentionne la possibilit\u00e9 d'assurer une v\u00e9rification rigoureuse sans avoir \u00e0 impl\u00e9menter enti\u00e8rement le syst\u00e8me dans un langage de mod\u00e9lisation, ainsi qu'une r\u00e9ponse flexible aux \u00e9v\u00e9nements impr\u00e9vus, par exemple, pour bloquer la propagation d'une d\u00e9faillance dans des syst\u00e8mes critiques. \n Source : opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"
![\"Un](\"\/wp-content\/uploads\/2022\/08\/56f02964c804a17b5cf5d811b2777368.jpg\")
<\/center> <\/p>\n