|
|
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ů.
|
|
|
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.
|
|
|
SELinux Policy Analysis Tool
Mojžíš, Vít ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis deals with mandatory access control (MAC)-based security module policy analysis, focusing on SELinux. Because of insuffient capabilities of available analysis tools, new tool was designed and implemented with the needs of Red Hat SELinux team in mind. Its main uses will be as aid in policy development and support in SELinux usefulness evaluation. If the tool proves useful, it will be incorporated into SELinux userspace tools package SETools 4.
|
|
|
Refactoring and Verification of the Code of mkfs xfs
Ťulák, Jan ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work describes the processes of refactoring mkfs.xfs program for a purpose of refining its code and cleaning the technical debt accumulated over 20 years of the program’s existence. The mkfs.xfs source code is then a subject to static analysis and the used tools (CppCheck, Coverity, Codacy, GCC, Clang) are compared in terms of the number and type of the found defects.
|
|
|
Reportovací nástroj nad git
Nečas, Vojtěch ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
Bakalářská práce se zabývá implementací softwarového nástroje pro vytváření a vizualizaci statistických informací o práci v souborech, které sleduje systém správy verzí - Git. Systém Git nemá funkce pro grafické znázornění statistik (grafem nebo tabulkou) a výstup informací o změnách v souborech je pouze v příkazovém řádku. Taková data, zejména u velkého počtu sledovaných souborů, není snadné analyzovat bez použití jiných existujících statistických nástrojů. Existuje několik nástrojů, které umí získat informace o změnách v Git, vyhodnotit statistiky a zobrazit výsledky. Hlavním problémem u těchto nástrojů je příliš dlouhá doba potřebná pro získání výsledků, podpora jen velmi stručných statistik nebo slabé uživatelské rozhraní. Nástroj implementovaný v této práci řeší efektivnější vyhodnocení výsledků pomocí databáze pro uložení informací o změnách z Git. Databáze oproti příkazovému řádku poskytuje rychlý přístup k uloženým informacím a časově náročné je pouze její založení. Snadné ovládaní nástroje zajišťuje grafické uživatelské rozhraní pomocí oken. Výsledkem jsou statistiky, které si může uživatel i přizpůsobit podle vlastních potřeb (která data budou zahrnuta a jejich rozsah). Navíc nástroj poskytuje přibližný odhad (matematicko-statistickou metodou nejmenších čtverců), jakým směrem se práce ve sledovaném projektu ubírá (zda je ve fázi vývoje, nebo dokončování a údržby).
|
|
|
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.
|
|
|
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.
|
|
|
Verifikace programů s ukazateli založená na detekci vzorů
Kubíček, Jan ; Erlebach, Pavel (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce navazuje na výsledky studií v oblasti verifikace nekonečně stavových systémů. Konkrétně se jedná o oblast abstraktního model checkingu. Seznámili jsme se s metodou založenou na abstrakci paměťové konfigurace pomocí paměťových vzorů. Tato metoda byla navržena pro verifikaci programů pracujících s dynamickými paměťovými strukturami jako například seznamy. Na dynamické paměťové struktury je nahlíženo jako na orientované grafy. Verifikace na základě paměťových vzorů abstrahuje obecně libovolné množství vytvořených uzlů do jednoho sumarizovaného uzlu. Tím se dosáhne reprezentace obecně neukončeného grafu konečným zápisem. Poté je možno efektivně provést verifikaci nad tímto abstrahovaným grafem. V naší práci se zabýváme tvorbou modelu pro nástroj implementující verifikaci na základě paměťových vzorů. Model programu je vytvořen z podmnožiny jazyka C. Hlavním přínosem práce je automatizace tvorby modelu pro verifikaci a tím dosáhnutí úplné automatizovanosti procesu verifikace. Je tak možné verifikovat programy napsané v běžném programovacím jazyce. V této práci je diskutována syntaxe vstupního jazyka i implementační detaily překladu.
|
|
|
Practical Application of Facebook Infer on Systems Code
Beránek, Tomáš ; Malík, Viktor (oponent) ; Vojnar, Tomáš (vedoucí práce)
Static analysis is nowadays often used in the development process to find defects in the produced software. Although static analysis tools can effectively find bugs in software with millions of lines of code, they have also some disadvantages. The main disadvantages are the difficulty to deploy the chosen tool on the given project, high numbers of false reports, and the time and space requirements. This thesis focuses on mitigating these negative features of the Facebook Infer tool mainly for the context of using it to analyse Linux utilities shipped as SRPM packages. To simplify its deployment, an Infer plugin has been created for the csmock tool, which allows static analysers to run automatically on packages for CentOS or Fedora. To reduce the number of false reports, a filter has been created, which filters Infer's output according to several proposed heuristics based on experience obtained by analysing the reports produced by Infer. The filter has been also included into the csmock plugin and tested on a number of packages. On the analysed packages, the filter was able to remove 60 % of false reports with a loss of 2.5 % of real defects. The time required to run the analysis can be reduced by using incremental analysis. Shortcomings of the incremental analysis provided implicitly by Infer were experimentally found, so this thesis also describes the creation of a wrapper for Infer, which replaces the incremental analysis in Infer.
|
|
|
Static Analysis for Discovering Security Vulnerabilities in Web Applications on the Asp.Net Platform
Říha, Jakub ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
This Bachelor thesis is intended to describe theoretical foundations as well as the construction of a static taint analyser based on the .NET Framework and the analysis services provided by the .NET Compiler Platform. This analyser detects SQL injection security vulnerabilities on the ASP.NET MVC platform. Firstly, the analyser constructs control flow graphs as an abstract representation of the analysed program. Then, it uses a static taint analysis to track potentially distrusted and tainted data values. Finally, analysis results are presented to the user.
|
host ::
RSS.