|
Applying formal methods to analysis of semantic differences between versions of software
Nečas, František ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout integraci formálních metod pro DiffKemp, nástroj pro statickou analýzu sémantických rozdílů v rozsáhlých programech napsaných v jazyce C. Cílem tohoto rozšíření je umožnit analýzu složitějších změn, které by typicky byly analyzovatelné spíše nástroji založenými na formálních metodách, a zároveň zachovat škálovatelnost nástroje DiffKemp na velké projekty. Principem navrženého řešení je při analýze v případě nalezení možné sémantické změny zakódovat problém ekvivalence příslušných instrukcí jako instanci problému SMT. Tím je možné sémantický rozdíl potvrdit, nebo vyvrátit s pomocí SMT solveru. Navržené řešení bylo implementováno v nástroji DiffKemp a experimenty provedené na sadě programů zvané EqBench ukazují, že rozšiřuje schopnosti nástroje DiffKemp, převážně v oblasti přesné analýzy úprav aritmetických výrazů.
|
|
Automated Testing of OS Linux Protocol Stack Behaviour During Congestion
Tomašov, Adrián ; Grégr, Matěj (referee) ; Lichtner, Ondrej (advisor)
Táto práca sa zaoberá štúdiom a simuláciou zahltenej siete v laboratorných podmienkach a následne automatizovaným testovaním protokolového zásobníka v operačnom systéme Linux na tejto sieti. Na základe sady experimentov zistíme, aký dopad na správanie protokolového zasobníku má zahltenie siete. Následne bude popísaný spôsob simulácie a emulácie takejto siete fyzickým zariadením. Výstupom tejto práce budú rôzne konfigurácie strojov a emulátorov pre zahltenie siete, a k ním priložená sada meraní s vyhodnotením výsledkov. Tieto konfigurácie budú použité v automatizovanom testovaní jadra operačného systému Linux, aby sa chyby vo vývoji a pri implementácii sieťových protokolov a ovládačov pre sieťové karty našli rýchlejšie.
|
|
System for Verifying the Minimum Resources Required to Run an Application
Žák, Jiří ; Doležal, Jan (referee) ; Smrž, Pavel (advisor)
The main goal of this bachelor thesis is to create a system for the verifying minimum resources required to run an application. The theoretical part deals with the topic of computer performance evaluation metrics and the principle of operation of the Linux operating system. The practical part describes how the design and implementation of the entire system, which uses BPF (Berkeley Packet Filter) technology, was created. The end of the work is completed by testing and evaluation of the whole work. The system was successfully deployed in the partner company BringAuto. It turned out, that the operating system is powerful enough to run applications.
|
|
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.
|
|
System for Verifying the Minimum Resources Required to Run an Application
Žák, Jiří ; Doležal, Jan (referee) ; Smrž, Pavel (advisor)
The main goal of this bachelor thesis is to create a system for the verifying minimum resources required to run an application. The theoretical part deals with the topic of computer performance evaluation metrics and the principle of operation of the Linux operating system. The practical part describes how the design and implementation of the entire system, which uses BPF (Berkeley Packet Filter) technology, was created.The end of the work is completed by testing and evaluation of the whole work. The system was successfully deployed in the partner company BringAuto. It turned out, that the operating system is powerful enough to run applications.
|
|
Establishment of the Linux internet gateway using advanced filtering
Matocha, Tomáš ; Pust, Radim (referee) ; Jelínek, Mojmír (advisor)
The thesis Establishment of the Linux internet gateway using advanced filtering focuses on~the installation of~the Linux operating system on~the older computers, that functions as a gateway to connect clients in the internal network to the Internet. The thesis describes creation an advanced filter with using iptables. Shows some types of security against attacks from the Internet. The other chapters are discussed, advanced traffic control mechanism (such as a TC and a qdisc). The system queue, it is highly beneficial where it is necessary to hierarchically divide traffic between users. It describes types of queue and assembled configurations for clients in the internal network. Next chapter describes the DNS server caching-only type and application denyhosts, which increases the overall security system. Have your own DNS server is certified, especially if we want to reduce the data traffic. Last chapter describes the RADIUS server and its implementation using Apache and MySQL database. Furthermore, the configuration options are described and the examples of the particular configurations are provided. Finally, it presented a system for authentication through the RADIUS server. The thesis seeks to provide a~complex view of security and filtering.
|
|
System for Verifying the Minimum Resources Required to Run an Application
Žák, Jiří ; Doležal, Jan (referee) ; Smrž, Pavel (advisor)
The main goal of this bachelor thesis is to create a system for the verifying minimum resources required to run an application. The theoretical part deals with the topic of computer performance evaluation metrics and the principle of operation of the Linux operating system. The practical part describes how the design and implementation of the entire system, which uses BPF (Berkeley Packet Filter) technology, was created. The end of the work is completed by testing and evaluation of the whole work. The system was successfully deployed in the partner company BringAuto. It turned out, that the operating system is powerful enough to run applications.
|
|
System for Verifying the Minimum Resources Required to Run an Application
Žák, Jiří ; Doležal, Jan (referee) ; Smrž, Pavel (advisor)
The main goal of this bachelor thesis is to create a system for the verifying minimum resources required to run an application. The theoretical part deals with the topic of computer performance evaluation metrics and the principle of operation of the Linux operating system. The practical part describes how the design and implementation of the entire system, which uses BPF (Berkeley Packet Filter) technology, was created.The end of the work is completed by testing and evaluation of the whole work. The system was successfully deployed in the partner company BringAuto. It turned out, that the operating system is powerful enough to run applications.
|
|
Automated Testing of OS Linux Protocol Stack Behaviour During Congestion
Tomašov, Adrián ; Grégr, Matěj (referee) ; Lichtner, Ondrej (advisor)
Táto práca sa zaoberá štúdiom a simuláciou zahltenej siete v laboratorných podmienkach a následne automatizovaným testovaním protokolového zásobníka v operačnom systéme Linux na tejto sieti. Na základe sady experimentov zistíme, aký dopad na správanie protokolového zasobníku má zahltenie siete. Následne bude popísaný spôsob simulácie a emulácie takejto siete fyzickým zariadením. Výstupom tejto práce budú rôzne konfigurácie strojov a emulátorov pre zahltenie siete, a k ním priložená sada meraní s vyhodnotením výsledkov. Tieto konfigurácie budú použité v automatizovanom testovaní jadra operačného systému Linux, aby sa chyby vo vývoji a pri implementácii sieťových protokolov a ovládačov pre sieťové karty našli rýchlejšie.
|
|
OS Chrome and the Chromium project
Pelcová, Lenka ; Vaněk, Jiří (advisor) ; Masner, Jan (referee)
The topic of this bachelor thesis is Google Chrome web-based operating system and open source Chromium project. In theoretical part of the thesis, general problematics of operating systems is shortly described, followed by the development of OS Chrome, description of the system architecture, and introduction of special hardware for usage of Chrome OS
The practical part is focused on the market analysis both in the Czech Republic and globally, including future prognoses, and comparison to Windows operating systems. Through a survey, knowledge of OS Chrome among people and most frequent usage in computers and laptops is found out. A comparison between OS Chrome and Windows 8.1 is made in these tasks.
|