|
|
Applying formal methods to analysis of semantic differences between versions of software
Nečas, František ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout integraci formálních metod pro DiffKemp, nástroj pro statickou analýzu sémantických rozdílů v rozsáhlých programech napsaných v jazyce C. Cílem tohoto rozšíření je umožnit analýzu složitějších změn, které by typicky byly analyzovatelné spíše nástroji založenými na formálních metodách, a zároveň zachovat škálovatelnost nástroje DiffKemp na velké projekty. Principem navrženého řešení je při analýze v případě nalezení možné sémantické změny zakódovat problém ekvivalence příslušných instrukcí jako instanci problému SMT. Tím je možné sémantický rozdíl potvrdit, nebo vyvrátit s pomocí SMT solveru. Navržené řešení bylo implementováno v nástroji DiffKemp a experimenty provedené na sadě programů zvané EqBench ukazují, že rozšiřuje schopnosti nástroje DiffKemp, převážně v oblasti přesné analýzy úprav aritmetických výrazů.
|
|
|
Automatic Searching of Instruction Extensions for Application Processors
Češka, Martin ; Křoustek, Jakub (referee) ; Masařík, Karel (advisor)
This thesis deals with the process of automatic searching of instruction-set extensions for application-specific instruction-set processors. This process uses slightly edited ISEGEN algorithm. At first, all important terms including this algorithm are described. Then there is a detailed description of implementation of whole process in C++ programming language. At last, newly created program is considered as useful or useless based on speed-up of processor at performing of input program using found extensions.
|
|
|
Program Instrumentation Enabling Coverage Measurement in SW Testing
Kapoun, Petr ; Peringer, Petr (referee) ; Smrčka, Aleš (advisor)
This work deals with the design and creation of an instrumentation tool for measuring coverage in software testing. During compilation, the tool obtains a representation of selected parts of the program in the form of a control flow graph and instruments the given parts of the program by inserting function callbacks. Using the data generated when calling the function callbacks of the instrumented program, the tool evaluates the measurement of the coverage criteria. Supported coverage criteria include line coverage and selected control flow and data flow coverage criteria.
|
|
|
Automatic Forward Slicing of Programs
Patrik, Nikolas ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Táto práca popisuje návrh a implementáciu nového riešenie pre nástroj DiffKemp na automatické dopredné prerezávanie programov. Po zdĺhavej analýze súčasného riešenia, sme sa rozhodli súčasné riešenie ponechať a rozšíriť ho o zopár vylepšení. Implementovali sme rozšírenie ktoré dovoľuje DiffKempu vykonávať analýzu nad prvkami štrukturovaných typov, pridali sme k súčasnému prerezávaciemu kritériu aj hodnotu premennej a na záver pridali podporu na analýzu parametrov modulov jadra. Po implementovaní týchto vylepšení sme vykonali experimenty ktoré potvrdili zlepšenie analýzi ktorú DiffKemp vykonával.
|
|
|
Software Execution Acceleration Using Automatic Instruction Set Extensions
Melo, Stanislav ; Dolíhal, Luděk (referee) ; Masařík, Karel (advisor)
One of the important feature of application specific processors is performance. To maximize it, the processor must adapt to needs of application that it is going to perform. One of the ways to do that is to search for appropriate instructions that can be joined into one special instruction. This instruction is then implemented in hardware as a single function block. This bachelor's thesis describes problem of finding and selecting suitable candidates for instruction-set extension. It also provides brief overview of the few best known algorithms that solve this problem. Moreover the thesis deals with the single-cut algorithm and its implementation in more detail.
|
|
|
Instrumentation of C/C++ Programs during Compilation
Mušková, Kateřina ; Peringer, Petr (referee) ; Smrčka, Aleš (advisor)
This thesis presents design and implementation of the TforcTool offering compile-time instrumentation of memory access and functions. The tool is built on an existing static instrumenting tool Tforc, which was extended in order to provide greater usability and functionality. The advantage of this solution compared to another compile-time tools is that there is no need to change current compile structure of project.
|
|
|
Static Behavioral Malware Detection over LLVM IR
Surovič, Marek ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá metodami pro behaviorální detekci malware, které využívají techniky formální analýzy a verifikace. Základem je odvozování stromových automatů z grafů závislostí systémových volání, které jsou získány pomocí statické analýzy LLVM IR. V rámci práce je implementován prototyp detektoru, který využívá překladačovou infrastrukturu LLVM. Pro experimentální ověření detektoru je použit překladač jazyka C/C++, který je schopen generovat mutace malware za pomoci obfuskujících transformací. Výsledky předběžných experimentů a případná budoucí rozšíření detektoru jsou diskutovány v závěru práce.
|
|
|
Extraction of Control Flow Graph from Java Bytecode
Sečkařová, Petra ; Kočí, Radek (referee) ; Smrčka, Aleš (advisor)
The most of the analyses evaluating the quality of code are derived from Control Flow Graphs -- CFG. Model-based testing as one of them uses paths found in CFG for generation of test cases. To ease use of a general analysis of CFG, there is a need for CFG to contain instructions of some general instruction set. This work deals with extraction of control flow graphs from Java bytecode, followed by a translation of the instructions inside basic blocks into LLVM IR set. The resulting program is able to reliably extract control flow graphs from a Java program, given in any of its casual forms (.jar archive, .java or .class file). In addition to that, the graphs on output are assembled so, that they can be analyzed in order to generate unit tests.
|
|
|
Semi-Automatic Optimization Using Specialized Instructions
Mikó, Albert ; Hynek, Jiří (referee) ; Masařík, Karel (advisor)
The design of instruction sets for application specific processors is a difficult task. This thesis describes the tasks of selection, marking and creation of instruction set extensions for application specific processors. The presented semiautomatic method provides the user with a simple way to select instruction set extensions by marking a section of source code in the application. The creation of the new instruction in the modelling language itself is solved automatically. Thanks to this the user can concentrate his efforts on tasks where human ingenuity and experience can be used the most.
|
|
|
Decompilation of x86-64 Binaries in RetDec Decompiler
Kubov, Peter ; Křivka, Zbyněk (referee) ; Kolář, Dušan (advisor)
The goal of this thesis is to implement support for decompilation of x64 binary files in the RetDec decompiler. The thesis analyses different approaches to reverse engineering, mainly from the view of information technology. After a general classification of decompilers, thesis brings to attention one particular decompiler from Avast company-RetDec. The thesis also deals with the description of broadly used architecture x86, and it's descendant architecture x86-64. In result, the thesis provides new and extends existing classes in C++ to provide missing functionality.
|
guest ::
