|
|
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.
|
|
|
A Fault Injection Bug Hunting Tool Based on Systemtap
Zelinka, Martin ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
This work describes different methods of fault injection, the principles of system calls in operating system Linux and the Systemtap tool. The main aim of thesis is design and implementation of the application that work on the principle of fault injection into the system calls using Systemtap tool. Implemented application automatically identifies the existing system calls with the error return values, which are then replaced the original system calls return value.
|
|
|
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.
|
|
|
Static Value Analysis over C Programs
Ďuričeková, Daniela ; Peringer, Petr (referee) ; Vojnar, Tomáš (advisor)
Value-range analysis is a static analysis technique based on arguing about the values that a variable may take on a given program point. It can be used to prove absence of run-time errors such as out-of-bound array accesses. Since value-range analysis collects information on each program point, data-flow analysis can be used in association with it. The main goal of this work is designing and implementing such a value-range analysis tool. The work begins with an introduction into the topic, an explanation of data-flow and value-range analyses and a description of abstract interpretation, which provides the formal basis of the analyser. The core of this work is the design, implementation, testing and evaluation of the analyser. In the conclusion, our personal experience obtained in the area of the thesis is mentioned, along with a discussion of a possible future development of the designed tool.
|
|
|
Model Checking Infinite-State Systems Using Language Inference
Rozehnal, Pavel ; Křena, Bohuslav (referee) ; Vojnar, Tomáš (advisor)
Regular model checking is a method for verifying infinite-state systems based on coding their configurations as words over a finite alphabet, sets of configurations as finite automata, and transitions as finite transducers. We implement regular model checking using inference of regular languages. The method builds upon the observations that for infinite-state systems whose behavior can be modeled using length-preserving transducers, there is a finite computation for obtaining all reachable configurations. Our new approach to regular model checking via inference of regular languages is based on the Angluin's L* algorithm that is used for finding out an invariant which can answer our question whether the system satisfies some property. We also provide an intro to the theory of finite automata, model checking, SAT solving and Anguin's L* and Bierman algorithm of learning finite automata.
|
|
|
Microkernels of Operating Systems
Beneš, Eduard ; Peringer, Petr (referee) ; Vojnar, Tomáš (advisor)
This thesis discusses the area of microkernel based operating systems. The first part is focused on the familiarization with the issue of the operating system kernel. This part contains the basic characteristics and mechanisms of the second generation microkernels represented by the microkernel L4, on which there is major focus in other parts of the thesis. Subsequently, there are described two different ports of the operating system Linux on top of L4 microkernel and those are L4Linux and Wombat. In the second part of the thesis, the method of the installation of the given ports is depicted and the main problems the author had to face. The third and forth part are focused on the issue of testing the performance of the installed systems. The methodology of chosen experiments is described and the meaning of the individual tests explained. The results, as well as their evaluation are stated in the forth part. If suitable, the gained results are compared with each other, or with the results gained from the Internet. In the last part, a short discussion is conducted based on the gained knowledge on the issue of the possibilities of microkernel application.
|
|
|
SELinux Policy Analysis Tool
Mojžíš, Vít ; Peringer, Petr (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá analýzou politik pro bezpečnostní moduly založené na mandatorním řízení přístupu (MAC), se zaměřením na SELinux. Vzhledem k omezeným schopnostem dostupných nástrojů byl navržen a implementován nový nástroj. Jeho hlavní cíle jsou usnadnění vývoje bezpečnostních politik a pomoc při odhadu role SELinuxu v zabezpečení systému. V případě úspěšného nasazení bude nový nástroj začleněn do balíčku nástrojů SETools 4.
|
|
| |
|
|
Git Reporting Tool
Nečas, Vojtěch ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
This bachelor thesis is about an implementation of the software tool dedicated for creation and visualization of statistical information files work. It also refers about Git version control system. System Git does not have any functions to display graphical statistics (graph or chart), therefore the output of the changes of the files is available in command line only. Such data, especially in a large amount of specific files, are not easy to analyze without using other existing statistic tools. There are couple of tools available which are capable of getting information of changes in Git, classify the statistics and display the results. The main disadvantage of such tools is a very long time needed to obtain the results. These tools support only very brief statistics and the user interface does not provide sufficient comfort either. The tool elaborated in this paper is offering more effective access to the changes information from Git using the saved data database. This database, compare to a single command line, is offering quick access to all information and timeline while there is only one time demanding operation - setting up the database. User-friendly interface is enabling an easy operation of the tool itself using window based interface. As a result there are various statistics (graphs and charts) which are user-editable. On the top of that the tool is equipped with an approximate estimation of the project work trends (mathematical-statistical method of the least squares).
|
|
|
Shared Board
Řezník, Jaroslav ; Mazal, Zdeněk (referee) ; Vojnar, Tomáš (advisor)
The aim of the "Shared Board" project is to design and implement an application that will allow a real-time collaboration on workgroup projects in a network environment. The communication can be accomplished using Instant Messaging or multimedia whiteboard with a possibility of drawing, attaching interactive objects and combined with voice and video communication. The term project part solves utilization of interactive whiteboards, design of communication protocol and grafical user interface. Implementation is solved as masters thesis part.
|
guest ::
