Uutiset paljastivat sen äskettäin on tehty ehdotus sisällytettäväksi ydin Linux 5.20 (tai ehkä haaran numero on 6.0, kaikki riippuu Linus Torvaldsin päätöksestä, joka johtuu hänen kommentistaan Kernel 5.19 -julkaisusta).
Tehty ehdotus on noin sarja korjaustiedostoja, joissa on toteutettu RV-mekanismi (Runtime Verification), jolla varmistetaan oikea toiminta erittäin luotettavissa järjestelmissä, jotka takaavat vikojen puuttumisen.
validointi tehdään ajon aikana liittämällä käsittelijät jäljityspisteisiin jotka tarkistavat suorituksen todellisen edistymisen automaatin ennalta määritettyyn deterministiseen vertailumalliin, joka määrittää järjestelmän odotetun toiminnan.
Linux-kehittäjä, Daniel Bristot de Oliveira mainitsee:
Muutaman viime vuoden ajan olen tutkinut mahdollisuutta tarkistaa Linux-ytimen käyttäytyminen Runtime Verificationin avulla.
Runtime Verification (RV) on kevyt (mutta tiukka) menetelmä, joka täydentää perinteisiä tyhjentäviä varmennustekniikoita (kuten mallin tarkistusta ja lauseiden todistamista) monimutkaisten järjestelmien käytännönläheisemmällä lähestymistavalla. Sen sijaan, että luottaisi järjestelmän yksityiskohtaiseen malliin (esimerkiksi käskytason uudelleentoteutukseen), VR toimii analysoimalla järjestelmän todellista suoritusjälkeä ja vertaamalla sitä järjestelmän toiminnan muodolliseen määrittelyyn.
Determinististen automaattien käyttö VR:ssä on vakiintunut lähestymistapa. Linux-ytimen erityistapauksessa voit oppia mallintamaan Linux-ytimen monimutkaisen toiminnan tämän artikkelin avulla:
De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo Silva. *Tehokas muodollinen tarkastus Linux-ytimelle.* Julkaisussa: International Conference on Software Engineering and Formal Methods. Springer, Cham, 2019. s. 315-332.
Ja kuinka tehokas tämä lähestymistapa on täällä:
De Oliveira, Daniel B.; De Oliveira, Romulo S.; Cucinotta, Tommaso. *Säikeen synkronointimalli PREEMPT_RT Linux-ytimelle.* Journal of Systems Architecture, 2020, 107: 101729.
TLDR: Monimutkaista käyttäytymistä voidaan mallintaa modulaarisesti hyväksyttävillä yleiskustannuksilla (jopa tuotantojärjestelmissä).
Mainitaan se seurantapistetiedot siirtävät mallin tilasta toiseen, ja jos uusi tila ei vastaa mallin parametreja, luodaan varoitus tai ydin siirtyy "paniikkitilaan" (olettaen, että erittäin luotettavat järjestelmät havaitsevat tällaiset tilanteet ja reagoivat niihin).
Automaattinen malli määrittää siirtymät tilasta toiseen viedään "piste"-muotoon (graphviz), jonka jälkeen se käännetään dot2c-apuohjelmalla C-esitykseen, joka ladataan poikkeamia jäljittävän ydinmoduulin muodossa. suoritus ennalta määritetystä mallista.
Mallien tarkastaminen ajon aikana on asetettu kevyemmäksi ja helpommaksi menetelmäksi toteuttaa suorituskriittisten järjestelmien suorittamisen oikeellisuuden todentamiseksi, joka täydentää klassisia luotettavuuden todentamismenetelmiä, kuten mallin varmennusta ja matemaattisia todisteita koodin yhteensopivuudesta muodollisella kielellä annettujen spesifikaatioiden kanssa.
Seurantaalijärjestelmän ylläpitäjä Steven Rostedt tiivisti asian seuraavasti:
» Tämä on tämän vetopyynnön suurin muutos. Esittelee ajonaikaisen vahvistuksen, jota tarvitaan Linuxin käyttämiseen tietoturvakriittisissä järjestelmissä. Se mahdollistaa determinististen automaatiomallien lisäämisen ytimeen liitettäväksi jäljityspisteisiin, joissa tiedot näistä jäljityspisteistä siirtävät mallin tilasta toiseen.
Mainittujen RV:n etujen joukossa on kyky tarjota tiukka varmennus ilman erillistä koko järjestelmän toteutusta mallinnuskielellä sekä joustava reagointi odottamattomiin tapahtumiin esimerkiksi kriittisten järjestelmien vikojen etenemisen estämiseksi.
Lopuksi, jos olet kiinnostunut saamaan lisätietoja siitä, voit tutustua yksityiskohtiin osoitteessa seuraava linkki.
lähde: https://www.phoronix.com/