|
|
Automatická formální verifikace korektnosti programů v nástrojích SDV, Copper a podobných
Kovalič, Peter ; Šimáček, Jiří (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se věnuje verifikaci ovládačů. Používají se při tom model checkery, hlavní z nich je Static Driver Verifier. Pomocí něj se kontroluje zvolený ovládač Ext2Fsd. Patří do skupiny ovládačů souborových systémů. Kontrola probíhá podle zadaných pravidel, které nesmí ovládač porušovat. Cílem práce bylo vybraný ovládač verifikovat pomocí zvoleného nástroje. Ve výsledcích bylo dosaženo stavu, kdy se ve verifikovaném ovládači objevili všechny tři dostupné možnosti výsledku ovládač splňoval některá pravidla, některá odhalily jeho chyby a jiné nebyly aplikovatelné. Na konci této práce se nachází ještě kapitola, věnována dalšímu model checkeru, s názvem Copper, která poskytuje základní poznatky o tomto nástroji.
|
|
|
Forenzní analýza malware
Král, Benjamin ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Tato diplomová práce popisuje metody a postupy používané při forenzní analýze malware, včetně metod statické i dynamické analýzy malware. S využitím popisovaných metod je poté navrhnut nástroj určený k užívání bezpečnostními týmy CSIRT, jež vyšetřovateli bezpečnostního incidentu umožní rychle analyzovat a rozhodnout roli vzorku malware s nímž se setká při šetření bezpečnostního incidentu. Tento nástroj je v rámci práce podrobně popsán v odborném technickém návrhu založeném na specifických požadavcích bezpečnostních týmů CSIRT specifikovaných taktéž v obsahu práce. Na základě tohoto návrhu je implementován nástroj ForensIRT, jež je následně otestován analýzou vzorku malware Cridex. Konečně výsledky této analýzy jsou porovnány s výsledky ostatních srovnatelných nástrojů určených k forenzní analýze malware.
|
|
|
Vylepšení analýzy živých proměnných pomocí points-to analýzy
Raiskup, Pavel ; Rogalewicz, Adam (oponent) ; Dudka, Kamil (vedoucí práce)
Jazyky, jako je C, hojně využívají práce s ukazateli. Implemetace dynamických datových struktur vázaných ukazateli a operací nad nimi však není jednoduchá - významně zvyšuje rizika zanášení chyb do zdrojových kódů. Jedna z cest, jakými lze eliminovat množství těchto chyb, je použití statické analýzy. Tato práce se tedy zabývá vylepšením architektury Code Listner, která nabízí rozhraní pro tvorbu statických analyzátorů. Vlastností tohoto rozhraní je, že poskytuje takovému analyzátoru k rozboru potřebné informace o programu - ku příkladu databázi proměnných, graf toku řízení čí graf volání funkcí. Součástí implementace Code Listeneru je také algoritmus pro analýzu živých proměnných, umožňující odstranit, neboli zabít proměnné, které nejsou v daném místě grafu toku řízení potřeba. Původní algoritmus ale nedovedl z důvodu bezpečnosti zabít žádné proměnné, na něž byla kdekoliv ve zdrojovém kódu vzata adresa. Předpokládalo se, že taková proměnná může být zpřístupněna pomocí reference kdekoliv v programu. Cílem práce tedy bylo navrhnout a implementovat algoritmus pro points-to analýzu, která dovede vyloučit existenci některých referencí v daném kontextu programu a umožní tedy zefektivnit analýzu živých proměnných.
|
|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an improved unwinding mechanism for the 2LS formal verification tool. 2LS is a static analysis framework for C programs based on reasoning about programs using an SMT solver. It combines multiple common verification techniques into an algorithm called k I k I. One of the crucial parts of the algorithm is loop unwinding. Unfortunately, the existing solution does not correctly support unwinding of loops containing operations with dynamically allocated memory. Our proposed solution is based on unwinding loops in a GOTO program rather than the SSA form, making it possible to correctly handle dynamic objects and operations over them. The proposed solution has been implemented in the 2LS framework and our experiments on a set of benchmarks from the International Competition on Software Verification (SV-COMP) show that it improves soundness of analysis of programs working with dynamic objects.
|
|
|
Použití statické analýzy pro detekci chyb v obsluze signálů
Kozovský, Daniel ; Vojnar, Tomáš (oponent) ; Peringer, Petr (vedoucí práce)
Táto práca sa zaoberá zásuvným modulom csigsafe pre prekladač GCC. Používa statickú analýzu programov na odhalenie chýb v obsluhe signálov podla normy POSIX. Tento nástroj analyzuje zdrojové súbory v jazyku C a C++. Tento analyzátor je vytvorený pre firmu Red Hat, ktorá ho používa na testovanie sRPM balíkov určených do ich Linuxových distribúcii. Nástroj bol testovaný na vzorku 37 projektoch s volne šíriteľnými zdrojmi. Z testovania sa ukázala užitočnosť nástroja pri vyhľadávaní chýb spojených s porušením pravidiel na správnu obsluhu signálov.
|
|
|
Statická analýza krovu
Hořínek, Josef ; Vlk, Zbyněk (oponent) ; Martinásek, Josef (vedoucí práce)
Bakalářská práce se zabývá statickou analýzou dřevěného krovu. Tento krov je součástí sedlové střechy na rodinném domě. Zatížení na konstrukci je spočítáno ručně dle platných norem. Zatížení je rozděleno do celkem 11 zatěžovacích stavů. Výpočtový model konstrukce je vytvořen v programu RFEM. Výsledky vnitřních sil a deformací jsou zkontrolovány ručním výpočtem metodami pro staticky neurčité konstrukce. Tyto hodnoty jsou na závěr porovnány.
|
|
|
Statická analýza protihlukového krytu
Hándlová, Barbora ; Martinásek, Josef (oponent) ; Vlk, Zbyněk (vedoucí práce)
Předmětem bakalářské práce je statická analýza samonosného protihlukového krytu, který je umístěn nad výrobním zařízením. Kryt je sestaven z jednotlivých segmentů s ocelovou nosnou kostrou a je možné jej po částech demontovat. K vytvoření prostorového výpočtového modelu byl použit program RFEM. Cílem práce je posouzení mezních stavů únosnosti a použitelnosti vybraných prvků konstrukce. Vybrané výsledky jsou ověřeny ručním výpočtem.
|
|
|
Multifunkční centrum v Hodoníně
Zbořil, David ; Štrba, Michal (oponent) ; Šmak, Milan (vedoucí práce)
Tato diplomová práce řeší návrh a statické posouzení multifunkčního centra v Hodoníně. Konstrukce je rozdělena na tři staticky oddělené části. Přičemž dva konstrukční celky, tvořeny ocelovými rámy se spřaženými železobetonovými deskami, jsou symetrické a střední částí, tvořenou dřevěnými rámy z lepeného lamelového dřeva. Konstrukce byla řešena pomocí výpočtového 3D modelu. Model byl vytvořen v programu RFEM 5.21.01. S pomocí modelu byly vypočteny vnitřní síly a dimenze většiny prvků. Konstrukce byla posouzena v programu RFEM 5.21.01 a v MS Excel 2010. Krajní objekty mají 7 podlaží a jsou určeny pro bytové a kancelářské prostory. Maximální výška konstrukce je 27,60 m včetně atiky. Střední multifunkční sál je zastřešen pochozí zelenou střechou. Maximální výška střední části je 12,50 m. Největší půdorysné rozměry objektu jsou 49,050 m x 24,000 m.
|
|
|
Nosná železobetonová konstrukce objektu pro parkování
Malecha, Tomáš ; Šimůnek, Petr (oponent) ; Šulák, Pavel (vedoucí práce)
Tato bakalářská práce obsahuje statickou analýzu a posouzení železobetonové, monolitické konstrukce objektu pro parkování. Je zde řešena lokálně podepřená stropní deska nad prvním nadzemním podlaží. Statická analýza byl spočítán programem Scia Engineer 14 a ověřen ručním výpočtem. Dále bylo provedeno nadimenzování na mezní stav únosnosti, konkrétně na ohybový moment, protlačení a na mezní stav použitelnosti, konkrétně na omezení trhlin. K bakalářské práci byla na základě vypočtených výsledků zhotovena výkresová dokumentace s výpisem a tvarem výztuže.
|
|
|
Analýza chování koleje na účinky železničních vozidel
Kopeček, Josef ; Plášek, Otto (oponent) ; Salajka, Vlastislav (vedoucí práce)
Diplomová práce se zabývá sestavením numerických modelů klasické koleje pomocí metody konečných prvků, a to v několika variantách. Modely jsou porovnány s výsledky získanými na analytických modelech. Komplexnější modely simulují reálné chování koleje pojížděné železničním vozidlem. Účelem je vytvoření metodiky modelování železniční tratě pro praktické využití při její statické a dynamické analýze.
|
host ::
RSS.