|
Applying formal methods to analysis of semantic differences between versions of software
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an integration of formal methods into DiffKemp, a static analysis tool for analyzing semantic differences of large-scale C projects. The aim of this extension is to facilitate analysis of more complex code changes, which would typically be better handled by a tool based on formal methods, while also maintaining DiffKemp’s scalability to large projects. To achieve this, whenever a possible semantic change is found, the equivalence of the relevant instructions is encoded into an SMT problem instance and the difference is either confirmed or refuted using an SMT solver. The proposed solution has been implemented in DiffKemp and our experiments on a set of benchmarks called EqBench show that it extends the capabilities of DiffKemp, mainly with regards to sound analysis of refactorings of arithmetic expressions.
|
|
Automated Testing of OS Linux Protocol Stack Behaviour During Congestion
Tomašov, Adrián ; Grégr, Matěj (oponent) ; Lichtner, Ondrej (vedoucí práce)
This thesis is focused on observing and simulating network congestion in laboratory conditions, and on automated testing of the protocol stack in the Linux operating system during network congestion. We perform a set of experiments to find the impact of network congestion on the protocol stack. The simulation and emulation method of this network using physical device will be described. The outcome of this thesis are various configurations of devices and emulators for network congestion together with measurements and evaluation of results. These configurations will be used for automated testing of the kernel of the Linux operating system to catch development errors, network protocol stack errors and card driver error earlier.
|
|
Systém pro ověření minimálních potřebných zdrojů pro běh aplikace
Žák, Jiří ; Doležal, Jan (oponent) ; Smrž, Pavel (vedoucí práce)
Cílem této bakalářské práce je vytvořit systém pro ověření minimálních potřebných zdrojů pro běh aplikace. Teoretická část se věnuje tématu vyhodnocovacích metrik počítačového výkonu a principu fungování operačního systému Linux. V praktické části je popsáno, jak byl vytvořen návrh a implementace celého systému, který využívá technologii BPF (Berkeley Packet Filter). Práce je završena testováním a vyhodnocením celé práce. Systém byl úspěšně nasazen v partnerské firmě BringAuto. Ukázalo se, že daný operační systém je dostatečně výkonný pro běh aplikací.
|
|
Metody útoků na operační systém Linux
Procházka, Boris ; Malinka, Kamil (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato bakalářská práce se zaměřuje na bezpečnost Linuxového jádra z útočníkova pohledu. Snaží se identifikovat a zmapovat veškeré charakteristické rysy a metody používané dnešními počítačovými piráty. Jedním z cílů této práce je poskytnout komplexní pohled na danou problematiku. Ve výsledku tak může sloužit jako malá referenční příručka komukoliv, kdo má zájem o rozšíření znalostí z oblasti jaderné bezpečnosti. Práce se skládá ze čtyř částí. První opakuje a definuje nejzákladnější pojmy a členění z oblasti operačních systémů. Druhá a třetí část tvoří jádro práce. Zahrnují principy a metody používané pro skrytí procesů, souborů, spojení apod. Poslední kapitola je věnována doprovodným tématům. Přílohou k této bakalářské práci je skupina jaderným modulů, které demonstrují diskutované problémy, a tabulky, porovnávající současné rootkity.
|
|
Systém pro ověření minimálních potřebných zdrojů pro běh aplikace
Žák, Jiří ; Doležal, Jan (oponent) ; Smrž, Pavel (vedoucí práce)
Cílem této bakalářské práce je vytvořit systém pro ověření minimálních potřebných zdrojů pro běh aplikace. Teoretická část se věnuje tématu vyhodnocovacích metrik počítačového výkonu a principu fungování operačního systému Linux. V praktická části je popsáno, jak byl vytvořen návrh a implementace celého systému, který využívá technologii BPF (Berkeley Packet Filter). Konec práce je završený testováním a vyhodnocením celé práce. Systém byl úspěšně nasazen v partnerské firmě BringAuto. Ukázalo se, že daný operační systém je dostatečně výkonný pro běh aplikací.
|
|
Realizace internetové brány na Linuxu s pokročilým filtrováním
Matocha, Tomáš ; Pust, Radim (oponent) ; Jelínek, Mojmír (vedoucí práce)
Práce Realizace internetové brány na Linuxu s pokročilým filtrováním se soustřeďuje na~instalaci operačního systému Linux na~starší počítače, který plní funkci jako brána pro připojení klientů ve~vnitřní síti do internetu. V práci je uveden popis vytvoření pokročilého filtrování s~pomocí iptables. Ukazuje některé typy bezpečnosti proti útokům z Internetu. V~dalších kapitolách jsou probrány pokročilé mechanismy řízení provozu (jako tc a qdisc). Tento systém front se ukazuje jako velice přínosný všude tam, kde je potřeba hierarchicky dělit provoz mezi uživatele. Jsou popsány typy front a~sestavena konfigurace pro klienty ve vnitřní síti. Dále je uvedeno použití dns serveru typu caching-only a také aplikace denyhosts, která zvyšuje celkovou bezpecnost systému. Mít vlastní DNS server se osvědčuje, zejména pokud chceme snížit datový provoz. Poslední kapitola se zabývá radius serverem a jeho implementací s použitím apache a databáze mysql. Popsány jsou možnosti některých konfiguračních voleb jednotlivých služeb a také uvedeny příklady konfigurací. Nakonec je předveden systém pro autentizaci uživatelů skrze RADIUS server. Celá práce se snaží poskytnout komplexní pohled na problematiku bezpečnosti a~filtrování.
|
|
Systém pro ověření minimálních potřebných zdrojů pro běh aplikace
Žák, Jiří ; Doležal, Jan (oponent) ; Smrž, Pavel (vedoucí práce)
Cílem této bakalářské práce je vytvořit systém pro ověření minimálních potřebných zdrojů pro běh aplikace. Teoretická část se věnuje tématu vyhodnocovacích metrik počítačového výkonu a principu fungování operačního systému Linux. V praktické části je popsáno, jak byl vytvořen návrh a implementace celého systému, který využívá technologii BPF (Berkeley Packet Filter). Práce je završena testováním a vyhodnocením celé práce. Systém byl úspěšně nasazen v partnerské firmě BringAuto. Ukázalo se, že daný operační systém je dostatečně výkonný pro běh aplikací.
|
|
Systém pro ověření minimálních potřebných zdrojů pro běh aplikace
Žák, Jiří ; Doležal, Jan (oponent) ; Smrž, Pavel (vedoucí práce)
Cílem této bakalářské práce je vytvořit systém pro ověření minimálních potřebných zdrojů pro běh aplikace. Teoretická část se věnuje tématu vyhodnocovacích metrik počítačového výkonu a principu fungování operačního systému Linux. V praktická části je popsáno, jak byl vytvořen návrh a implementace celého systému, který využívá technologii BPF (Berkeley Packet Filter). Konec práce je završený testováním a vyhodnocením celé práce. Systém byl úspěšně nasazen v partnerské firmě BringAuto. Ukázalo se, že daný operační systém je dostatečně výkonný pro běh aplikací.
|
|
Automated Testing of OS Linux Protocol Stack Behaviour During Congestion
Tomašov, Adrián ; Grégr, Matěj (oponent) ; Lichtner, Ondrej (vedoucí práce)
This thesis is focused on observing and simulating network congestion in laboratory conditions, and on automated testing of the protocol stack in the Linux operating system during network congestion. We perform a set of experiments to find the impact of network congestion on the protocol stack. The simulation and emulation method of this network using physical device will be described. The outcome of this thesis are various configurations of devices and emulators for network congestion together with measurements and evaluation of results. These configurations will be used for automated testing of the kernel of the Linux operating system to catch development errors, network protocol stack errors and card driver error earlier.
|
|
OS Chrome a projekt Chromium
Pelcová, Lenka ; Vaněk, Jiří (vedoucí práce) ; Masner, Jan (oponent)
Tématem bakalářské práce je webově orientovaný operační systém Google Chrome a open source projekt Chromium. V teoretické části práce je krátce nastíněna obecná problematika operačních systémů, dále je sledován vývoj OS Chrome od představení po aktuální verzi, uvedena architektura, na které je systém postaven, a na jakém hardwaru se používá.
Praktická část práce se zaměřuje na analýzu pozice systému na trhu jak v České republice, tak ve světě, včetně prognóz do budoucna, a porovnání s operačními systémy Windows. Pomocí dotazníkového šetření je zjištěno povědomí o OS Chrome, dále analyzovány činnosti, ke kterým jsou notebooky a počítače nejčastěji používány. V nich je pak porovnán OS Chrome s OS Windows 8.1.
|