Intel ya buga babban sakin farko na kayan aiki na ControlFlag 1.0, wanda ke ba ku damar gano kurakurai da rashin daidaituwa a cikin lambar tushe ta amfani da tsarin koyon injin da aka horar akan adadi mai yawa na lambar data kasance. Ba kamar na gargajiya static analyzers, ControlFlag ba ya amfani da shirye-sanya dokoki, a cikin abin da yana da wuya a samar da duk yiwu zažužžukan, amma dogara ne a kan statistics a kan amfani da daban-daban harsuna ginawa a cikin wani babban adadin data kasance ayyuka. An rubuta lambar ControlFlag a cikin C++ kuma an buɗe ta a ƙarƙashin lasisin MIT.
An horar da tsarin ta hanyar gina tsarin ƙididdiga na jerin lambobin da ke akwai na ayyukan buɗaɗɗen tushe da aka buga a GitHub da makamantan wuraren ajiyar jama'a. A matakin horo, tsarin yana ƙayyade alamu na yau da kullun don gina sifofi a cikin lambar kuma ya gina bishiyar haɗin gwiwa tsakanin waɗannan alamu, yana nuna kwararar aiwatar da code a cikin shirin. A sakamakon haka, an kafa bishiyar yanke shawara wanda ya haɗu da ƙwarewar ci gaba na duk lambobin tushe da aka bincika. Lambar da ake dubawa tana aiwatar da irin wannan tsari na gano alamu waɗanda aka bincika akan bishiyar yanke shawara. Babban bambance-bambance tare da rassan maƙwabta suna nuna kasancewar anomaly a cikin tsarin da ake dubawa.
A matsayin misali na iyawar ControlFlag, masu haɓakawa sun bincika lambobin tushe na ayyukan OpenSSL da cURL:
- Haɓaka haɓaka "(s1 == NULL) ∧ (s2 == NULL)" da "(s1 == NULL) | (s2 == NULL)" , wanda bai dace da tsarin da aka saba amfani da shi ba "(s1 == NULL) || (s2 = NULL)". Lambar ta kuma gano abubuwan da ba su dace ba a cikin kalmomin "(-2 == rv)" (raguwa ita ce typo) da "BIO_puts(bp, ":") <= 0)" (a cikin mahallin duba nasarar kammala aikin aikin ya kamata ya kasance "== 0").
- A cikin CURL, an gano kuskuren da ba a iya gano shi ta hanyar masu nazari na tsaye ba yayin amfani da sigar tsarin "s->keepon", wanda ke da nau'in lamba, amma an kwatanta shi da ƙimar boolean GASKIYA.
Daga cikin fasalulluka na sigar ControlFlag 1.0, akwai cikakken goyan baya ga daidaitattun samfura don harshen C da ikon gano abubuwan da ba su da kyau a cikin yanayin “idan” maganganun. Misali, lokacin nazarin guntun lambar "idan (x = 7) y = x;" Tsarin zai ƙayyade cewa bayanin "idan" yawanci yana amfani da ginin "mai canzawa == lamba" don kwatanta ƙimar lambobi, don haka yana da yuwuwar "m = lamba" a cikin "if" furci ya samo asali ta hanyar bugawa. Kit ɗin ya haɗa da rubutun da ke ba ku damar zazzage ma'ajiyar yaren C na yanzu akan GitHub kuma kuyi amfani da su don gina ƙirar. Hakanan akwai samfuran shirye-shiryen da aka yi, suna ba ku damar fara duba lambar nan da nan.
source: budenet.ru