{"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\/sv\/blog\/news\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","title":{"rendered":"En mekanism f\u00f6r verifiering av k\u00e4rnans korrekthet har f\u00f6reslagits f\u00f6r Linux","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
F\u00f6r att inkludera i k\u00e4rnan av Linux 5.20 (det \u00e4r m\u00f6jligt att grenen f\u00e5r nummer 6.0) f\u00f6resl\u00e5s en upps\u00e4ttning patchar med en implementation av RV (Runtime Verification) mekanismen, som representerar medel f\u00f6r att kontrollera korrektheten i driften av h\u00f6gp\u00e5litliga system som garanterar avbrottsfrihet. Kontroll utf\u00f6rs under k\u00f6rning genom att f\u00e4sta hanterare vid sp\u00e5rningspunkter som verifierar den faktiska exekveringen med en f\u00f6rdefinierad referensmodell av en automat som definierar det f\u00f6rv\u00e4ntade beteendet i systemet. <\/p>\n
Information fr\u00e5n sp\u00e5rningspunkter \u00f6verf\u00f6r modellen fr\u00e5n ett tillst\u00e5nd till ett annat, och om det nya tillst\u00e5ndet inte \u00f6verensst\u00e4mmer med modellens parametrar genereras en varning eller k\u00e4rnan \u00f6verf\u00f6rs till ett tillst\u00e5nd av «panic» (det f\u00f6ruts\u00e4tts att h\u00f6gp\u00e5litliga system kommer att identifiera s\u00e5dana situationer och reagera p\u00e5 dem). Automatmodellen som definierar \u00f6verg\u00e5ngarna fr\u00e5n ett tillst\u00e5nd till ett annat exporteras till formatet «dot» (graphviz), varefter den \u00f6vers\u00e4tts med hj\u00e4lp av verktyget dot2c till en representation i C-spr\u00e5ket, som laddas som en k\u00e4rnmodul som \u00f6vervakar avvikelser fr\u00e5n den f\u00f6rutbest\u00e4mda modellen.
<\/center> <\/p>\n
Verifiering mot modellen under k\u00f6rning positioneras som en mer l\u00e4ttviktig och praktiskt genomf\u00f6rbar metod f\u00f6r att bekr\u00e4fta korrektheten i driften av kritiska system, som komplementerar klassiska metoder f\u00f6r att bekr\u00e4fta tillf\u00f6rlitlighet, s\u00e5som modellkontroll och matematiska bevis f\u00f6r att koden \u00f6verensst\u00e4mmer med specifikationerna som definieras i ett formellt spr\u00e5k. Bland f\u00f6rdelarna med RV n\u00e4mns m\u00f6jligheten att s\u00e4kerst\u00e4lla strikt verifiering utan att hela systemet implementeras p\u00e5 modelleringsspr\u00e5ket, samt flexibel reaktion p\u00e5 of\u00f6rutsedda h\u00e4ndelser, exempelvis f\u00f6r att blockera ytterligare spridning av fel i kritiska system. \n K\u00e4lla: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"
![\"En](\"\/wp-content\/uploads\/2022\/08\/56f02964c804a17b5cf5d811b2777368.jpg\")
<\/center> <\/p>\n