За Linux, предложен е механизам за да се потврди правилната работа на кернелот

За вклучување во кернелот на Линукс 5.20 (можеби гранката ќе биде нумерирана 6.0), се предлага сет на закрпи со имплементација на механизмот RV (Верификација на траење), кој обезбедува алатки за проверка на правилното работење на високо доверливи системи кои гарантираат отсуство на неуспеси. Верификацијата се врши при извршување со прикачување на управувачи на точки за трага кои го проверуваат вистинскиот напредок на извршувањето според однапред определен референтен детерминистички модел на автоматот кој го дефинира очекуваното однесување на системот.

Информациите од точките во трага го преместуваат моделот од една во друга состојба, и ако новата состојба не се совпаѓа со параметрите на моделот, се генерира предупредување или кернелот се става во „панична“ состојба (системите со висока доверливост се очекува да детектираат и одговори на такви ситуации). Автоматскиот модел, кој ги дефинира транзициите од една во друга состојба, се извезува во формат „точка“ (graphviz), по што се преведува со помош на алатката dot2c во претстава C, која е вчитана во форма на кернел модул кој ги следи отстапувањата на напредокот на извршувањето од претходно дефинираниот модел.

За Linux, предложен е механизам за да се потврди правилната работа на кернелот

Проверката на моделот во време на извршување е позиционирана како метод со помала тежина и полесен за имплементација за проверка на правилното извршување на системи кои се критични за мисијата, дополнувајќи ги класичните методи за проверка на доверливост, како што се проверка на моделот и математички докази за усогласеноста на кодот со спецификациите дадени во формален јазик. Меѓу предностите на RV е способноста да се обезбеди строга верификација без посебна имплементација на целиот систем на јазик за моделирање, како и флексибилен одговор на непредвидени настани, на пример, да се блокира понатамошното ширење на дефект во критичните системи.

Извор: opennet.ru

Додадете коментар