|
|
Applying formal methods to analysis of semantic differences between versions of software
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an integration of formal methods into DiffKemp, a static analysis tool for analyzing semantic differences of large-scale C projects. The aim of this extension is to facilitate analysis of more complex code changes, which would typically be better handled by a tool based on formal methods, while also maintaining DiffKemp’s scalability to large projects. To achieve this, whenever a possible semantic change is found, the equivalence of the relevant instructions is encoded into an SMT problem instance and the difference is either confirmed or refuted using an SMT solver. The proposed solution has been implemented in DiffKemp and our experiments on a set of benchmarks called EqBench show that it extends the capabilities of DiffKemp, mainly with regards to sound analysis of refactorings of arithmetic expressions.
|
|
|
Automatické vyhledávání instrukčních rozšíření aplikačních procesorů
Češka, Martin ; Křoustek, Jakub (oponent) ; Masařík, Karel (vedoucí práce)
Tato práce se zabývá procesem automatického vyhledávání instrukčních rozšíření u aplikačně-specifických procesorů. K tomuto procesu je použito mírně upraveného algoritmu ISEGEN. Nejdříve jsou popsány veškeré důležité pojmy týkající se tohoto procesu včetně vybraného algoritmu ISEGEN. Následuje podrobný popis implementace celého procesu do jazyka C++. Nakonec je výsledný program zhodnocen na základě urychlení vykonávání vstupních programů na daném aplikačním procesoru při použití vyhledaných instrukčních rozšíření.
|
|
|
Instrumentace programů pro měření pokrytí při testování SW
Kapoun, Petr ; Peringer, Petr (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem a tvorbou instrumentačního nástroje pro měření pokrytí při softwarovém testování. Nástroj při překladu získá reprezentaci vybraných částí programu v podobě grafu toku řízení a instrumentuje dané části programu vložením zpětných volání funkcí. Pomocí dat generovaných při volání vložených funkcí instrumentovaného programu nástroj vyhodnotí měření kritérií pokrytí. Mezi podporovaná kritéria pokrytí patří pokrytí řádků kódu a vybraná kritéria pokrytí toku řízení a toku dat.
|
|
|
Automatic Forward Slicing of Programs
Patrik, Nikolas ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
This thesis presents designing new forward slicing solution for the DiffKemp tool. After strenuous analysis of currently implemented solution in DiffKemp for forward slicing we decided to retain current solution and extend it by few enhancements that should improve the analysis provided by DiffKemp in a quite big scope. We have implemented extensions so DiffKemp can perform analysis on fields of structured types which might represent run-time parameters and also we extended slicing criterion with the value of analyzed variable. Also we added support for slicing module kernel parameters. After implementing this solutions, we did experiments which proved that implemented solution has improved the analysis performed by DiffKemp.
|
|
|
Zrychlení vykonávání softwaru pomocí automatických instrukčních rozšíření
Melo, Stanislav ; Dolíhal, Luděk (oponent) ; Masařík, Karel (vedoucí práce)
Jednou z důležitých vlastností aplikačně specifických procesorů je jejich výkon. Aby byl co největší, musí se procesor přizpůsobit potřebám aplikace, kterou bude vykonávat. Jedním ze způsobů přizpůsobení se je hledání vhodných instrukcí, které se následně spojí do jedné speciální instrukce. Daná instrukce je pak implementována v hardwaru jako jeden funkční blok, takže se vykoná rychleji. Tahle práce popisuje problém nalezení a vybrání vhodných kandidátů na instrukční rozšíření. Také poskytuje stručný přehled pár nejznámějších algo- ritmů na řešení tohohle problému. Dále se práce detailněji zabývá algoritmem single-cut a jeho implementací.
|
|
|
Instrumentace C/C++ programů při překladu
Mušková, Kateřina ; Peringer, Petr (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem a implementací nástroje TforcTool sloužícího k instrumentaci programů napsaných v jazyce C++, a to instrumentaci přístupu do paměti a volání funkcí. Nástroj staví už na existujícím nástroji Tforc poskytující statickou instrumentaci při překladu, jehož funkcionalitu a použitelnost rozšiřuje. Velkou výhodou oproti stávajícím řešením nabízejícím instrumentaci při překladu je možnost použití nástroje bez změny stávajících překladových skriptů (např. Make).
|
|
|
Static Behavioral Malware Detection over LLVM IR
Surovič, Marek ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
In this thesis we study methods for behavioral malware detection, which use techniques of formal verification. In particular we build on the works, which use inference of tree automata from syscall dependency graphs, obtained by static analysis of LLVM IR. We design and implement a prototype detector using the LLVM compiler framework. For experiments with the detector we use an obfuscating compiler capable of generating mutations of malware from C/C++ source code. We discuss preliminary experiments which show the capabilities of the detector and possible future extensions to the detector.
|
|
|
Extrakce grafu toku řízení z bajtkódu Java
Sečkařová, Petra ; Kočí, Radek (oponent) ; Smrčka, Aleš (vedoucí práce)
Grafy toku řízení (Control Flow Graph -- CFG) slouží jako základ pro mnoho analýz vyhodnocujících kvalitu programu. Takovou analýzou je i testování založené na modelech (model-based testing), které na základě analýzy modelu kódu, např. grafu, generuje testovací případy. Aby bylo možné tuto analýzu provádět co nejobecněji, je vhodné, aby instrukce obsažené v CFG patřily do některé z obecných instrukčních sad.Tato práce se zabývá extrakcí grafů toku řízení z bajtkódu jazyka Java a následným překladem jednotlivých instrukcí bajtkódu uvnitř základních bloků do instrukční sady LLVM IR. Výsledný program dokáže spolehlivě získat grafy toku řízení z programů v jazyce Java zadaných v jakékoli z nejběžnějších forem pro šíření tohoto typu software (.jar archiv, .java nebo .class soubory). Grafy na výstupu jsou navíc koncipovány tak, aby nad nimi bylo možné provádět analýzu za účelem generování jednotkových testů.
|
|
|
Semiautomatická optimalizace pomocí specializovaných instrukcí
Mikó, Albert ; Hynek, Jiří (oponent) ; Masařík, Karel (vedoucí práce)
Návrh instrukční sady aplikačně specifických procesorů je náročná úloha. Tato práce popisuje problematiku výběru, označení a vytvoření instrukčních rozšíření aplikačně specifických procesorů. Použitá semiautomatická metoda umožňuje uživateli snadný výběr instrukčních rozšíření pomocí označení úseku zdrojového kódu aplikace. Samotné vytvoření nové instrukce v modelovacím jazyku je řešen automaticky. Tím nechá uživatele soustředit se na činnost, při které se nejvíce uplatní vynalézavost a zkušenosti člověka.
|
|
|
Zpětný překlad aplikací pro architekturu x86-64 v nástroji RetDec
Kubov, Peter ; Křivka, Zbyněk (oponent) ; Kolář, Dušan (vedoucí práce)
Cieľom práce je implementovať podporu spätného prekladu binárnych súborov architektúry x64 pre spätný prekladač RetDec. Práca skúma prístupy reverzného inžinierstva, najmä z pohľadu informačných technológií. Zaoberá sa všobecným princípom spätných prekladačov a konkrétne prekladačom RetDec od spoločnosti Avast. Popisuje architektúru x86 a z nej odvovodenú architektúru x86-64. Výstupom práce je implementácia nových a rozšírenie existujúcich tried v jazyku C++, ktoré plnia chýbajúcu činnosť.
|
host ::
RSS.