|
| |
|
|
Vývoj LLVM adaptéru pro infrastrukturu Code Listener
Šoková, Veronika ; Peringer, Petr (oponent) ; Dudka, Kamil (vedoucí práce)
Tato bakalářská práce se zabývá vývojem LLVM adaptéru pro infrastrukturu Code Listener, která usnadňuje tvorbu statických analyzátorů jako jsou Predator a Forester. Ty jsou vyvíjeny a využívany v rámci skupiny VeriFIT. Popisuje překladový systém LLVM, jeho interní reprezentaci kódu a frontend Clang. Součástí práce je implementace daného adaptéru. K dnešnímu dni je schopen analyzovat omezenou množinu programů jazyka C. Je schopen generovat CFG k funkcím. Některé testy pro Predator a Forester projdou. Dále je naznačen budoucí vývoj adaptéru.
|
|
|
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.
|
|
|
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.
|
|
|
Nástroj pro analýzu skriptů unixového shellu
Holomek, Jiří ; Janoušek, Vladimír (oponent) ; Smrčka, Aleš (vedoucí práce)
Bakalářská práce se zabývá analýzou skriptů. V dnešních distribucích Linuxu nebo jiných operačních systémů založených na myšlence Unixu je mnoho nastavení konfigurováno pomocí skriptů. Práce směřuje k vytvoření programu, který takové skripty analyzuje a sdělí uživateli jejich funkci a také bezpečnost. Na základě průzkumu se práce zaměřuje na jazyk Bash.
|
|
|
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.
|
|
|
Optimalizace přední části zpětného překladače
Odaloš, Matej ; Ďurfina, Lukáš (oponent) ; Křoustek, Jakub (vedoucí práce)
Zpětný překladač je nástroj reverzního inženýrství umožňující rekonstrukci strojového kódu na některý z vyšších programovacích jazyků. Tato práce se zaobírá popisem tohoto nástroje, přičemž se soustředí hlavně na zpětný překladač projektu Lissom. Je tu navrhnutých několik technik pro optimalizaci překladu jako statická interpretace LLVM IR kódu a paměť pro výsledky interpretace. Další optimalizace se týkají rozšíření funkcionality přední části překladače, podporu delay slotů a detekci rozložení paměti a endianity. Implementované techniky jsou nakonec demonstrované na generovaném kódu.
|
|
|
Standardy a kódování zdrojového kódu PHP
Pospíšilík, Oldřich ; Kužela, Alois (oponent) ; Marušinec, Jaromír (vedoucí práce)
Tento diplomový projekt pojednává o metodice psaní zdrojových kódu a jejich vlivu na efektivitu programování. Dále potom možností odhalování metodických chyb ve zdrojovém kódu PHP. Konkrétně je rozebrána možnost integrace nástroje pro statickou analýzu v rámci vybraného vývojového týmu. Jako vývojový tým byl konzultantem Ing. Michalem Juroszem zvolen programátorský tým, který má na starosti vývoj a rozšiřování internetového informačního systému VUT v Brně. V této prácí jsou uvedeny nejzajímavější současné nástroje pro statickou analýzu jazyka PHP. Po zhodnocení a následném výběru nástroje a dalšího postupu je vypracována analýza a neformální specifikace nástroje. Následuje podrobný návrh, popis implementace a integrace.. V závěru najdeme zhodnocení celé této práce, přínos pro programátorský tým a pokračování vývoje nástroje.
|
|
|
Statická detekce častých chyb JBoss aplikačního serveru
Vyvial, Pavel ; Rogalewicz, Adam (oponent) ; Letko, Zdeněk (vedoucí práce)
Práce si klade za úkol poskytnout čtenáři popis statické analýzy prováděné prostřednictvím nástroje FindBugs nad aplikačním serverem JBoss od společnosti Red Hat. Na základě analýzy vybraných chyb byly vytvořeny vzory pro jejich detekci, které byly následně naimplementovány jako zásuvné moduly statického analyzátoru FindBugs (tzv. detektory). Vytvořené detektory byly otestovány na vývojové verzi JBoss aplikačního serveru a výsledky jsou publikovány v závěru práce.
|
|
|
Vytvoření Sparse adaptéru pro infrastrukturu Code Listener
Pokorný, Jan ; Peringer, Petr (oponent) ; Dudka, Kamil (vedoucí práce)
Kontrola programu na výskyt chyb má nezpochybnitelný význam, obzvlášť ta založená na formálních metodách. VeriFIT na FIT VUT k tomu používá vlastní infrastrukturu Code Listener (CL) modulárně propojující tzv. přední stranu, typicky adaptér převádějící kód zprostředkovaný jiným způsobem (jiným tzv. parserem), a zadní stranu typicky tvořenou koncovým analyzátorem. Cílem práce je poskytnout to prvé jako kompaktní alternativu k existujícímu zásuvnému modulu pro překladač GCC. Náš adaptér používá linearizovaný kód, jak jej zprostředkuje knihovna sparse pro statickou analýzu programů v C. Experimenty s jedním z hlavních analyzátorů v rámci CL, nástrojem Predator , a příslušnou sadou testů, dosahuje náš produkt - program clsp - úspěšnosti zhruba v 75% případů oproti onomu modulu pro GCC. Další zlepšení jsou předmětem budoucího vývoje.
|
host ::
RSS.