|
|
A Tool for Easily Securing Computers with Linux
Barabas, Maroš ; Hanáček, Petr (referee) ; Vojnar, Tomáš (advisor)
The purpose of this thesis is to explain new approaches to scanning and locking vulnerabilities in computer security and to design a new system to improve security of computers running the Linux operating system. The purpose of this system is to analyze remote operating systems and detect and lock down vulnerabilities by existing security standards.
|
|
|
Static Analysis in the Frama-C Environment Focused on Deadlock Detection
Dacík, Tomáš ; Holík, Lukáš (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá návrhem nového statického analyzátoru pro detekci uváznutí, implementovaného jako plugin platformy Frama-C. Kromě samotného algoritmu pro detekci uváznutí představuje také odlehčené řešení, které umožňuje využít platformu Frama-C pro analýzu vícevláknových programů s využitím analyzátorů Frama-C podporujících pouze sekvenční programy. Výsledky experimentů ukazují, že implementovaný nástroj je schopný analyzovat reálné programy s vysokou přesností. Pro demonstraci další rozšiřitelnosti je představeno experimentální rozšíření umožňující detekovat také časově závislé chyby nad daty.
|
|
|
An Efficient Finite Tree Automata Library
Lengál, Ondřej ; Konečný, Filip (referee) ; Vojnar, Tomáš (advisor)
Numerous computer systems use dynamic control and data structures of unbounded size. These data structures have often the character of trees or they can be encoded as trees with some additional pointers. This is exploited by some currently intensively studied techniques of formal verification that represent an infinite number of states using a finite tree automaton. However, currently there is no tree automata library implementation that would provide an efficient and flexible support for such methods. Thus the aim of this Mas- ter's Thesis is to provide such a library. The present paper first describes the theoretical background of finite tree automata and regular tree languages. Then it surveys the cur- rent implementations of tree automata libraries and studies various verification techniques, outlining requirements for the library. Representation of a finite tree automaton and algo- rithms that perform standard language operations on this representation are proposed in the next part, which is followed by description of library implementation. Through a series of experiments it is shown that the library can compete with other available tree automata libraries, in certain areas being even significantly superior to them.
|
|
|
Minimization of Counting Automata
Turcel, Matej ; Vojnar, Tomáš (referee) ; Holík, Lukáš (advisor)
Táto práca sa zaoberá redukciou veľkosti tzv. čítačových automatov. Čítačové automaty rozširujú klasické konečné automaty o čítače s obmedzeným rozsahom hodnôt. Umožňujú tým efektívne spracovať napr. regulárne výrazy s opakovaním: a{5,10}. V tejto práci sa zaoberáme reláciou simulácie v čítačových automatoch, pomocou ktorej sme schopní zredukovať ich veľkosť. Opierame sa pritom o klasickú simuláciu v konečných automatoch, ktorú netriviálnym spôsobom rozširujeme na čítačové automaty. Kľúčovým rozdielom je nutnosť simulovať okrem stavov taktiež čítače. Za týmto účelom zavádzame nový koncept parametrizovanej relácie simulácie, a navrhujeme metódy výpočtu tejto relácie a redukcie veľkosti čítačových automatov pomocou nej. Navrhnuté metódy sú tiež implementované a je vyhodnotená ich efektivita.
|
|
|
Analysis and Notification of New ResultCloud Submissions
Iakymets, Bohdan ; Vojnar, Tomáš (referee) ; Šimková, Hana (advisor)
Software tests results have mostly the same values, therefore they do not contain any important or interesting information. Developers must spend a lot of time for looking for something interesting in tests results, thus developer require tool for analysis results and in case finding interesting information notify user about it. This tool can save a lot of time. Assignment of this bachelor work is design and implement mechanism for analyzing and notifing user about interesting changes in test results. Part of the work is to learn ResultCloud and based on acquired knowledge to extend ResultCloud.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (referee) ; Radu, Iosif (referee) ; Vojnar, Tomáš (advisor)
Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.
|
|
|
Statická analýza v nástroji Meta Infer zaměřená na detekci souběhu nad daty
Svobodová, Lucie ; Fiedor, Jan (referee) ; Vojnar, Tomáš (advisor)
Vícevláknové programy jsou v moderních softwarových systémech využívány ke zlepšení výkonu a zvýšení efektivity. Zajištění spolehlivosti a bezpečnosti takových programů však může být náročné kvůli zvýšenému množství chyb, které se v nich vyskytují, včetně souběhu nad daty. V této práci představujeme nový statický detektor souběhu nad daty, DarC, navržený k analýze programů napsaných v jazyce C využívajících knihovnu Pthreads. Navrhovaný nástroj byl implementován jako zásuvný modul prostředí Meta Infer, což je nástroj pro statickou analýzu programů, který klade důraz na kompoziční, inkrementální a díky tomu i vysoce škálující analýzu programů. Nový analyzátor zaznamenává množinu přístupů ke sdíleným proměnným, ke kterým v analyzovaném programu došlo, spolu s informací o množině zámků uzamknutých při jednotlivých přístupech. Množina přístupů je dále použita k identifikaci dvojic přístupů, mezi nimiž by k souběhu nad daty mohlo dojít. Nástroj byl úspěšně ověřen na sadě testovacích vícevláknových programů, stejně tak jako na několika programech běžně využívaných v praxi, čímž byl ukázán jeho potenciál pro efektivní detekci souběhu nad daty v programech napsaných v programovacím jazyce C.
|
|
|
Pokročilá statická analýza výkonnosti v nástroji Meta Infer
Pavela, Ondřej ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Statický analyzátor složitosti Looper slouží pro odvozování přesných horních mezí ceny vykonání programů. Jako teoretický základ byl využit dříve existující nástroj Loopus a jeho abstraktní programový model využívající tzv. difference constraints (nerovnosti typu + ), které umožňují přirozeným způsobem modelovat typické modifikace počítadel cyklů = + + a = + 0. Looper byl původně navržen a implementován v rámci autorovy bakalářské práce jako zásuvný modul aplikačního rámce Meta Infer. Výsledný nástroj nicméně nenaplnil očekávání při pokusech o jeho nasazení na reálné programy. Tato diplomová práce představuje návrh nové verze, která si dává za cíl odstranit hlavní limitace původního nástroje Looper, zejména díky nově podporované in- terprocedurální analýze. Dále byla implementována řada rozšíření, které cílily na zvýšení přesnosti intraprocedurální analýzy, jako např. nový abstrakční algoritmus, podpora pro složené podmínky v hlavičkách smyček a další. Kromě toho bylo také výrazně vylepšeno logování, hlášení chyb a sběr výsledků analýzy. Na závěr byla skrze skrze rozsáhlé exper- imenty demonstrována schopnost nové verze nástroje Looper analyzovat reálný kód obec- nějším, škálovatelnějším a přesnějším způsobem.
|
|
|
Automatické generování šablon změn kódu
Kříž, Daniel ; Vašíček, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Cílem této bakalářské práce je navržení metody automatického generování šablon změn kódu v jazyce LLVM IR pro DiffKemp, nástroj pro analýzu sémantických rozdílů mezi verzemi rozsáhlých programů. Dále je cílem umožnit automatické parametrizování změn mezi verzemi projektu pomocí hodnot, globálních proměnných a strukturových typů. Toho bylo dosaženo pomocí nalezení společné šablony mezi změnami a následným generováním jejích variant, které se liší v použití globálních proměnných a typů. Navržené řešení je implementováno jako rozšíření nástroje DiffKemp a naše experimentování na malých programech ukázalo, že námi navržená metoda je schopná vytvořit alespoň částečně uspokojivé výsledky.
|
|
|
Visualisation of Static Comparison of Semantic Equivalence of Different Versions of Software Written in C
Petr, Lukáš ; Fiedor, Tomáš (referee) ; Vojnar, Tomáš (advisor)
The aim of this thesis is to create a more comprehensive presentation of results of the DiffKemp tool, which is used for static analysis of semantic differences in large projects written in C. Currently, DiffKemp displays all information about the found differences in an unstructured text which is often confusing for users. To solve this problem, a new output of the DiffKemp tool was created in this thesis, which provides the results in a serialized form using the YAML format. This output is subsequently processed and displayed using a newly created results browser, implemented as a web application using the React library, the Bootstrap framework, and the react-diff-view package. In the browser, we focus on providing an additional context in the form of source codes of the analyzed functions, and on facilitation of navigation and orientation in the found differences as well as in the provided information such as the call stacks. A comparison of the newly created browser with the original solution has shown that it is easier for the user to recognize changes in the provided call stacks and that the new browser allows him to navigate faster in the results as well as between relationships of the found differences and analysed parts.
|
guest ::
