A Linux 5.20/6.0 proposa un mecanisme per verificar la correcció del nucli

Linux Kernel

Fa poc es va donar a conèixer la notícia que s'ha realitzat una proposta per ser inclòs a el nucli de Linux 5.20 (o potser la branca es numerarà 6.0, tot depèn de la decisió de Linus torvalds a causa del seu comentari que faig en el llançament del Kernel 5.19).

La proposta realitzada és sobre un conjunt de pegats amb la implementació del mecanisme RV (Runtime Verification), que és un mitjà per verificar el funcionament correcte en sistemes altament fiables que garanteixen l'absència d'errors.

La validació es realitza en temps d'execució en adjuntar controladors a punts de traça que verifiquen el progrés real de lexecució contra un model determinista de referència predefinit de lautòmat que determina el comportament esperat del sistema.

El desenvolupador de Linux, Daniel Bristot d'Oliveira esmenta:

Durant els darrers anys, he estat explorant la possibilitat de verificar el comportament del kernel de Linux usant Runtime Verification.

Runtime Verification (RV) és un mètode lleuger (però rigorós) que complementa les tècniques clàssiques de verificació exhaustiva (com la comprovació de models i la demostració de teoremes) amb un enfocament més pràctic per a sistemes complexos. En lloc de dependre d‟un model detallat d‟un sistema (per exemple, una reimplementació d‟un nivell d‟instrucció), RV funciona analitzant el rastre de l‟execució real del sistema, comparant-lo amb una especificació formal del comportament del sistema.

L'ús d'autòmats deterministes per a RV és un enfocament ben establert. En el cas específic del kernel de Linux, podeu consultar com modelar el comportament complex del kernel de Linux amb aquest article:

D'Oliveira, Daniel Bristot; Cucinotta, Tommaso; D'Oliveira, Ròmul Silva. *Verificació formal eficient per al nucli de Linux.* A: Conferència Internacional sobre Enginyeria de Programari i Mètodes Formals. Springer, Cham, 2019. pàg. 315-332.

I com eficient és aquest enfocament aquí:

D'Oliveira, Daniel B.; D'Oliveira, Ròmul S.; Cucinotta, Tommaso. *Un model de sincronització de subprocessos per al nucli de Linux PREEMPT_RT.* Journal of Systems Architecture, 2020, 107: 101729.

TLDR: és possible modelar comportaments complexos de forma modular, amb una sobrecàrrega acceptable (fins i tot per a sistemes de producció).

S'esmenta que la informació dels punts de traça mou el model d'un estat a un altre, i si el nou estat no coincideix amb els paràmetres del model, es genera una advertència o el kernel entra en un estat panic (suposant que els sistemes altament fiables detectaran i respondran a aquestes situacions).

El model d'autòmat que defineix les transicions d'un estat a un altre s'exporta al format dot (graphviz), després d'això es tradueix utilitzant la utilitat dot2c en una representació C, que es carrega en forma d'un mòdul kernel que rastreja les desviacions. de lexecució a partir dun model predefinit.

La verificació de models en temps d'execució es posiciona com un mètode més lleuger i fàcil d'implementar per verificar la correcció de l'execució en sistemes de missió crítica, que complementa els mètodes clàssics de verificació de fiabilitat, com ara la verificació de models i les proves matemàtiques del compliment del codi amb les especificacions donades en un llenguatge formal.

El mantenidor del subsistema de seguiment, Steven Rostedt, ho va resumir així:

» Aquest és el canvi més gran per a aquesta sol·licitud dextracció. Introduïu la verificació en temps d'execució que és necessària per executar Linux en sistemes crítics per a la seguretat. Permet que s'insereixin models d'autòmats deterministes al nucli que s'adjuntarà als punts de seguiment, on la informació sobre aquests punts de seguiment mourà el model d'un estat a un altre.

Entre els avantatges que s'esmenten de RV es destaca que hi ha la capacitat de proporcionar una verificació rigorosa sense una implementació separada de tot el sistema en un llenguatge de modelatge, així com una resposta flexible a esdeveniments imprevistos, per exemple, per bloquejar la propagació de una falla en sistemes crítics.

Finalment si estàs interessat a poder conèixer més sobre això, pots consultar els detalls al següent enllaç.

font: https://www.phoronix.com/


Sigues el primer a comentar

Deixa el teu comentari

La seva adreça de correu electrònic no es publicarà. Els camps obligatoris estan marcats amb *

*

*

  1. Responsable de les dades: AB Internet Networks 2008 SL
  2. Finalitat de les dades: Controlar l'SPAM, gestió de comentaris.
  3. Legitimació: El teu consentiment
  4. Comunicació de les dades: No es comunicaran les dades a tercers excepte per obligació legal.
  5. Emmagatzematge de les dades: Base de dades allotjada en Occentus Networks (UE)
  6. Drets: En qualsevol moment pots limitar, recuperar i esborrar la teva informació.