|
|
Efektivní knihovna pro práci s konečnými stromovými automaty
Lengál, Ondřej ; Konečný, Filip (oponent) ; Vojnar, Tomáš (vedoucí práce)
Mnoho současných počítačových systémů používá dynamické datové či řídicí struktury předem neomezené velikosti. Tyto datové struktury mají často charakter stromů nebo se dají zakódovat jako stromy s některými dodatečnými ukazateli nad stromovou kostrou. Této skutečnosti využívají některé v současné době intenzivně studované techniky formální verifikace, které reprezentují nekonečně mnoho stavů konečným stromovým automatem. Nicméně v současnosti neexistuje efektivní a flexibilní implementace knihovny pro stromové automaty, která by byla pro tyto techniky vhodná. Cílem této diplomové práce je takovouto knihovnu poskytnout. Předložený text nejdříve popisuje základy teorie konečných stromových automatů a regulárních stromových jazyků. Dále jsou prozkoumány existující implementace knihoven pro stromové automaty a různé verifikační techniky pro systémy se stromovou strukturou. Poté se text zaobírá návrhem reprezentace stromového automatu a algoritmů provádějících standardní jazykové operace nad touto reprezentací, načež následuje popis implementace knihovny. Prostřednictvím provedených experimentů ukazujeme, že knihovna může konkurovat ostatním dostupným knihovnám pro práci se stromovými automaty, přičemž její výkon v určitých oblastech je řádově vyšší.
|
|
|
Útoky na operační systém Linux v teorii a praxi
Procházka, Boris ; Hanáček, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato diplomová práce se zaměřuje na bezpečnost linuxového jádra z pohledu útočníka. Mapuje metody a techniky skrývání výpočetních prostředků používané dnešními počítačovými piráty. Práce přináší unikátní metodu útoku na rozhraní systémových volání, kterou implementuje v podobě dvou nástrojů (tzv. rootkitů). Práce je rozdělena na teoretickou a praktickou část. Velký důraz je kladen především na praktickou část, která formou experimentů předkládané informace ověřuje a ukazuje jejich reálné použití. Čtenář je postupně veden až k tvorbě jedinečného rootkitu, který dokáže infiltrovat linuxové jádro nově objevenou metodou, a to i bez podpory dynamicky zaveditelných modulů. Část práce se zabývá i problematikou, jak diskutované útoky detekovat a jak se proti nim účinně bránit.
|
|
|
Nástroj pro vyvolávání chyb založený na infrastrukuře Systemtap
Zelinka, Martin ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Práce popisuje různé metody vkládání chyb, princip systémových volání v operačním systému Linux a nástroj Systemtap. Hlavním cílem práce je návrh a implementace aplikace pracující na principu vkládání chyb do systémových volání pomocí nástroje Systemtap. Realizovaná aplikace si nejprve automaticky identifikuje existující systémová volání s jejich chybovými návratovými hodnotami, kterými jsou potom nahrazovány původní návratové hodnoty systémových volání.
|
|
|
Model checking nekonečně stavových systémů založený na inferenci jazyků
Rozehnal, Pavel ; Křena, Bohuslav (oponent) ; Vojnar, Tomáš (vedoucí práce)
Regulární model checking je metoda pro verifikaci nekonečně stavových systémů. Je založena na kódování jejich konfigurace jako slov nad konečnou abecedou, množiny konfigurací jako konečného automatu a přechodů jako konečných transducerů. Je zde představen nový přístup k regulárnímu model checkingu založený na odvozování regulárních jazyků. Metoda je založena na prozkoumávání nekonečně stavového systému, jehož chování může být modelováno použitím transducerů, které zachovávají délku řetězců a jejich aplikací je možné získat všechny dosažitelné konfigurace systému. Naše metoda regulárního model checkingu je založena na odvozování regulárních jazyků pomocí algoritmu Angluin, který je použit pro nalezení vhodného invariantu (nadaproximace), který je schopen zodpovedět otázku zachování či porušení nějaké vlastnosti. Je zde také uveden úvod do teorie konečných automatů, model checkingu, SAT problémů a popis Angluinova a Biermanova algoritmu pro učení konečných automatů.
|
|
|
Řídicí systém pro testování linuxových aplikací
Beneš, Eduard ; Vojnar, Tomáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Táto práca sa zaoberá problematikou riadiaceho systému pre testovanie linuxových aplikácií. Práca poukazuje na dôležitosť testovania software a jeho kvality pomocou automatizovaných softwarových nástrojov. Red Hat Test System (RHTS) je jedným z mnohých testovacích nástrojov. Predstavené sú rozdielne prístupy k ich klasifikácii a vyhodnocovaniu. Vybrané nástroje sú vyhodnotené a porovnané so systémom RHTS. V tejto práci je navrhnutý systém pre neinteraktívne testovanie linuxových aplikácií s podporou pre RHTS testy a s dôrazom na budúce rozšírenia. Implementovaný systém je následne otestovaný pomocou navrhnutých testov a popísaných je niekoľko príkladov použitia.
|
|
|
Rozpoznávání podobností souborů na základě chování
Otočka, Dávid ; Vojnar, Tomáš (oponent) ; Peringer, Petr (vedoucí práce)
Cílem práce bylo navrhnout algoritmus, který na základě výstupu z analýzy chovaní programu, dokáže stanovit míru podobnosti s jinými programy. Pro potřeby algoritmu byla upravena Levenshteinova metoda pro výpočet rozdílu mezi dvěma řetězci a metoda NCD. U obou metod je v práci uveden spůsob jejich implementace a výsledky testů. V práci jsou popsány způsoby analýzy programů v prostředí virtuálního počítače i vysvětlení některých základních pojmů týkajících se analýzy škodlivého kódu.
|
|
|
Statická analýza možných hodnot proměnných v programech v C
Ďuričeková, Daniela ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
Analýza rozsahu hodnot (anglicky value-range analysis) je metoda statické analýzy založená na zjišťování hodnot, kterých může daná proměnná nabývat v určitém místě v programu. Tato technika může být použita k dokázání, že se v programu nevyskytují chyby za běhu, jako například přístup za hranici pole. Jelikož analýza rozsahu hodnot získává informace o každém místě v programu, lze k její implementaci využít analýzu toku dat (anglicky data-flow analysis). Cílem této diplomové práce je návrh a implementace funkčního nástroje provádějícího analýzu rozsahu hodnot. Práce začíná úvodem do problematiky, vysvětlením analýz toku dat a hodnot proměnných a popisem abstraktní interpretace, která tvoří formální základ analyzátoru. Následuje seznámení s prostředím Code Listener, které bylo využito k implementaci analyzátoru. Jádro práce tvoří návrh, implementace a otestování analyzátoru. V závěru jsou shrnuty nabyté zkušenosti a diskutovány možnosti budoucího vývoje vytvořeného nástroje.
|
|
|
Dynamická detekce a léčení časově závislých chyb nad daty v prostředí Java
Letko, Zdeněk ; Kolář, Dušan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Hledání chyb plynoucích ze souběžného zpracovávání výpočtů je obtížné. Proto se tato diplomová práce zabývá detekcí a léčením časově závislých chyb nad daty a chyb plynoucích z nesprávné atomicity operací v prostředí Java. Práce prezentuje dva různé algoritmy pro detekci. Jedním z nich je nový algoritmus nazvaný AtomRace, který detekuje časově závislé chyby nad daty jako speciální případ nesprávné atomicity operací. Následné léčení detekovaných chyb je založeno na potlačení opakování chyby, buď zavedením přídavné synchronizace, nebo legálním ovlivňováním plánovače Javy, za účelem vynucení správné atomicity operací. Navržená architektura, která pracuje souběžně se sledovaným programem, využívá ke sledování a ovlivňování výpočtu techniku instrumentace na úrovni Java bytecode. Architektura a algoritmy byly implementovány a otestovány v několika případových studiích.
|
|
|
Sdílená tabule
Řezník, Jaroslav ; Mazal, Zdeněk (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem projektu "Sdílená tabule" je navrhnout a implementovat aplikaci, která umožní spolupráci na skupinových projektech v reálném čase v síťovém prostředí. Komunikace může probíhat jak pomocí textových zpráv, tak multimediálně pomocí kreslení na sdílené tabuli, vkládáním interaktivních objektů a hlasovou či video komunikací. V rámci semestrální části projektu se řeší využití interaktivních tabulí, návrh komunikačního protokolu a grafického uživatelského rozhraní. V diplomové práci následně implementace aplikace.
|
|
|
Mikrojádra operačních systémů
Beneš, Eduard ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
Táto práca sa zaoberá problematikou mikrojadier operačných systémov. Prvá časť je zameraná na oboznámenie s problematikou jadier operačných systémov. Obsahuje základné vlastnosti a mechanizmy druhej generácie mikrojadier reprezentovanej mikrojadrom L4, na ktoré sa zameriavame v ďalších častiach práce. Následne sú opísané dva rôzne porty operačného systému Linux nad mikrojadro L4, sú to L4Linux a Wombat. V druhej časti práce je popísaný spôsob inštalácie vybraných portov a hlavné problémy, ktoré sme museli riešiť. Tretia a štvrtá časť sú zamerané na problematiku testovania výkonnosti nainštalovaných systémov. Popisujeme metodológiu zvolených experimentov a význam jednotlivých testov. Výsledky, spolu s ich vyhodnotením, sú uvedené vo štvrtej časti. Pokiaľ to je vhodné, získané výsledky konfrontujeme medzi sebou, prípadne s výsledkami testov získaných z Internetu. V záverečnej časti je na základe nadobudnutých znalostí uvedená stručná diskusia na tému možností uplatnenia mikrojadier.
|
host ::
RSS.