|
| |
|
|
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.
|
|
|
Using optimization methods to design machine parts
Kubrický, Daniel ; Pokorný, Přemysl (referee) ; Zeizinger, Lukáš (advisor)
This bachelor thesis describes using structural optimization methods to design machine parts. In the first part of the thesis, a description of the current state of knowledge of the optimization process was made together with its theoretical background. In the second part of the thesis, a static analysis and topology optimization or Generative design was developed using the example of a bell crank in six commercial software. In the third part, the resulting models of each software were compared with each other, and the results were compared using the von Mises maximum stress criterion and the overall model deformation. Finally, this work was concluded with an evaluation of the use of the structural optimization software.
|
|
|
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.
|
|
|
Detection of Malware Communication in Network Flows
Korvas, Václav ; Matoušek, Petr (referee) ; Ryšavý, Ondřej (advisor)
This thesis deals with the issue of network communication of malicious code, methods of their analysis and especially the comparison of accuracy of different machine learning algorithms among themselves. The paper presents a comparison of the accuracy of different machine learning algorithms, both on test data and when used in real life. Accuracy, F1-score and false positive rate were used as metrics to evaluate the results. On the test data, the Random Forest and XGBoost algorithms were found to be the most accurate, achieving 99.2% accuracy with a rate of false positivity of 0.6%. In real-life experiments, approximately 9% of flows were incorrectly detected and classified as malware. When the computer was compromised, the rate of flows classified as malware increased to 18%, and several indicators of compromise were captured and confirmed the infection of the computer.
|
|
|
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.
|
|
|
Plugin for a Code Risk Analysis
Kvasnička, Jaroslav ; Lengál, Ondřej (referee) ; Havlena, Vojtěch (advisor)
Tato práce se zabývá významem analýzy a testování kódu a jeho dopadem na funkčnost a náklady programu. Pojednává o základních principech a typech testování se zaměřením na statickou analýzu. Zkoumá také platformu Eclipse a zásuvné moduly a architekturu cílového kódu. Dále jsme probrali a implementovali rozšíření statického analyzátoru MFB, který byl vyvinut společností BOC-GROUP, spolu s rozšířeními, jako je kontrola Log4j a analyzátor GDPR. Navrhli jsme a implementovali také zásuvný modul pro Eclipse, který dokáže zvýraznit výsledky analyzátoru MFB v prostředí Eclipse IDE. V závěru jsou také diskutována možná budoucí rozšíření, včetně detektorů škodlivých regulárních výrazů a prevence XSS.
|
|
|
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.
|
|
|
Translation Among Higher Programming Languages
Knapovský, Jan ; Kožár, Tomáš (referee) ; Meduna, Alexandr (advisor)
With the development of new technologies, programming languages and their devices the need arises for existing codebases to be updated and upgraded to use such devices and technologies, to preserve the maintainability and sustainability of such systems. This thesis proposes the use of automatised means to aid such efforts – a transpiler.
|
|
|
Analysis of pathological brain tissue from MRI data
Širůčková, Kateřina ; Bartušek, Karel (referee) ; Marcoň, Petr (advisor)
Due to the high resolution of soft tissue, magnetic resonance imaging plays a crucial role in the diagnosis and therapy planning in the neurosurgery field whereas it is necessary to determine which pathology in the brain tissue is involved. Glioblastoma multiforme, metastatic tumours, lymphomas, and abscesses are examined in detail from magnetic resonance images. In clinical practice, all mentioned pathologies are diagnosed through invasive methods in the form of biopsy followed by histology of the affected tissue. This work is focused on an alternative non-invasive method of tumour diagnosis. The method is based on the data analysis from defined curves (drawn into the apparent diffusion images) that lead from the tumour area through peritumoral edema, up to healthy tissue. The analysis of descending and ascending parts of the curve could lead to non-invasive diagnostics of the pathological tissue.
|
guest ::
