Linuxille on ehdotettu mekanismia ytimen oikean toiminnan tarkistamiseksi

Lisättäväksi Linux 5.20 -ytimeen (ehkä haaran numero on 6.0) ehdotetaan joukko korjaustiedostoja, joissa on toteutettu RV (Runtime Verification) -mekanismi, joka tarjoaa työkaluja oikean toiminnan tarkistamiseen erittäin luotettavissa järjestelmissä, jotka takaavat epäonnistumisten puuttuminen. Varmentaminen suoritetaan ajon aikana liittämällä käsittelijät jäljityspisteisiin, jotka tarkistavat suorituksen todellisen edistymisen automaatin ennalta määrättyä referenssideterminististä mallia vastaan, joka määrittelee järjestelmän odotetun toiminnan.

Jäljityspisteiden tiedot siirtävät mallin tilasta toiseen, ja jos uusi tila ei vastaa mallin parametreja, syntyy varoitus tai ydin asetetaan "paniikkitilaan" (korkean luotettavuuden järjestelmien odotetaan havaittavan ja reagoida sellaisiin tilanteisiin). Automaattimalli, joka määrittää siirtymät tilasta toiseen, viedään "piste"-muotoon (graphviz), jonka jälkeen se käännetään dot2c-apuohjelmalla C-esitykseen, joka ladataan ydinmoduulin muodossa, joka seuraa suorituksen edistymisen poikkeamia ennalta määritetystä mallista.

Linuxille on ehdotettu mekanismia ytimen oikean toiminnan tarkistamiseksi

Ajonaikainen mallin tarkistus on sijoitettu kevyemmäksi ja helpompi toteuttaa menetelmäksi oikean suorituskyvyn varmentamiseen kriittisissä järjestelmissä, ja se täydentää klassisia luotettavuuden varmistusmenetelmiä, kuten mallin tarkistusta ja matemaattisia todisteita koodin noudattamisesta muodollisissa eritelmissä. Kieli. RV:n etuja ovat muun muassa kyky tarjota tiukka varmennus ilman erillistä koko järjestelmän toteutusta mallinnuskielellä sekä joustava reagointi odottamattomiin tapahtumiin, esimerkiksi estämään vian leviäminen kriittisissä järjestelmissä.

Lähde: opennet.ru

Lisää kommentti