|
|
Static Behavioral Malware Detection over LLVM IR
Surovič, Marek ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
In this thesis we study methods for behavioral malware detection, which use techniques of formal verification. In particular we build on the works, which use inference of tree automata from syscall dependency graphs, obtained by static analysis of LLVM IR. We design and implement a prototype detector using the LLVM compiler framework. For experiments with the detector we use an obfuscating compiler capable of generating mutations of malware from C/C++ source code. We discuss preliminary experiments which show the capabilities of the detector and possible future extensions to the detector.
|
|
|
Analýza práce s dynamickými datovými strukturami v C programech
Šoková, Veronika ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Táto diplomová práca sa zaoberá analýzou dynamických dátových štruktúr pomocou analýzy tvaru použitej v nástroji Predator. Popisuje zvolenú abstraktnú doménu pre reprezentáciu pamäte vo forme symbolických grafov pamäte. Ďalej sa zaoberá návrhom prostredia pre vývoj statických analyzátorov nad clang/LLVM. Prínosom tejto práce je vytvorenie a otestovanie transformačných priechodov zjednodušujúcich LLVM IR medzikód. Ďalším prínosom je optimalizácia parametrov paralelnej nadstavby Predatora opakovaným spúšťaním testov z medzinárodnej súťaže SV-COMP'16, kde táto verzia nástroja Predator získala zlatú medailu v kategórii Heap Data Structures. Posledným prínosom je návrh architektúry samotného verifikačného jadra s ohľadom na SMG doménu.
|
|
|
Zdokonalení integrace SSSD a SUDO
Šrubař, Michal ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této bakalářské práce je zlepšení integrace mezi SUDO a SSSD se zaměřením na vylepšení podpory SUDO pravidel uložených na serveru FreeIPA. Zabývá se popisem LDAP SUDO provideru a prezentuje návrh a implementaci IPA SUDO providera. Navržený provider eliminuje nadbytečnou režii překládání SUDO pravidel z IPA SUDO schématu do nativního LDAP SUDO schématu na straně FreeIPA serveru.
|
|
|
Detection of Expressions with Undefined Behavior in C Language
Hellebrandt, Lukáš ; Vojnar, Tomáš (oponent) ; Müller, Petr (vedoucí práce)
This thesis engages in detection of undefined behavior in the C language programs. We focus on undefined behavior stemming from incorrect work with sequence points and side effects. We perform a theoretical analysis and put terms like undefined behavior or side effect in context of the paper. Furthermore, we explain dangerousness of the constructs leading to undefined behavior. We propose a method for automated detection of the mentioned kind of undefined behavior. Finally, we design and implement a tool for its automated static detection and show the principles of the tool’s function. While designing the tool, contrary to current solutions, we stress functionality even in cases like accessing the memory via a pointer or from a called function. The thesis contains examples of dangerous constructs, functions of the created tool are demonstrated on some of them.
|
|
|
Symbolická reprezentace konečných automatů
Chromečka, Jiří ; Vojnar, Tomáš (oponent) ; Lengál, Ondřej (vedoucí práce)
V~oblasti formální analýzy se často setkáváme s~konečnými automaty s~velkým množstvím stavů nad velkými abecedami. Jejich explicitní reprezentace může vyústit ve stavovou explozi a~tento problém může být vyřešen použitím symbolické reprezentace schopné pracovat s~celou množinou stavů najednou. Cílem této práce je rozšířit knihovnu libVATA o~podporu této reprezentace včetně algoritmů pro některé operace nad touto reprezentací. Předložený text se v~úvodu zabývá předpoklady nezbytnými pro pochopení konečných automatů a~binárních rozhodovacích diagramů, které se využívají pro jejich symbolickou reprezentaci. Dále jsou uvedeny některé existující knihovny pro práci s~konečnými automaty. Následuje jádro této práce, návrh symbolické reprezentace a~operací nad ní, které jsou poté implementovány jako rozšíření zmíněné knihovny. Výsledky testů dokazují, že symbolická reprezentace je zajímavou alternativou explicitní reprezentace.
|
|
|
Static Analysis for Discovering Security Vulnerabilities in Web Applications on the Asp.Net Platform
Říha, Jakub ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
This Bachelor thesis is intended to describe theoretical foundations as well as the construction of a static taint analyser based on the .NET Framework and the analysis services provided by the .NET Compiler Platform. This analyser detects SQL injection security vulnerabilities on the ASP.NET MVC platform. Firstly, the analyser constructs control flow graphs as an abstract representation of the analysed program. Then, it uses a static taint analysis to track potentially distrusted and tainted data values. Finally, analysis results are presented to the user.
|
|
|
Network monitor pro Gnome
Hrozek, Jakub ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Práce představuje novou grafickou aplikaci pro monitorování síťového provozu pro operační systém Linux. Jejím hlavním přinosem je, že je první linuxovou aplikací svého druhu, monitoruje široké spektrum aspektů síťové komunikace a zároveň poskytuje pohodlné grafické rozhraní. Je současně integrována do desktopového prostředí GNOME s možností začlenění do distribuce Fedora. Byly prostudovány a porovnány podobné existující programy, klíčovou částí práce je pak samotný návrh, implementace a testování nástroje.
|
|
|
Správa paměti v Linuxu
Tuček, Jaroslav ; Kočí, Radek (oponent) ; Vojnar, Tomáš (vedoucí práce)
Práce popisuje správu paměti v jádře linuxu. První část je věnována stručnému shrnutí architektury operačních systémů a teorii správy paměti - jmenovitě virtuální paměti, stránkovacím tabulkám, algoritmům stránkování a jádrovým alokátorům. Druhá část se soustřeďuje na vlastní implementaci zmíněných principů ve skutečném operačním systému, linuxu. Součástí je též sada testů navržených pro zjištění chování paměťového správce a krátké zmínění současně existujících omezení včetně jejich navrhovaných řešení.
|
|
|
Verifikace programů s ukazateli založená na detekci vzorů
Kubíček, Jan ; Erlebach, Pavel (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce navazuje na výsledky studií v oblasti verifikace nekonečně stavových systémů. Konkrétně se jedná o oblast abstraktního model checkingu. Seznámili jsme se s metodou založenou na abstrakci paměťové konfigurace pomocí paměťových vzorů. Tato metoda byla navržena pro verifikaci programů pracujících s dynamickými paměťovými strukturami jako například seznamy. Na dynamické paměťové struktury je nahlíženo jako na orientované grafy. Verifikace na základě paměťových vzorů abstrahuje obecně libovolné množství vytvořených uzlů do jednoho sumarizovaného uzlu. Tím se dosáhne reprezentace obecně neukončeného grafu konečným zápisem. Poté je možno efektivně provést verifikaci nad tímto abstrahovaným grafem. V naší práci se zabýváme tvorbou modelu pro nástroj implementující verifikaci na základě paměťových vzorů. Model programu je vytvořen z podmnožiny jazyka C. Hlavním přínosem práce je automatizace tvorby modelu pro verifikaci a tím dosáhnutí úplné automatizovanosti procesu verifikace. Je tak možné verifikovat programy napsané v běžném programovacím jazyce. V této práci je diskutována syntaxe vstupního jazyka i implementační detaily překladu.
|
|
|
GUI pro konfiguraci FTP serveru
Barabas, Maroš ; Janoušek, Vladimír (oponent) ; Vojnar, Tomáš (vedoucí práce)
Obsahom tejto bakalárskej práce je návrh a implementácia grafického konfiguračného nástroja pre ftp server vsftpd, distribuovaný do operačných systémov Red Hat Linux. Dôraz je kladený na jednoduchosť prístupu užívateľov ku konfigurácii servera, komplexnosť v prístupe ku konfiguračným možnostiam a ich škálovateľnosť. Program je integrovaný do desktopového prostredia GNOME.
|
host ::
RSS.