Don haɗawa a cikin Linux kernel 5.20 (wataƙila reshe za a ƙidaya 6.0), ana ba da shawarar faci tare da aiwatar da tsarin RV (Runtime Verification), wanda ke ba da kayan aiki don bincika ingantaccen aiki akan tsarin ingantaccen aminci wanda ke ba da garantin rashin gazawa. Ana yin tabbatarwa a lokacin aiki ta hanyar haɗa masu aiki zuwa wuraren gano abubuwan da ke bincika ainihin ci gaban aiwatarwa a kan ƙayyadaddun ƙayyadaddun ƙayyadaddun ƙididdiga na atomatik wanda ke bayyana halayen da ake tsammanin tsarin.
Bayanai daga wuraren da aka gano suna motsa samfurin daga wannan jiha zuwa waccan, kuma idan sabuwar jihar ba ta dace da ma'auni na ƙirar ba, ana haifar da gargaɗi ko an sanya kernel a cikin yanayin "firgita" (ana sa ran tsarin aminci mai girma zai gano. da amsa irin wannan yanayi). Samfurin automaton, wanda ke bayyana sauye-sauye daga wannan jiha zuwa waccan, ana fitar da shi zuwa tsarin “dot” (graphviz), bayan haka an fassara shi ta hanyar amfani da dot2c mai amfani a cikin wakilcin C, wanda aka ɗora a cikin nau'in kernel module wanda yana bin saɓanin ci gaban aiwatarwa daga ƙayyadaddun samfurin.
An saita ƙirar ƙirar lokacin gudu azaman hanya mai sauƙi- nauyi da sauƙi don aiwatarwa na tabbatar da aiwatar da daidaitaccen aiwatarwa akan tsarin manufa-mahimmanci, haɓaka hanyoyin tabbatar da amincin na gargajiya kamar bincika ƙirar ƙira da hujjojin lissafin ƙima na lamba tare da ƙayyadaddun bayanai da aka bayar a cikin tsari. harshe. Daga cikin fa'idodin RV shine ikon samar da tabbataccen tabbaci ba tare da aiwatar da keɓantaccen aiwatar da tsarin gabaɗayan a cikin yaren ƙirar ƙira ba, da kuma sassaucin ra'ayi ga abubuwan da ba a zata ba, alal misali, don toshe ƙarin yaduwa na gazawa a cikin mahimman tsarin.
source: budenet.ru