Automatic Bug-finding Techniques for Large Software Projects
Jiří Slabý · 2013
Cilem teto prace je výzkum aplikovatelnosti soucasných technik pro automa- ticke hledani chyb na velkých softwarových projektech. Vzhledem k tomu, že tyto projekty bývaji komplexni, je poptavka po výkonných analyzatorech, ktere mohou takove projekty zpracovat bez přilisneho generovani falesných hlaseni. Ke splněni tohoto cile se prace zaměřuje na staticke analyzatory, zejmena pak na ty, ktere použivaji techniky jako abstraktni interpretace a symbolicka exekuce. Od doby jejich uvedeni v 70. letech 19. stoleti se jejich použiti v soucasnosti zvysuje diky rychlým procesorům. Jedině diky tomu jsou tyto techniky použitelne na velkých softwarových projektech. Prace shrnuje aktualni stav vybraných technik implementovaných v sou- casných statických analyzatorech. Nadale diskutuje několik velkých softwa- rových projektů, ktere mohou být použity jako zakladna pro vyzkouseni technik. Nakonec jako zakladnu pro zkouseni zvolime Linuxove jadro. Kromě prozkoumaneho stavu soucasných technik navrhujeme v praci nase vlastni techniky. Prace prezentuje nastroj Stanse, který použiva abstraktni inter- pretaci a který nema obtiže se zpracovanim Linuxoveho jadra. Nastroj take filtruje falesna hlaseni z některých inspektorů kodu. Filtrace je založena na vyhledavani vzorů, což se ukazalo být nedostatecne. Proto jsme se nasledně snažili situaci zlepsit symbolickou exekuci. K tomu ucelu použivame sym- bolický exekutor Klee v nasem novem nastroji Symbiotic. Ale protože symbolicka exekuce potřebuje dlouhý výpocetni cas, nejprve kod prořeza- vame technikou „static program slicing”. Během nasich experimentů jsme si vytvořili povědomi o kategoriich chyb, ktere jsou obvykle přitomne v kodu jako je Linuxove jadro. Prozkoumali jsme je dale a vyvinuli databazi znamých chyb v jedne verzi jadra. Databaze je veřejně dostupna a obsahuje informace o chybach a falesných hlasenich nalezených několika nastroji hledajicimi chyby. To může pomoci vývojařům nových statických analyzatorů, aby si porovnali jejich zcela nový analyzator oproti databazi a zjistili, jak se jejich nastroj chova vzhledem k falesným hlasenim, k chybam, ktere minul a samozřejmě k chybam, ktere spravně nasel. Zucastnili jsme se take s nastrojem Symbiotic soutěže Software Ve- rification Competition. Nastroj musel být upraven na potřeby soutěže. A protože jsme se zucastnili s přilis předcasnou verzi, výsledky nebyly přilis povzbudive. Nicmeně, nastroj byl vylepsen a nyni dava dobre výsledky – ziskavame teměř vsechny body v některých kategoriich soutěže. Planujeme se zucastnit s nasim nastrojem dalsiho rocniku soutěže.