Fir Linux gouf e Mechanismus proposéiert fir d'korrekt Operatioun vum Kernel z'iwwerpréiwen

Fir d'Inklusioun am Linux Kernel 5.20 (vläicht wäert d'Branche 6.0 nummeréiert sinn), gëtt e Set vu Patches proposéiert mat der Implementatioun vum RV (Runtime Verification) Mechanismus, deen Tools ubitt fir déi richteg Operatioun op héich zouverléissege Systemer ze kontrolléieren, déi d'Garantie garantéieren. Fehlen vu Feeler. D'Verifizéierung gëtt während der Runtime duerchgefouert andeems Dir Handler op Spuerpunkte befestegt, déi den aktuellen Fortschrëtt vun der Ausféierung iwwerpréift géint e virbestëmmte Referenz-deterministesche Modell vum Automat, deen dat erwaart Verhalen vum System definéiert.

Informatioun vu Spuerpunkte bewegt de Modell vun engem Staat an en aneren, a wann den neie Staat net mat de Parameteren vum Modell entsprécht, gëtt eng Warnung generéiert oder de Kernel gëtt an engem "Panik" Zoustand gesat (Héich Zouverlässegkeet Systemer ginn erwaart z'entdecken an op esou Situatiounen reagéieren). Den Automatmodell, deen Iwwergäng vun engem Staat an en aneren definéiert, gëtt an de "Punkt" Format (graphviz) exportéiert, duerno gëtt et mat der dot2c Utility an eng C Representatioun iwwersat, déi a Form vun engem Kernel Modul gelueden gëtt verfollegt Ofwäichunge vum Ausféierung Fortschrëtt vum virdefinéierte Modell.

Fir Linux gouf e Mechanismus proposéiert fir d'korrekt Operatioun vum Kernel z'iwwerpréiwen

Run-Time Modellprüfung ass positionéiert als e méi liicht a méi einfach z'implementéieren Method fir d'korrekt Ausféierung op missionskritesch Systemer z'iwwerpréiwen, komplementéiert klassesch Zouverlässegkeetsverifizéierungsmethoden wéi Modellprüfung a mathematesch Beweiser vu Codekonformitéit mat Spezifikatioune, déi an engem formelle ginn. Sprooch. Ënner de Virdeeler vum RV ass d'Fäegkeet fir strikt Verifizéierung ze bidden ouni eng separat Ëmsetzung vum ganze System an enger Modelléierungssprooch, souwéi flexibel Äntwert op onerwaart Eventer, zum Beispill fir d'weider Verbreedung vun engem Feeler a kriteschen Systemer ze blockéieren.

Source: opennet.ru

Setzt e Commentaire