|
|
Static Behavioral Malware Detection over LLVM IR
Surovič, Marek ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá metodami pro behaviorální detekci malware, které využívají techniky formální analýzy a verifikace. Základem je odvozování stromových automatů z grafů závislostí systémových volání, které jsou získány pomocí statické analýzy LLVM IR. V rámci práce je implementován prototyp detektoru, který využívá překladačovou infrastrukturu LLVM. Pro experimentální ověření detektoru je použit překladač jazyka C/C++, který je schopen generovat mutace malware za pomoci obfuskujících transformací. Výsledky předběžných experimentů a případná budoucí rozšíření detektoru jsou diskutovány v závěru práce.
|
|
|
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.
|
|
|
Improved Integration of SSSD and SUDO
Šrubař, Michal ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
The purpose of this thesis is to improve integration between SUDO and SSSD with a fo- cus on improved support of SUDO rules stored on an FreeIPA server in the native IPA SUDO scheme. It presents documentation of LDAP SUDO provider and also the design and implementation of a native IPA SUDO provider. The designed provider eliminates an unnecessary overhead of exporting SUDO rules from IPA SUDO schema to native LDAP SUDO scheme on an FreeIPA server.
|
|
|
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.
|
|
|
Symbolic Representation of Finite Automata
Chromečka, Jiří ; Vojnar, Tomáš (referee) ; Lengál, Ondřej (advisor)
In formal analysis we often encounter finite automata with a~large amount of states over large alphabets. Their explicit representation can result in a~state explosion and this problem can be solved by the use of symbolic representation that can manipulate a~whole set of states at once. The aim of this work is to extend the libVATA library to support such a~representation including algorithms for some operations on this representation. The presented text first deals with prerequisites necessary to undestand finite automata and binary decision diagrams used for their symbolic representation. Then it lists some existing libraries for work with finite automata. Next follows the core of this work, the~design of a~symbolic representation and operations on it, which are later implemented in the previously mentioned library. The test results proves that the symbolic representation is an interesting alternative to the explicit representation.
|
|
|
Static Analysis for Discovering Security Vulnerabilities in Web Applications on the Asp.Net Platform
Říha, Jakub ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Tato bakalářská práce popisuje jak teoretické základy, tak způsob vytvoření statického analyzátoru založeném na platformě .NET Framework a službách poskytnutých prostřednictvím .NET Compiler Platform. Tento analyzátor detekuje bezpečnostní slabiny typu SQL injection na platformě ASP.NET MVC. Analyzátor nejdříve sestrojuje grafy řízení toku jako abstraktní reprezentaci analyzovaného programu. Poté využívá statické analýzy pro sledování potenciálně nedůvěryhodných dat. Nakonec jsou výsledky analýzy prezentovány uživateli.
|
|
|
Network Monitor for Gnome
Hrozek, Jakub ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The thesis presents a new network monitoring application for the Linux operating system. It is the first graphical application with such functionality which monitors wide range of network traffic aspects and operates in graphical environment. It is integrated into the GNOME desktop environment and is also integrated into Fedora Linux distribution. The thesis discusses similar existing tools, the key part of the thesis is design, implementation and testing of the application.
|
|
|
Memory Management in Linux
Tuček, Jaroslav ; Kočí, Radek (referee) ; Vojnar, Tomáš (advisor)
This work describes the memory manager subsystem of the linux kernel. The first part gives a brief account of operating systems architecture and memory management theory - of virtual memory management, page tables, page replacement algorithms and kernel allocators in particular. The second part discusses the actual implementation of these principles in a modern kernel - in linux. Finally, a series of tests stressing the memory subsystem is conducted to determine the memory manager's real behaviour. Limitations of the current linux kernel memory management and some of their proposed solutions are also discussed.
|
|
|
Verification of Programs with Pointers Based on Pattern Detection
Kubíček, Jan ; Erlebach, Pavel (referee) ; Vojnar, Tomáš (advisor)
This paper presents our results in study of verifiaction of infinite state space systems. We deal more concretely with abstract model checking. As main part of study we learned about pattern-based verification. This method is supposed to verify programs with dynamic memory structures like lists. Those structures are presented as directed graph. Pattern-based verifiaction abstracts any number of nodes by replacing them with summarized node. This way we achieve bounded presentation of unbounded memory structure. Afterwards, verification is very effective due to low number of possible memory configurations. In our own work we deal with making model of a program for a tool that implements pattern-based verification. This model isconstructed from a subset of the C language. The main contribution of work is making the verification of simple programs written in C language completely self-acting by automation of constructing input model. In this paper wepresent the grammar of created subset of the C language and implementation details of translation.
|
|
|
A GUI for Configuring an FTP Server
Barabas, Maroš ; Janoušek, Vladimír (referee) ; Vojnar, Tomáš (advisor)
The subject of this document is concept and implementation of graphical configuration tool for vsftpd ftp server, which is distributed to Red Hat Linux operating systems. Mainly, the document puts accent on simplicity of user's access to server configuration, complexity of access to configuration options and their scalability. The program is integrated to GNOME desktop enviroment.
|
guest ::
