Detail práce
Static Analysis of C Programs
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.
statická analýza, formálna verifikácia, formálne metódy, analýza tvaru haldy, abstraktná doména pre popis polí, syntéza invariantov založená na šablónach, abstraktná interpretácia, SAT/SMT solving, invarianty cyklov sémantická ekvivalencia programov, refaktoring, vyhľadávanie vzorov, vzory zachovávajúce sémantiku, vzory zmien v programoch, jadro Linuxu, prerezávanie programov, LLVM IR
@phdthesis{FITPT1059,
author = "Viktor Mal\'{i}k",
type = "Diserta\v{c}n\'{i} pr\'{a}ce",
title = "Static Analysis of C Programs",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2024,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/phd-thesis/1059/"
}