|
| |
|
|
Development of an LLVM Adapter for the Code Listener Infrastructure
Šoková, Veronika ; Peringer, Petr (referee) ; Dudka, Kamil (advisor)
This Bachelor's thesis deals with the development of an LLVM adapter for the Code Listener Infrastructure, which simplifies the creation of static analyzers such as the Predator and the Forester. They are developed and used within the group VeriFIT. It describes LLVM compiler system, the internal representation of the code and frontend Clang. Part of this work is the implementation of the adapter. Up to this date, it is able to analyze a limited set of programs in C. It is able to generate CFGs. Some tests for Predator and Forester pass. It is also hinted at future developments.
|
|
|
Detection of Expressions with Undefined Behavior in C Language
Hellebrandt, Lukáš ; Vojnar, Tomáš (referee) ; Müller, Petr (advisor)
Práce se zabývá detekcí nedefinovaného chování v programech v jazyce C. Zaměřujemese na nedefinované chování vznikající nesprávnou prací se sekvenčními body a vedlejšími efekty. Provedeme teoretický rozbor a pojmy jako nedefinované chování nebo vedlejší efekt zasadíme do kontextu práce. Dále vysvětlíme nebezpečnost konstrukcí vedoucích k nedefinovanému chování. Navrhneme metodu pro automatickou detekci zmíněného druhu nedefinovaného chování. Nakonec navrhneme a implementujeme nástroj pro jeho automatizovanou statickou detekci a popíšeme principy funkce tohoto nástroje. Při jeho návrhu klademe, narozdíl od současných řešení, důraz na funkčnost i v případě přístupu k paměti přes ukazatel nebo z volané funkce. Práce obsahuje příklady nebezpečných konstrukcí, na některých z nich jsou demonstrovány funkce vytvořeného nástroje.
|
|
|
Automated Formal Verification of Program Correctness Using SDV, Copper, or Similar Tools
Kovalič, Peter ; Šimáček, Jiří (referee) ; Vojnar, Tomáš (advisor)
This thesis is concerning about verification of drivers. Principally is focused on model checking tools, from which the Static Driver Verifier is the most important. A driver Ext2Fsd is checked by this program. This driver belongs to group of file system drivers. Control is driven by entered rules, which the driver must not violate. The aim of this thesis was to verify chosen driver by selected tool. The results have covered all three types of verification´s end. There were rules that driver passed, that driver violated and also that driver didn´t accept. The final chapter of work is about another model checking tool Copper. It offers the basic knowledge about this program.
|
|
|
A Tool for Shell-Script Analysis
Holomek, Jiří ; Janoušek, Vladimír (referee) ; Smrčka, Aleš (advisor)
This bachelor's thesis deals with analysis of scripts. In the current distributions of Linux or other operating systems based on the Unix principals, there is made a lot of configuration by using scripts. The main objective of this work is to create a program that analyses the scripts and also reports theirs functionality and safety to a user. According to my research the work is aimed to Bash language.
|
|
|
Static Analysis of Java Programs
Vyvial, Pavel ; Hýsek, Jiří (referee) ; Křena, Bohuslav (advisor)
The project SHADOWS has started research which is developing software for automatic bug healing. We work with self-healing software, which looks for concurrent bugs. If the~detection software finds a bug, the healing action will be performed. After every healing action, one would like to know whether this action has fixed the detected problem and, perhaps even more importantly, that it has not caused any other, possibly even more serious, problem. Therefore this paper describes a technique which gives the answer for this question after automatical healing. One can fix some concurent bugs by adding healing locks. One does healing assurance by searching monitorenter instruction and uses Control Flow Graph analysis over Java byte-code. The prototype uses static analysis (tool FindBugs) for this purpose.
|
|
|
Decompiler Front-End Optimizations
Odaloš, Matej ; Ďurfina, Lukáš (referee) ; Křoustek, Jakub (advisor)
Decompiler is a reverse engineering tool for translation of binary codes into one of the higher level languages. This bachelor thesis describes such a tool paying special attention on decompiler of the Lissom project. There are proposed several techniques for translation optimalization like static LLVM IR code interpretation and memory for its results. Other optimalizations are conserning addition of platform dependent features like delay slot support or memory datalayout and endianness detection. Finally implemented techniques are demostrated on several examples.
|
|
|
PHP Coding Standards
Pospíšilík, Oldřich ; Kužela, Alois (referee) ; Marušinec, Jaromír (advisor)
This master's thesis deals with the methodology of writing the source code and their impact on the effectiveness of programming. Furthermore, the possibility of error detection patterns in the source code of PHP. Specifically, it addressed the possibility of integration tools for static analysis of the working group. The working group was elected by supervisor Ing. Michael Jurosz, which is in charge of the development and expansion of the Internet Information System Technical University of Brno. The works are given the best tools for static analysis of the PHP language. After evaluation and subsequent selection of tools and the procedure is further analysis and informal specifications tools. The following is a detailed proposal, a description of the implementation and integration .. In conclusion, we find an assessment of the whole of this work, added value for working team and the continuation of development tool.
|
|
| |
|
|
Creation of Sparse Adapter for the Code Listener Infrastructure
Pokorný, Jan ; Peringer, Petr (referee) ; Dudka, Kamil (advisor)
Program checking is indisputably important, especially if originating in formal methods. VeriFIT at FIT BUT uses custom Code Listener (CL) infrastructure modularly interconnecting the front-end, typically a code parser adapter, and the back-end, typically an analyser. Our aim is to offer a former as a compact alternative to existing GCC compiler plug-in. This adapter uses linearized code mediated by sparse library for static analysis of programs in C. According to the experiments with one of the main CL analysers, Predator tool and its tests suite, our product - clsp program - is successful successful in roughly 75% of cases in comparison with the GCC plug-in. Further improvements are expected.
|
guest ::
