|
|
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.
|
|
|
Nástroj pro snazší zabezpečení počítačů s OS Linux
Barabas, Maroš ; Hanáček, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
Účelem práce je příblížit čtenáři nové přístupy při zjištování a odstraňování zranitelností v oblasti počítačové bezpečnosti a navrhnout nový systém na zlepšení bezpečnosti v počítačích s operačním systémem Linux. Tento systém má za úkol analyzovat vzdálené operační systémy a odhalit tím zranitelná místa, které můžou být následně odstraněné aplikováním existujících bezpečnostních standardů.
|
|
|
Static Analysis in the Frama-C Environment Focused on Deadlock Detection
Dacík, Tomáš ; Holík, Lukáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis presents a design of a new static analyser focused on deadlock detection, implemented as a plugin of the Frama-C platform. Together with the core algorithm of deadlock detection, we also present a light-weight method that allows one to analyse (not only for the purposes of deadlock detection) multi-threaded programs using sequential analysers of Frama-C. Results of experiments show that our tool is able to handle real-world C code with high precision. Moreover, we demonstrate its extensibility by so-far experimental implementation of data race detection.
|
|
|
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šší.
|
|
|
Minimization of Counting Automata
Turcel, Matej ; Vojnar, Tomáš (oponent) ; Holík, Lukáš (vedoucí práce)
This works deals with size reduction of counting automata (CA). Counting automata extend the classical finite automata with bounded counters. This allows efficient handling of e.g. regular expressions with repetition: a{5,10}. In this thesis we discusses the simulation relation in CA, which allows us to reduce their size. We rely on classical simulation in finite automata, which we non-trivially extend to CA. The key difference lies in the necessity to simulate counters as well as states. To this end, we present the novel concept of parameterized simulation relation in CA, and propose methods for computing this relation and using it to reduce the size of a CA. The proposed methods have been implemented and their efficiency experimentally evaluated.
|
host ::
RSS.