|
|
Static Analysis of C Programs
Malík, Viktor ; Zuleger, Florian (referee) ; Strejček, Jan (referee) ; Vojnar, Tomáš (advisor)
Táto práca prináša niekoľko originálnych príspevkov do oblasti statickej analýzy programov so zameraním na nízkoúrovňový softvér napísaný v jazyku C. Práca je rozdelená do dvoch častí, z ktorých každá sa venuje inej oblasti statickej analýzy, konkrétne formálnej verifikácii a statickej analýze sémantickej ekvivalencie rôznych verzií softvéru. V prvej časti práce navrhujeme nové analýzy vhodné pre verifikačné nástroje založené na automatickom odvodzovaní invariantov s využitím SMT solveru. Navrhnuté riešenie zahŕňa dve nové abstraktné domény založené na šablónach, ktoré umožňujú popísať tvar programovej haldy a obsahy polí pomocou logických formulí nad bit-vektormi. Doména pre reprezentáciu tvaru haldy je založená na zachytení vzťahov medzi ukazovateľmi a symbolickými adresami abstraktných objektov v pamäti. Doména pre reprezentáciu obsahov polí je založená na rozdelení polí na niekoľko neprekrývajúcich sa spojitých segmentov a odvodení samostatného invariantu pre každý segment. Obidve domény sú navrhnuté spôsobom, ktorý umožňuje ich kombináciu s inými doménami, vďaka čomu je možné abstrahovať tvar a obsah dátových štruktúr zároveň. Informácie získané z týchto analýz je možné použiť na dokázanie bezpečnosti práce s pamäťou a nedosiahnuteľnosti chybových stavov v programoch, ktoré pracujú s dynamickými dátovými štruktúrami. Všetky navrhnuté rozšírenia boli implementované do nástroja 2LS a porovnané s nástrojmi, ktoré sa pravidelne umiestňujú na najvyšších priečkach v relevantných kategóriách v medzinárodnej súťaži vo verifikácii software SV-COMP. Výsledky experimentov ukazujú, že 2LS poráža tieto nástroje na úlohách vyžadujúcich invarianty cyklov kombinujúce popis tvaru a obsahu dynamických dátových štruktúr. Druhá časť práce je motivovaná existenciou softvérových projektov, ktoré vyžadujú zachovanie stability niektorých dôležitých častí, no zároveň sú podrobované pravidelným zmenám. V rámci tejto časti navrhujeme nový prístup pre automatickú analýzu sémantickej ekvivalencie rôznych verzí veľkého priemyselného softvéru napísaného v jazyku C, so špeciálnym zameraním na jadro operačného systému Linux. Navrhnutá metóda používa unikátnu kombináciu vyhľadávania vzorov, rýchlej statickej analýzy a transformácií toku riadenia programov. Tento prístup umožňuje kontrolu zachovania sémantiky funkcií, ktoré tvoria rozhranie analyzovaného projektu ako aj globálnych premenných, ktoré typicky reprezentujú hodnoty konfigurovateľných parametrov systému. Pre porovnávanie globálnych premenných zároveň navrhnujeme špecializovanú procedúru pre prerezávanie programov, ktorá je schopná odstrániť časti programov, ktoré nie sú závislé na hodnotách analyzovaných premenných a obmedziť analýzu iba na závislé časti. Napriek tomu, že metóda nie je schopná formálne dokázať sémantickú ekvivalenciu zásadne upraveného, no ekvivalentného kódu, je schopná porovnať tisíce funkcií v rámci minút a zároveň poskytnúť relatívne malé množstvo nesprávnych výsledkov. Metóda bola implementovaná v nástroji DiffKemp nad infraštruk- túrou LLVM. Výsledky experimentov ukazujú, že DiffKemp, narozdiel od iných nástrojov v oblasti, dáva prakticky použiteľné výsledky aj na projekte o veľkosti jadra Linuxu.
|
|
|
Určení spolehlivosti výsledků statické analýzy pomocí strojového učení
Beránek, Tomáš ; Fiedor, Jan (referee) ; Vojnar, Tomáš (advisor)
Statický analyzátor Meta Infer je nástrojem pro hledání různých typů chyb ve zdrojovém kódu. Jeho výsledky však obsahují více než 95 % falešných hlášení. Tato teze navrhuje řešení, které řadí hlášení od Meta Inferu pomocí grafových neuronových sítí (GNN) podle pravděpodobnosti, že se jedná o skutečnou chybu, a redukuje tak problém s falešnými hlášeními. Systém se skládá z trénovací části, která převádí datovou sadu D2A – sadu roztříděných hlášení z Meta Inferu – na rozšířené grafy vlastností kódu (ECPG) a z modelů GNN natrénovaných na ECPG grafech. Výsledky experimentů ukazují, že vytvořené modely GNN mohou konkurovat a v některých případech dokonce překonat existující řešení vyvíjené silnými průmyslovými týmy. Tato existující řešení mají navíc uzavřený zdrojový kód, a tak řešení vytvořené v této tezi poskytuje slibnou alternativu s otevřeným zdrojovým kódem.
|
guest ::
