|
|
Analýza práce s dynamickými datovými strukturami v C programech
Šoková, Veronika ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Táto diplomová práca sa zaoberá analýzou dynamických dátových štruktúr pomocou analýzy tvaru použitej v nástroji Predator. Popisuje zvolenú abstraktnú doménu pre reprezentáciu pamäte vo forme symbolických grafov pamäte. Ďalej sa zaoberá návrhom prostredia pre vývoj statických analyzátorov nad clang/LLVM. Prínosom tejto práce je vytvorenie a otestovanie transformačných priechodov zjednodušujúcich LLVM IR medzikód. Ďalším prínosom je optimalizácia parametrov paralelnej nadstavby Predatora opakovaným spúšťaním testov z medzinárodnej súťaže SV-COMP'16, kde táto verzia nástroja Predator získala zlatú medailu v kategórii Heap Data Structures. Posledným prínosom je návrh architektúry samotného verifikačného jadra s ohľadom na SMG doménu.
|
|
|
Detection of Expressions with Undefined Behavior in C Language
Hellebrandt, Lukáš ; Vojnar, Tomáš (oponent) ; Müller, Petr (vedoucí práce)
This thesis engages in detection of undefined behavior in the C language programs. We focus on undefined behavior stemming from incorrect work with sequence points and side effects. We perform a theoretical analysis and put terms like undefined behavior or side effect in context of the paper. Furthermore, we explain dangerousness of the constructs leading to undefined behavior. We propose a method for automated detection of the mentioned kind of undefined behavior. Finally, we design and implement a tool for its automated static detection and show the principles of the tool’s function. While designing the tool, contrary to current solutions, we stress functionality even in cases like accessing the memory via a pointer or from a called function. The thesis contains examples of dangerous constructs, functions of the created tool are demonstrated on some of them.
|
|
|
Statická analýza Java programů
Vyvial, Pavel ; Hýsek, Jiří (oponent) ; Křena, Bohuslav (vedoucí práce)
Projekt SHADOWS se zabývá vývojem software, který je schopen automaticky opravovat chyby v programech. Po každé opravě je třeba zjistit, zda opravná akce úspěšně odstranila chybu a nezanesla do kódu chybu novou, mnohem závažnější. Ve své bakalářské práci se zabývám právě takovýmto dokazováním korektni opravy kódu v konkurentních systémech. Některé z chyb v konkurentních systémech mohou být opraveny automatickým přidáním synchronizace. Při takovémto opravování chyb je potřeba zkontrolovat zda v uzamykané části neexistuje instrukce monitorenter, která by mohla představovat potenciální nebezpečí uváznutí. Dokazování korektnosti opravy je prováděno za pomocí Control Flow Graph analýzy nad Java byte-kódem. Prototyp k tomuto účelu využívá statickou analýzu zastoupenou nástrojem FindBugs.
|
|
|
Analýza konstrukčních, statických a proporčních kritérií románských a předrománských rotund.
Kříž, Pavel ; Kalousek, Lubor (oponent) ; Unger,, Josef (oponent) ; Vlček, Milan (vedoucí práce)
Disertační práce svým tématem navazuje na předchozí disertace v oboru rekonstrukcí historických staveb, které byly na Ústavu pozemního stavitelství Stavební fakulty VUT v Brně, vypracovány a obhájeny. Objekty, kterými se práce zabývá, jsou předrománské a románské okrouhlé kostely, nazývané rotundy, které vznikaly od 9. do 13. století. Tyto, svým tvarem specifické kostely, se vyskytují zejména na historickém území Velké Moravy a v omezené míře i v okolních zemích. Dobou svého vzniku se řadí k nejstarším zděným stavbám, které na našem území vznikaly a některé rotundy jsou nejstarší dochované zděné stavby na území ČR. Z tohoto pohledu jsou to tedy jedny z nejcennějších stavebních památek u nás. Část těchto staveb v průběhu historie zanikla a jsou známy pouze z archeologických nálezů nebo z písemných záznamů. Některé také ještě čekají na objevení. Existující objekty prošly v mnoha případech různými stavebními úpravami. Z důvodu stáří jsou počátky historie těchto objektů zahaleny mnoha tajemstvími a to je jeden z důvodů, proč na sebe dlouhá léta přitahují pozornost mnoha badatelů zejména z oboru archeologie, historie a historie umění. Při bádání odborníků z těchto oborů vzniká celá řada otázek, které mají interdisciplinární charakter a pro jejich odvození je potřeba spolupráce řady odborníků z různých oborů a jedním z těchto oborů je i stavitelství. Disertační práce se zabývá analýzou proporčních, konstrukčních a statických souvislostí výstavby předrománských a románských rotund. Výsledky této disertační práce jsou zejména závěry proporční analýzy, ve které autor ověřil některé hypotézy uvažované odbornou veřejností v souvislosti s problematikou románských rotund. Jedná se zejména o ověření hypotézy o používání historických jednotek při navrhování rotund, dále o hypotézy uvažující nějaký proporční kánon, případně používání nějakých univerzálních poměrových proporčních pravidel pro navrhování půdorysných i vertikálních rozměrů. Proporční analýza také ověřila někter
|
|
|
Multiplatform Linux Sandbox for Analyzing IoT Malware
Uhříček, Daniel ; Burget, Radek (oponent) ; Kolář, Dušan (vedoucí práce)
Diversity of processor architectures used by IoT devices complicates IoT malware analysis. This thesis summarizes current state of static, dynamic, and network analysis and it evaluates existing open source solutions of sandboxes providing automated analysis. It proposes a design of a modular system that is easy-to-use, has available REST API, and web interface. The implementation supports five processor architectures. It was tested on current IoT malware samples.
|
|
|
Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Harmim, Dominik ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů.
|
|
|
Automatická tvorba testovacích případů z datových toků
Kraut, Daniel ; Fiedor, Tomáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá automatickou tvorbou testovacích případů na úrovni jednotkového testování, pro zdrojové texty v jazyce C. K dosažení automatizace jsou použity metody přístupu k software jako k datovým tokům proměnných. Je zde nastíněn náhled na průběh tvorby testů a funkci CSP solverů, které jsou nezbytnou částí pro rozhodnutelnost těhto problémů. Statická analýza kódu je umožněna knihovnou LibTooling v projektu překladačového front-endu Clang. Jsou uvedeny výstupy z aplikace, jimiž jsou automaticky vytvořené vstupní hodnoty pro testovací případy.
|
|
|
Návrh mostu na dálnici D48
Holuša, Adam ; Nováček, Jan (oponent) ; Zich, Miloš (vedoucí práce)
Diplomová práce se zabývá návrhem mostu na dálnici D48 na obchvatu města Frýdek – Místek. Celkové rozpětí mostu je 113 m. Byly navrženy 3 studie. Pro podrobný návrh byla vybrána varianta monolitického komorového nosníku o 3 polích. Most je betonován na pevné skruži. Do statické analýzy je zahrnut také vliv výstavby pomocí TDA. Posudek je proveden pomocí programu Scia Engineer 18.0. Konstrukce byla posuzována podle platných EC.
|
|
|
Nástroj pro statickou analýzu programů se seznamy
Kotoun, Michal ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tvorba softwarového analyzátoru je komplexní úloha -- je nutno implementovat parsování zdrojového kódu, reprezentaci instrukcí, abstrakci hodnot, uživatelské rozhraní, ... a také analýzu samu. Abychom předešli zbytečné práci vývojářů analýz, rozhodli jsme se vytvořit framework pro statickou analýzu programů. Předkládáme obecný návrh frameworku zvaného Angie s důrazem na jeho použitelnost a popisujeme prototyp frameworku, včetně modelové analýzy založené na symbolických paměťových grafech. Angie je implementován v C++ a používá nástroje z kolekce LLVM pro parsování zdrojového kódu analyzovaných programů.
|
|
| |
host ::
RSS.