|
|
Practical Application of Facebook Infer on Systems Code
Beránek, Tomáš ; Malík, Viktor (oponent) ; Vojnar, Tomáš (vedoucí práce)
Static analysis is nowadays often used in the development process to find defects in the produced software. Although static analysis tools can effectively find bugs in software with millions of lines of code, they have also some disadvantages. The main disadvantages are the difficulty to deploy the chosen tool on the given project, high numbers of false reports, and the time and space requirements. This thesis focuses on mitigating these negative features of the Facebook Infer tool mainly for the context of using it to analyse Linux utilities shipped as SRPM packages. To simplify its deployment, an Infer plugin has been created for the csmock tool, which allows static analysers to run automatically on packages for CentOS or Fedora. To reduce the number of false reports, a filter has been created, which filters Infer's output according to several proposed heuristics based on experience obtained by analysing the reports produced by Infer. The filter has been also included into the csmock plugin and tested on a number of packages. On the analysed packages, the filter was able to remove 60 % of false reports with a loss of 2.5 % of real defects. The time required to run the analysis can be reduced by using incremental analysis. Shortcomings of the incremental analysis provided implicitly by Infer were experimentally found, so this thesis also describes the creation of a wrapper for Infer, which replaces the incremental analysis in Infer.
|
|
|
Equivalence-Based Slicing of Programs
Malecová, Tatiana ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The aim of this work is to design a method that simplifies two programs based on the results of analysis of their semantic difference. The goal is to remove as many semantically equivalent parts of the programs as possible. To find these equivalent parts, we apply our own solution to the problem of finding the maximum common induced subgraph. Subsequently, we are able to simplify the programs by using backward static slicing. By applying this simplification, we obtain sliced programs that consist of the differing parts and parts that can affect these differences. The method has been implemented as an extension of the DiffKemp tool, which is a static analyser of semantic differences between different versions of large scale programs. Our experiments on the Linux kernel show that the method is able to produce correct slices very efficiently (the analysis is prolonged only by 3.2%). Moreover, the created slices are much smaller than the original programs, which makes them suitable for further analysis.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (oponent) ; Radu, Iosif (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis focuses on improving the state of the art of automata-based formal analysis and verification techniques for systems with an infinite state space. In the first part of the thesis, we develop two efficient decision procedures for the WS1S logic, both of them exploiting the correspondence between formulae of WS1S logic and finite automata. We start by proposing a novel antichain-based decision procedure which is, however, limited to formulae in the prenex normal form. Later, we generalize the approach to arbitrary formulae by defining the so-called language terms and constructing an on-the-fly procedure dealing with the terms using lazy techniques. In order to achieve an efficient implementation, we propose numerous optimizations (some of these optimization are not limited to our approaches only). We evaluated both our methods with other recent state-of-the art tools. The achieved results are encouraging and show we can extend the usage of WS1S to wider classes of formulae. The second part of the thesis focuses on resource bounds analysis of heap-manipulating programs. We propose a new class of shape norms based on lengths of paths between distinct points in the heap, which we derive automatically from the analysed program. For this class of norms, we introduce a calculus capable of precisely inferring changes of the analysed norms and use it to generate a corresponding integer representation of an input program followed by dedicated state-of-the art resource bounds analysis. We implemented our approach over the shape analysis based on forest-automata, implemented in the Forester tool, and using a well-established resource bounds analyser, implemented in the Loopus tool. In our experimental evaluation, we show that we indeed obtained a powerful analyser that is able to handle some showcase examples that were never analysed fully automatically before.
|
|
|
Application of Genetic Algorithms and Data Mining in Noise-based Testing of Concurrent Software
Šimková, Hana ; Kofroň, Jan (oponent) ; Lourenco, Joao (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis proposes an improvement of the efficiency of testing concurrent software by employing data mining techniques and genetic algorithms in the process of testing concurrent software. Concurrent, or multi-threaded, programming has become very popular over the last few years. However, as the concurrent programming is far more demanding the sequential programming, its increased use leads to a significant increase in the number of errors that appear in commercial software due to errors in synchronization. Finding such errors using traditional testing methods is difficult. Moreover, repeated test executions of traditional testing that are performed in the same environment will typically examine similar interleavings only. Hence, the noise-based injection approach is used for influencing the scheduling by injecting various kinds of noise (delays, context switches, and so on) into the common thread behaviour which stress the software and can to show some rare behaviour. However, for the noise injection to be efficient, one has to choose suitable noise injection heuristics from among the many existing ones as well as to suitably choose values of their various parameters, which is not easy. In this work, there are used data mining methods and genetic algorithms and their combinations to deal with the problem of choosing such noise injection heuristics and values of their parameters. Besides setting up of the goals of the thesis, this proposal also provides a brief summary of the state of the art in application of data mining techniques and genetic algorithms to program testing problems.
|
|
|
Symbolic Automata for Analysing String Manipulating Programs
Kotoun, Michal ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Many software applications receive, send and process data in a text form. Correct and safe processing of these data is usually ensured by so-called string sanitization. With the help of methods of formal verification, we can analyse these string operations and check whether they are correctly designed and implemented. The goal of this work is to create a tool for analysis of systems whose configurations can be encoded as words over a suitable alphabet, as well as its specialization for analysing string manipulating programs. First, we describe finite automata and transducers in general and characterize various classes and sub-classes of symbolic transducers, especially their limitations. Based on this study, a new class of symbolic transducers is proposed for use in the program analysis. Later, we introduce regular model checking, especially its variant based on abstraction over automata, the so called ARMC, which was proved to be able to quite successfully fight the state explosion problem in the size of the automata and allows us to reach a fix-point. We then design an analysis of programs written in imperative languages, especially those that manipulate strings, using the principles of ARMC. Finally, the implementation of the tool is presented, highlighting its practical aspects and discussing relevant parts of AutomataDotNet library it is based on. The work completes debating the experimental evaluation of the tool using test inputs from LibStranger project.
|
|
|
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.
|
|
|
Automated Generation of Tests for GNOME GUI Applications Using AT-SPI Metadata
Krajňák, Martin ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
The goal of this work is the development of a tool capable of automatic test generation for GUI applications in the GNOME desktop environment. The tests are generated using metadata provided by the assistive technologies, specifically the AT-SPI. The proposed test generator utilizes the given metadata to create a model of a tested application. The model maps the event sequences that are applied on the tested application during the test generation process. The generation process involves the detection of severe bugs in the tested application. The results of the test generation process are automated test cases suitable for regression testing. The functionality of the implemented test generator was successfully verified by testing 5 open-source applications. The testing of applications performed by the proposed tool has proven the ability to reveal new bugs.
|
|
|
Detection of Timing Side-Channels in TLS
Koscielniak, Jan ; Malík, Viktor (oponent) ; Vojnar, Tomáš (vedoucí práce)
The TLS protocol is complex and widely used, which necessitates thorough testing, as there are many devices relying on it for secure communication. This thesis focuses on timing side-channel vulnerabilities, which seem to come back every few years in different variations of the same attacks. It aims to help correctly fix those vulnerabilities and prevent the creation of new ones by providing an automated side-channel testing framework that is integrated into the tlsfuzzer tool, and by expanding its test suite with test scripts for known attacks that exploit timing side-channels. The extension utilizes tcpdump for collecting the timing information and statistical tests and supporting plots to make a decision. The extension and the new test scripts were evaluated and shown to be accurate at spotting side-channels. Both the extension and the test scripts are now a part of the tlsfuzzer tool.
|
|
|
Static Analysis in the Frama-C Environment Focused on Deadlock Detection
Dacík, Tomáš ; Holík, Lukáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis presents a design of a new static analyser focused on deadlock detection, implemented as a plugin of the Frama-C platform. Together with the core algorithm of deadlock detection, we also present a light-weight method that allows one to analyse (not only for the purposes of deadlock detection) multi-threaded programs using sequential analysers of Frama-C. Results of experiments show that our tool is able to handle real-world C code with high precision. Moreover, we demonstrate its extensibility by so-far experimental implementation of data race detection.
|
|
|
Optimalizace mazání souborů v ext4 pro snadnější obnovu souborů
Uhliarik, Luboš ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
Práce se zabývá úpravou souborového systému ext4 za účelem optimalizace procesu mazání souborů pro jejich snadnější obnovu. Součástí práce je popis změn souborového systému ext4, včetně popisu nástroje, který se stará o samotnou obnovu smazaných souborů. Dále práce obsahuje popis, jak byly provedené změny v souborovém systému ext4 testovány. V této práci jsou rovněž popsány existující metody pro obnovu souborů, včetně všech jejich hlavních výhod a nevýhod.
|
host ::
RSS.