|
|
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.
|
|
|
Analýza a oznámení o nových ResultCloud výsledcích
Iakymets, Bohdan ; Vojnar, Tomáš (oponent) ; Šimková, Hana (vedoucí práce)
Většinou výsledky testů aplikace jsou stejné a proto nenesou žádnou užitečnou informaci. Vývojáři musejí neustále probírat velké množství zbytečných informací, aby našli něco za jímavého. Tedy vývojář potřebuje nástroj pro analýzu testovacích výsledků a v případě nalezení zajimavé informace to oznámí uživateli. Tento nástroj ušetří spoustu času. Zadání této bakalářské práce je navrhnout a implementovat, mechanismus pro analýzu a oznámení uživateli o zajímavých změnách v výsledcích sady testů. Mechanismy musejí být snadno rozšiřitelné a dobře integrovatelné v ResultCloud. Součástí této práce je prostu dování ResultCloud a na základě získaných znalostí rozšíření ResultCloud o analyzátor a oznamovatele. Nástroj je implementován pomocí AngularJS a PHP.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (oponent) ; Radu, Iosif (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis focuses on improving the state of the art of automata-based formal analysis and verification techniques for systems with an infinite state space. In the first part of the thesis, we develop two efficient decision procedures for the WS1S logic, both of them exploiting the correspondence between formulae of WS1S logic and finite automata. We start by proposing a novel antichain-based decision procedure which is, however, limited to formulae in the prenex normal form. Later, we generalize the approach to arbitrary formulae by defining the so-called language terms and constructing an on-the-fly procedure dealing with the terms using lazy techniques. In order to achieve an efficient implementation, we propose numerous optimizations (some of these optimization are not limited to our approaches only). We evaluated both our methods with other recent state-of-the art tools. The achieved results are encouraging and show we can extend the usage of WS1S to wider classes of formulae. The second part of the thesis focuses on resource bounds analysis of heap-manipulating programs. We propose a new class of shape norms based on lengths of paths between distinct points in the heap, which we derive automatically from the analysed program. For this class of norms, we introduce a calculus capable of precisely inferring changes of the analysed norms and use it to generate a corresponding integer representation of an input program followed by dedicated state-of-the art resource bounds analysis. We implemented our approach over the shape analysis based on forest-automata, implemented in the Forester tool, and using a well-established resource bounds analyser, implemented in the Loopus tool. In our experimental evaluation, we show that we indeed obtained a powerful analyser that is able to handle some showcase examples that were never analysed fully automatically before.
|
host ::
RSS.