|
|
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.
|
|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout vylepšený mechanismus rozbalování smyček pro analyzátor 2LS. 2LS je nástroj pro statickou analýzu C programů založený na usuzování o programech pomocí SMT solveru. Kombinuje několik běžných verifikačních technik do algoritmu zvaného k I k I. Jednou z klíčových součástí tohoto algoritmu je rozbalování smyček programu. Současné řešení bohužel neumožňuje správně rozbalovat smyčky obsahující operace s dynamicky alokovanou pamětí. Námi navrhované řešení je založeno na rozbalování smyček v GOTO programu namísto SSA formy, díky čemuž je možné správně pracovat s dynamickými objekty a operacemi s nimi. Navržené řešení bylo implementováno v nástroji 2LS a naše experimenty na sadě testů z mezinárodní soutěže ve verifikaci software (SV-COMP) ukazují, že zvyšuje korektnost analýzy programů pracujících s dynamickými objekty.
|
|
|
Static analysis of the roof
Hořínek, Josef ; Vlk, Zbyněk (referee) ; Martinásek, Josef (advisor)
The Bachelor Thesis focuses on a static analysis of a timber roof truss. This roof trust is part of the saddle roof on the family home. The load on the structure is calculated manually according to valid standards. The load is divided into a total of 11 load cases. The calculation model of the structure is created in RFEM. Results of internal forces and deformations are checked by manual calculation using methods for statically indeterminate structures. These values are compared at the end.
|
|
|
Hiding and obfuscation of malware to avoid antivirus detection
Rybár, Matej ; Dzurenda, Petr (referee) ; Casanova-Marqués, Raúl (advisor)
Počas hodnotenia bezpečnosti je pomerne nezvyčajné, aby bol niekto presvedčený, že antivírusový softvér neposkytuje úplnú bezpečnosť. Keď penetračný tester narazí na antivírusový softvér, sú chvíle, kedy musí konať rýchlo. Z týchto a iných dôvodov boli vyvinuté rôzne spôsoby obchádzania antivírusového softvéru. Niektoré z týchto prístupov obsfukácie majú za cieľ uniknúť statickej analýze úpravou a manipuláciou s formátom Portable Executable, čo je štandardizovaný formát spustiteľného súboru Windows. Niekoľko typov malvéru mení formát súboru PE, aby sa zabránilo statickej detekcii antivírusu. Táto práca sa zaoberá formátom súborov PE, detekciou malvéru a statickou detekciou obfukačných techník. Výsledkom tejto práce je scantime crypter Persesutor, ktorý zašifruje vstupný súbor a následne po spustení zašifrovaný súbor dešifruje a načítá v pamäti.
|
|
|
Implementing control flow resolution in dynamic language
Šindelář, Štěpán ; Zavoral, Filip (advisor) ; Ježek, Pavel (referee)
Dynamic programming languages allow us to write code without type information and types of variables can change during execution. Although easier to use and suitable for fast prototyping, dynamic typing can lead to error prone code and is challenging for the compilers or interpreters. Programmers often use documentation comments to provide the type information, but the correspondence of the documentation and the actual code is usually not checked by the tools. In this thesis, we focus on one of the most popular dynamic programming languages: PHP. We have developed a framework for static analysis of PHP code as a part of the Phalanger project -- the PHP to .NET compiler. The framework supports any kind of analysis, but in particular, we implemented type inference analysis with emphasis on discovery of possible type related errors and mismatches between documentation and the actual code. The implementation was evaluated on real PHP applications and discovered several real errors and documentation mismatches with a good ratio of false positives. Powered by TCPDF (www.tcpdf.org)
|
|
|
Towards Static Analysis of Languages with Dynamic Features
Hauzar, David ; Plášil, František (advisor) ; Sinz, Carsten (referee) ; Holík, Lukáš (referee)
Dynamic features of programming languages such as dynamic type system, dynamic method calls, dynamic code execution, and dynamic data structures provide the flexibility which can accelerate the development, but on the other hand they reduce the information that is checked at compile time and thus make programs more error-prone and less efficient. While the problem of lacking compile time checks can be partially addressed by techniques of static analysis, dynamic features pose major challenges for these techniques sacrificing their precision, soundness, and scalability. To tackle this problem, we propose a framework for static analysis that automatically resolves these features and thus allows defining sound and precise static analyses similarly as the analyzed program would not use these functions. To build the framework, we propose a novel heap analysis that models associative arrays and dynamic (prototype) objects. Next, we propose value analysis providing additional information necessary to resolve dynamic features. Finally, we propose a technique that automatically and generically combines value analysis and a heap analysis modeling associative arrays and prototype objects. Powered by TCPDF (www.tcpdf.org)
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Nástroj Atomer je statický analyzátor založený na myšlence, že pokud jsou některé sekvence funkcí vícevláknového programu prováděny v některých bězích pod zámky, je pravděpodobně zamýšleno, že mají být vždy provedeny atomicky. Analyzátor Atomer se tudíž snaží takové sekvence hledat a poté zjišťovat, pro které z nich může být v některých jiných bězích programu porušena atomicita. Autor této diplomové práce ve své bakalářské práci navrhl a implementoval první verzi nástroje Atomer jako zásuvný modul aplikačního rámce Facebook Infer. V této diplomové práci je navržena nová a výrazně vylepšená verze analyzátoru Atomer. Cílem vylepšení je zvýšení jak škálovatelnosti, tak přesnosti. Kromě toho byla přidána podpora pro několik původně nepodporovaných programovacích vlastností (včetně např. možnosti analyzovat programy napsané v jazycích C++ a Java nebo podpory pro reentrantní zámky nebo stráže zámků, tzv. "lock guards"). Prostřednictvím řady experimentů (včetně experimentů s reálnými programy a reálnými chybami) se ukázalo, že nová verze nástroje Atomer je skutečně mnohem obecnější, přesnější a lépe škáluje.
|
|
|
Practical Application of Facebook Infer on Systems Code
Beránek, Tomáš ; Malík, Viktor (referee) ; Vojnar, Tomáš (advisor)
Statická analýza je dnes často využívána ve vývojovém procesu pro hledání defektů v produkovaném softwaru. I když nástroje na statickou analýzu dokáží hledat defekty v softwarech o miliónech řádků kódu, mají také řadu nevýhod. Hlavními nevýhodami jsou náročnost nasazení nástroj na vyvíjený projekt, vysoký počet falešných hlášení a časové i paměťové požadavky. Tato práce se zaměřuje na zmírnění těchto negativních vlastností u nástroje Facebook Infer, zejména pro analýzu Linuxových nástrojů v podobě SRPM balíčků. Pro zjednodušení nasazení byl vytvořen modul pro nástroj csmock, který umožňuje automaticky spouštět statické analyzátory nad balíčky pro CentOS a Fedoru. Pro snížení počtu falešných hlášení byl vytvořen filtr, který filtruje výstup Inferu podle heuristik, které byly navrženy na základě zkušeností získaných kontrolou hlášení z Inferu. Filtr byl také zapojen do modulu pro csmock a otestován na řadě balíčků. Na analyzovaných balíčcích filtr dokázal odstranit 60 % falešných hlášení se ztrátou 2.5 % skutečných defektů. Doba potřebná pro běh analýzy může být zkrácena použitím inkrementální analýzy. U inkrementální analýzy Inferu byly experimentálně zjištěny nedostatky, proto se tato práce věnuje také vytvoření nástavby nad Inferem, která nahrazuje inkrementální analýzu v Inferu.
|
|
|
Equivalence-Based Slicing of Programs
Malecová, Tatiana ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cieľom tejto práce je navrhnúť metódu, ktorá zjednoduší dva porovnávané programy na základe výsledkov ich sémantickej analýzy. Cieľom je odstránenie čo najväčšieho množstva sémanticky ekvivalentných častí porovnávaných programov. Pre nájdenie týchto ekvivalentných častí aplikujeme vlastné riešenie problému nájdenia najväčšieho spoločného indukovaného podgrafu. Následne sme schopní zjednodušiť programy využitím spätného statického prerezávania. Aplikáciou tohto zjednodušenia získame prerezané programy, ktoré obsahujú rozdielne časti a časti programov, ktoré môžu tieto rozdiely ovplyvniť. Táto metóda je naimplementovaná ako rozšírenie nástroja DiffKemp, čo je statický analyzátor sémantických rozdielov medzi rôznymi verziami rozsiahlych programov. Experimenty vykonané na jadrách Linux-u ukazujú, že metóda je schopná veľmi efektívne vyprodukovať korektné prerezané programy (analýza sa predĺžila len o 3.2%). Navyše, vzniknuté prerezané programy sú omnoho menšie, ako originálne, čo ich činí vhodnými pre ďalšiu analýzu.
|
guest ::
