|
|
A Portmap Plugin for BusyBox
Huba, Lukáš ; Fiedor, Jan (referee) ; Vojnar, Tomáš (advisor)
This bachelor thesis deals with an implementation portmap of the BusyBox package. The first part deals with the theoretical background of the thesis in particular, introducing the technology of remote procedures call, data representation, and the portmap protocol. The second part of the thesis briefly acquaints the reader with the BusyBox project and describes an implementation of the portmap plugin done within the the thesis. The conclusion of the thesis summaries the work that has been done and discusses possible future work in the area.
|
|
|
Equivalence-Based Slicing of Programs
Malecová, Tatiana ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cieľom tejto práce je navrhnúť metódu, ktorá zjednoduší dva porovnávané programy na základe výsledkov ich sémantickej analýzy. Cieľom je odstránenie čo najväčšieho množstva sémanticky ekvivalentných častí porovnávaných programov. Pre nájdenie týchto ekvivalentných častí aplikujeme vlastné riešenie problému nájdenia najväčšieho spoločného indukovaného podgrafu. Následne sme schopní zjednodušiť programy využitím spätného statického prerezávania. Aplikáciou tohto zjednodušenia získame prerezané programy, ktoré obsahujú rozdielne časti a časti programov, ktoré môžu tieto rozdiely ovplyvniť. Táto metóda je naimplementovaná ako rozšírenie nástroja DiffKemp, čo je statický analyzátor sémantických rozdielov medzi rôznymi verziami rozsiahlych programov. Experimenty vykonané na jadrách Linux-u ukazujú, že metóda je schopná veľmi efektívne vyprodukovať korektné prerezané programy (analýza sa predĺžila len o 3.2%). Navyše, vzniknuté prerezané programy sú omnoho menšie, ako originálne, čo ich činí vhodnými pre ďalšiu analýzu.
|
|
|
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.
|
|
|
Detection of Expressions with Undefined Behavior in C Language
Hellebrandt, Lukáš ; Vojnar, Tomáš (referee) ; Müller, Petr (advisor)
Práce se zabývá detekcí nedefinovaného chování v programech v jazyce C. Zaměřujemese na nedefinované chování vznikající nesprávnou prací se sekvenčními body a vedlejšími efekty. Provedeme teoretický rozbor a pojmy jako nedefinované chování nebo vedlejší efekt zasadíme do kontextu práce. Dále vysvětlíme nebezpečnost konstrukcí vedoucích k nedefinovanému chování. Navrhneme metodu pro automatickou detekci zmíněného druhu nedefinovaného chování. Nakonec navrhneme a implementujeme nástroj pro jeho automatizovanou statickou detekci a popíšeme principy funkce tohoto nástroje. Při jeho návrhu klademe, narozdíl od současných řešení, důraz na funkčnost i v případě přístupu k paměti přes ukazatel nebo z volané funkce. Práce obsahuje příklady nebezpečných konstrukcí, na některých z nich jsou demonstrovány funkce vytvořeného nástroje.
|
|
|
Minimization of Counting Automata
Turcel, Matej ; Vojnar, Tomáš (referee) ; Holík, Lukáš (advisor)
Táto práca sa zaoberá redukciou veľkosti tzv. čítačových automatov. Čítačové automaty rozširujú klasické konečné automaty o čítače s obmedzeným rozsahom hodnôt. Umožňujú tým efektívne spracovať napr. regulárne výrazy s opakovaním: a{5,10}. V tejto práci sa zaoberáme reláciou simulácie v čítačových automatoch, pomocou ktorej sme schopní zredukovať ich veľkosť. Opierame sa pritom o klasickú simuláciu v konečných automatoch, ktorú netriviálnym spôsobom rozširujeme na čítačové automaty. Kľúčovým rozdielom je nutnosť simulovať okrem stavov taktiež čítače. Za týmto účelom zavádzame nový koncept parametrizovanej relácie simulácie, a navrhujeme metódy výpočtu tejto relácie a redukcie veľkosti čítačových automatov pomocou nej. Navrhnuté metódy sú tiež implementované a je vyhodnotená ich efektivita.
|
|
|
Detection of Timing Side-Channels in TLS
Koscielniak, Jan ; Malík, Viktor (referee) ; Vojnar, Tomáš (advisor)
Protokol TLS je komplexní a jeho použití je široce rozšířené. Mnoho zařízení používá TLS na ustanovení bezpečné komunikace, vzniká tak potřeba tento protokol důkladně testovat. Tato diplomová práce se zaměřuje na útoky přes časové postranní kanály, které se znovu a znovu objevují jako variace na už známé útoky. Práce si klade za cíl usnadnit korektní odstranění těchto postranních kanálů a předcházet vzniku nových vytvořením automatizovaného frameworku, který pak bude integrován do nástroje tlsfuzzer, a vytvořením testovacích scénářů pro známé útoky postranními kanály. Vytvořené rozšíření využívá program tcpdump pro sběr časových údajů a statistické testy spolu s podpůrnými grafy k rozhodnutí, zda se jedná o možný postranní kanál. Rozšíření bylo zhodnoceno pomocí nových testovacích skriptů a byla předvedena jeho dobrá schopnost rozlišit postranní kanál. Rozšíření spolu s testy je nyní součástí nástroje tlsfuzzer.
|
|
|
Automatic Comparison of Static Analysis Outputs on Different Versions of Programs
Kompová, Radmila ; Müller, Petr (referee) ; Vojnar, Tomáš (advisor)
This thesis aims at development of a tool support for comparing the output of static analysis applied to different versions of program source codes. The thesis also comprises a discussion of three opensource static analyzers of the C source code. Based on this discussion, one of these analyzers, Cppcheck, was chosen for the implementation of the designed tool. The static analyzer's outputs, obtained for various versions of a specific program, are compared on the basis of the context of the line at which an error was found. The patch utility is used for comparing the appropriate contexts. Detected errors are classified into three groups: new, old, and fixed errors. A web interface allowing an easier-to-follow presentation of the results is also provided. The designed tool set has been successfully tested on three opensource projects, including the Linux kernel, Coreutils and CPython.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
|
|
|
Static Analysis Using Facebook Infer to Find Atomicity Violations
Harmim, Dominik ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The goal of this thesis is to propose a static analyser that detects atomicity violations. The proposed analyser Atomer is implemented as a module of Facebook Infer, which is an open-source and extendable static analysis framework that promotes efficient modular and incremental analysis. The analyser works on the level of sequences of function calls. The proposed solution is based on the assumption that sequences executed atomically once should probably be executed always atomically. The implemented analyser has been successfully verified and evaluated on both smaller programs created for testing purposes as well as publicly available benchmarks derived from real-life low-level programs.
|
|
|
Static Analyzer for List Manipulating Programs
Kotoun, Michal ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Creating a software verification tool is a complex task -- one must implement source code parsing, instruction representation, value abstraction, user interface, ... and the analysis itself. Therefore, we decided to create a static analysis framework to prevent unnecessary wheel reinventing by an analyses implementers. We propose a general design of the framework called Angie with a primary focus on usability, and describe a prototype implementation of the framework, including a model analysis based on symbolic memory graphs. Angie is implemented in C++ and uses the LLVM toolchain as the front-end for parsing the source code of analysed programs.
|
guest ::
