|
|
Automated Formal Verification of Program Correctness Using SDV, Copper, or Similar Tools
Kovalič, Peter ; Šimáček, Jiří (referee) ; Vojnar, Tomáš (advisor)
This thesis is concerning about verification of drivers. Principally is focused on model checking tools, from which the Static Driver Verifier is the most important. A driver Ext2Fsd is checked by this program. This driver belongs to group of file system drivers. Control is driven by entered rules, which the driver must not violate. The aim of this thesis was to verify chosen driver by selected tool. The results have covered all three types of verification´s end. There were rules that driver passed, that driver violated and also that driver didn´t accept. The final chapter of work is about another model checking tool Copper. It offers the basic knowledge about this program.
|
|
|
Plugins for Getting Information about the System for BusyBox
Poláček, Marek ; Konečný, Filip (referee) ; Vojnar, Tomáš (advisor)
In this thesis, we discuss implementation of tools for getting information from the system. We examine file systems sysfs and procfs in the Linux operating system. Furthermore, we discourse how to write small programs in the C language. Eventually, we take a look at implementation of tools like iostat, mpstat and powertop. These tools were implemented in a minimalistic form suitable for Busybox within this thesis.
|
|
|
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.
|
|
|
Automated Methods of Finding Bugs in Compilers
Müller, Petr ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
This thesis discusses an application of the fuzz testing method for testing compilers and interpreters. In the first part, it deals with compilers, optimizations, and bugs typical for an optimizing compiler. It analyzes applicability of static and dynamic analysis methods for searching such bugs and proposes dynamic fuzz testing as suitable for this task. A compiler testing tool suite using this method was implemented within this thesis and applied on several real compilers, including GCC, in which the tool revealed a series of bugs.
|
|
|
Methods of Linux Kernel Hacking
Procházka, Boris ; Malinka, Kamil (referee) ; Vojnar, Tomáš (advisor)
This bachelor thesis focuses on the Linux kernel security from the attacker perspective. It tries to identify and map all key features and methods used by nowadays cyber-terrorists. One of its aims is to give a comprehensive overview of this topic. At final, it can serve as a small reference for everybody who wants to broaden his knowledge of Linux kernel security. The work consists of four parts. The first part repeats and defines basic notions and taxonomy of operation systems. The second and third part form the core. They cover principles and methods used to hide processes, files, connections, etc. The last chaper is devoted to related issues. A supplement of this bachelor thesis is a set of demonstrating modules, which implement discussed problems involved, and tables, where can be found a comparison of nowadays rootkits.
|
|
|
Techniques of Virtualisation of Computing Platforms in Linux
Župka, Jiří ; Kumpošt, Marek (referee) ; Vojnar, Tomáš (advisor)
The thesis tests and compares various existing virtualization tools for virtualization of computing platforms and explains important conceptions of virtualization technology. It's main contribution is a performance, efficiency, scalability and robustness comparison of virtualization tools. This comparison should help the Redhat company to make a decision whether they should leave XEN as a main virtualization tool in their distributions and move on to another newer and more user friendly virtualization tool like KVM.
|
|
|
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.
|
|
|
Selected Extensions of the Albegraic System Octave
Salač, Radek ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
This work deals with issues linked to solving system of linear equations in the environment of numerical computer. It describes the fundamental algorithms emphasizing their positive as well as negative sides. The work is devoted to general issues such as time complexity and memory demandingness of given algorithms. In the last part, the process of implementation of selected procedures into the algebraic system Octave is described.
|
|
|
Implementation of an ifplugd Plugin to the BusyBox Project
Kryzhanovskyy, Maksym ; Šimáček, Jiří (referee) ; Vojnar, Tomáš (advisor)
This work deals with porting the ifplugd daemon to BusyBox project. The first part gives introductory information about the BusyBox project, and looks into the structure of the application. The second part deals with the implementation of the ifplugd daemon. As part of this work was carried out partial adjustments in the BusyBox code and ifplugd daemon has been implemented as an applet of the BusyBox package. At the conclusion of this work are discussed the results.
|
|
|
A Tool for Analyzing Performance of Memory Allocators in Linux
Müller, Petr ; Peringer, Petr (referee) ; Vojnar, Tomáš (advisor)
This diploma thesis presents a tool for dynamic memory allocator analysis, focused on their performance. The work identifies the important memory allocator performance metrics, as well as the environment and program factors influencing these metrics. Using this knowledge, a tool was designed and implemented. This tool allows to gather and analyze these metrics. The tool provides the ability to create memory allocator usage scenarios for the purpose of the allocator behavior analysis under different conditions. The tool was tested on several available memory allocators with free license.
|
guest ::
