|
|
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.
|
|
|
Analysis of C Programs with Dynamic Linked Data Structures
Šoková, Veronika ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
This master's thesis deals with the analysis of dynamic linked data structures using shape analysis used in the Predator tool. It describes the chosen abstract domain for heap representation - symbolic memory graphs. It deals with the design of framework for the development of static analyzers based on Clang/LLVM. The main contribution is implementing and testing LLVM's transformation passes that simplify the LLVM IR. Second contribution is the optimization of parameters for parallel run of several variants of the Predator tool. Parameters are tuned for benchmark from SV-COMP'16, where our tool won gold medal in Heap Data Structures category. Last contribution is the design of verification core with the focus on the SMG domain.
|
|
|
Generic Template-Based Synthesis of Program Abstractions
Marušák, Matej ; Holík, Lukáš (referee) ; Malík, Viktor (advisor)
Cieľom tejto práce je návrh a implementácia generického strategy solveru pre nástroj 2LS. 2LS je analyzátor na statickú verifikáciu programov napísaných v jazyku C. Verifikovaný program je za využita abstraktnej interpretácie analyzovaný SMT solverom. Prevod z ab- straktného stavu programu do logickej formule, s ktorou vie pracovať SMT solver vykonáva komponenta nazývaná strategy solver. Aktuálne pre každú doménu existuje jeden takýto solver. Navrhované riešenie vytvára jeden obecný strategy solver, ktorý zjednodušuje tvorbu nových domén. Zároveň navrhovaný spôsob umožnuje prevedenie existujúcich domén a teda zmenšuje program analyzátora.
|
|
|
Static Analysis Using Facebook Infer Focused on Deadlock Detection
Marcin, Vladimír ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Static analysis has nowadays become one of the most popular ways of catching bugs early in the modern software. However, a frequent problem of static analysers, which are reasonably precise, is their scalability. Moreover, these which are efficient and scale (e.g.: Coverity, KlockWork, etc.) are often proprietary and difficult to openly evaluate or extend. An improvement to this state of practice is brought Facebook Infer, which offers an open-source framework for compositional and incremental static analysis. In this thesis, we present our Low-Level Deadlock Detector (L2D2) extending the capabilities of Infer. Our algorithm fits the compositional analysis, based on a context independent computation of a summary for each function, which results in its high scalability. We have implemented the algorithm and evaluated it on a benchmark consisting of real-life programs derived from the Debian GNU/Linux with in total 11.4 MLOC. While neither sound nor complete, our approach is effective in practice, finding all known deadlocks and giving false alarms in less than 4% of the considered programs only.
|
|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
Cieľom tejto práce je návrh analýzy tvaru haldy vhodnej pre potreby analyzátora 2LS. 2LS je nástroj pre analýzu C programov založený na automatickom odvodzovaní invariantov s použitím SMT solvera. Navrhované riešenie obsahuje spôsob reprezentácie tvaru programovej haldy pomocou logických formulí nad teóriou bitových vektorov. Tie sú následne využité v SMT solveri pre predikátovú logiku prvého rádu na odvodenie invariantov cyklov a súhrnov jednotlivých funkcií analyzovaného programu. Náš prístup je založený na ukazateľových prístupových cestách, ktoré vyjadrujú dosiahnuteľnosť objektov na halde z ukazateľových premenných. Informácie získané z analýzy môžu byť využité na dokázanie rôznych vlastností programu súvisiacich s prácou s dynamickýcmi dátovými štruktúrami. Riešenie bolo implementované v rámci nástroja 2LS. S jeho použitím došlo k výraznému zlepšeniu schopnosti 2LS analyzovať programy pracujúce s ukazateľmi a dynamickými dátovými štruktúrami. Toto je demonštrované na sade experimentov prevzatých zo známej medzinárodnej súťaže vo verifikácii programov SV-COMP a iných experimentoch.
|
|
|
Generic Template-Based Synthesis of Program Abstractions
Marušák, Matej ; Holík, Lukáš (referee) ; Malík, Viktor (advisor)
Cieľom tejto práce je návrh a implementácia generického strategy solveru pre nástroj 2LS. 2LS je analyzátor na statickú verifikáciu programov napísaných v jazyku C. Verifikovaný program je za využita abstraktnej interpretácie analyzovaný SMT solverom. Prevod z ab- straktného stavu programu do logickej formule, s ktorou vie pracovať SMT solver vykonáva komponenta nazývaná strategy solver. Aktuálne pre každú doménu existuje jeden takýto solver. Navrhované riešenie vytvára jeden obecný strategy solver, ktorý zjednodušuje tvorbu nových domén. Zároveň navrhovaný spôsob umožnuje prevedenie existujúcich domén a teda zmenšuje program analyzátora.
|
|
|
Static Analysis Using Facebook Infer Focused on Deadlock Detection
Marcin, Vladimír ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Static analysis has nowadays become one of the most popular ways of catching bugs early in the modern software. However, a frequent problem of static analysers, which are reasonably precise, is their scalability. Moreover, these which are efficient and scale (e.g.: Coverity, KlockWork, etc.) are often proprietary and difficult to openly evaluate or extend. An improvement to this state of practice is brought Facebook Infer, which offers an open-source framework for compositional and incremental static analysis. In this thesis, we present our Low-Level Deadlock Detector (L2D2) extending the capabilities of Infer. Our algorithm fits the compositional analysis, based on a context independent computation of a summary for each function, which results in its high scalability. We have implemented the algorithm and evaluated it on a benchmark consisting of real-life programs derived from the Debian GNU/Linux with in total 11.4 MLOC. While neither sound nor complete, our approach is effective in practice, finding all known deadlocks and giving false alarms in less than 4% of the considered programs only.
|
|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
Cieľom tejto práce je návrh analýzy tvaru haldy vhodnej pre potreby analyzátora 2LS. 2LS je nástroj pre analýzu C programov založený na automatickom odvodzovaní invariantov s použitím SMT solvera. Navrhované riešenie obsahuje spôsob reprezentácie tvaru programovej haldy pomocou logických formulí nad teóriou bitových vektorov. Tie sú následne využité v SMT solveri pre predikátovú logiku prvého rádu na odvodenie invariantov cyklov a súhrnov jednotlivých funkcií analyzovaného programu. Náš prístup je založený na ukazateľových prístupových cestách, ktoré vyjadrujú dosiahnuteľnosť objektov na halde z ukazateľových premenných. Informácie získané z analýzy môžu byť využité na dokázanie rôznych vlastností programu súvisiacich s prácou s dynamickýcmi dátovými štruktúrami. Riešenie bolo implementované v rámci nástroja 2LS. S jeho použitím došlo k výraznému zlepšeniu schopnosti 2LS analyzovať programy pracujúce s ukazateľmi a dynamickými dátovými štruktúrami. Toto je demonštrované na sade experimentov prevzatých zo známej medzinárodnej súťaže vo verifikácii programov SV-COMP a iných experimentoch.
|
|
|
Analysis of C Programs with Dynamic Linked Data Structures
Šoková, Veronika ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
This master's thesis deals with the analysis of dynamic linked data structures using shape analysis used in the Predator tool. It describes the chosen abstract domain for heap representation - symbolic memory graphs. It deals with the design of framework for the development of static analyzers based on Clang/LLVM. The main contribution is implementing and testing LLVM's transformation passes that simplify the LLVM IR. Second contribution is the optimization of parameters for parallel run of several variants of the Predator tool. Parameters are tuned for benchmark from SV-COMP'16, where our tool won gold medal in Heap Data Structures category. Last contribution is the design of verification core with the focus on the SMG domain.
|
guest ::
