|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an improved unwinding mechanism for the 2LS formal verification tool. 2LS is a static analysis framework for C programs based on reasoning about programs using an SMT solver. It combines multiple common verification techniques into an algorithm called k I k I. One of the crucial parts of the algorithm is loop unwinding. Unfortunately, the existing solution does not correctly support unwinding of loops containing operations with dynamically allocated memory. Our proposed solution is based on unwinding loops in a GOTO program rather than the SSA form, making it possible to correctly handle dynamic objects and operations over them. The proposed solution has been implemented in the 2LS framework and our experiments on a set of benchmarks from the International Competition on Software Verification (SV-COMP) show that it improves soundness of analysis of programs working with dynamic objects.
|
|
|
Improving Precision of Program Analysis in the 2LS Framework
Smutný, Martin ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose a way to improve precision of program analysis in the 2LS framework, based on its existing concepts, mainly template-based synthesis of invariants. 2LS is a static analysis framework for analysing C programs which relies on the use of an SMT solver and of abstract interpretation for automatic invariant inference. In a case when 2LS can not decide whether a program is correct, the proposed solution analyses the invariants computed in various abstract domains and identifies parts of the invariants that potentially cause undecidability of the verification. Using the obtained information, the designed method is able to identify variables of the original program that possibly determine whether the verification is successful. The output of our solution can be used as a feedback to indicate variables with problematic values that should be constrained. Also, it can be utilized by the 2LS developers for debugging purposes during development of new analyses. The solution has been implemented in the 2LS framework. Testing our solution on various benchmarks from the International Competition on Software Verification (SV-COMP) shows that it can identify variables that cause undecidability of the verification in more than half of the programs where the verification currently fails.
|
|
|
Static Analysis Using Facebook Infer Focused on Errors in RCU-Based Synchronisation
Marek, Daniel ; Malík, Viktor (oponent) ; Vojnar, Tomáš (vedoucí práce)
Read Copy Update (RCU) is a synchronization mechanism, found mostly in the Linux kernel. Its sought-after features include almost zero overhead and high speed when reading shared memory. RCU has a set of rules of use, which need to be followed in order for the synchronization to work properly. To the best of our knowledge, there is no analyzer that sufficiently verifies if the RCU rules of use are adhered to. To overcome this, we propose a new analyzer, with the focus on finding violations in the use of RCU rules. The analyzer is based on static analysis and implemented as a module for the static analysis framework Facebook/Meta Infer. This platform was chosen because it provides scalability, which is needed when dealing with such an extensive software as the Linux kernel. The designed analyzer is capable of detecting multiple different ways in which the RCU usage rules can be broken, each causing either a race condition or a deadlock. It is also capable of generating warnings for situations when a deprecated function call is used or when the use of incompatible RCU reader and writer primitives is detected. The analyzer is the first of its kind. It may become a basis for future analyzer development in the field of Read Copy Update. Furthermore, it may be used as a test tool in the Linux kernel development cycle.
|
|
|
Real Time Data Processing with Strimzi Project
Orsák, Maroš ; Malík, Viktor (oponent) ; Rogalewicz, Adam (vedoucí práce)
Container technologies become broadly used in modern times. In prevailing, applications made on the micro-service architecture are rising. This thesis analyzes the design of an application that will process data in real-time. Further, the application will be built using state-of-the-art technologies used by world companies like Netflix, Uber. They are using the systems for real-time data processing such as Apache Kafka, and in recent times they raised it on a higher level by encapsulating this system in the container environment, which guaranteeing effortless scalability. Additionally, using the latest native Kubernetes technologies for processing dozens of data with Quarkus and Strimzi. The problem, which arises, is that these types of real-time data processing systems encapsulated in the containers are especially challenging to test. The main goal of this thesis is a proof-of-concept application based on Strimzi project and also show the designed long term test of the application also known as Marathon, which is the ideal demonstration of user conditions.
|
|
|
Webový prohlížeč reportů analýzy zdrojových kódů
Dolejší, Jakub ; Malík, Viktor (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato bakalářská práce se zabývá návrhem a vývojem webové aplikace RepView. Tento nástroj slouží k interaktivní revizi zdrojových kódů na základě příslušného reportu analýzy zdrojových kódů. Aplikace se skládá ze dvou oddělených služeb, které běží v separátních kontejnerech technologie Docker. Cílem aplikace je usnadnit interpretaci reportu a jeho vazbu na zdrojové kódy. Výsledku je dosaženo za použití moderních webových technologií (Vuejs, Quasar), které umožňují provést uživatelsky přívětivou revizi zdrojových kódů.
|
|
|
Fuzz Testing of REST API
Segedy, Patrik ; Rogalewicz, Adam (oponent) ; Malík, Viktor (vedoucí práce)
This thesis is dealing with fuzz testing of REST API. After presenting state-of-the-art of fuzzing and assessing the current research regarding REST API fuzz testing, we design and implement our REST API fuzzer. The proposed fuzzer infers dependencies of API calls defined in an OpenAPI specification and makes the fuzzing stateful. One of the features is minimization of the number of successive 404 responses while maintaining exploration of a deeper state space of a tested application. To solve the exploration vs. exploitation problem, we used the ordering of dependencies maximizing the probability of obtaining a needed input values and determining of fuzzability of a required parameters. The implementation is an enhancement of the Schemathesis project that is using the Hypothesis library to randomly generate inputs. Our fuzzer is evaluated against the Red Hat Insights application, finding 32 bugs. Amid them, one bug is reproducible only by a stateful set of steps.
|
|
|
Generování testovacích vstupů podle stopy programu
Sušovský, Tomáš ; Malík, Viktor (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem a implementací nástroje pro automatické generování testových vstupů na základě určené stopy programu. Cílem je zjednodušit a zefektivnit proces vytváření testových sad splňující pokročilá kritéria pokrytí (používaných v kritických aplikacích psaných v nízko úrovňových jazycích C/C++ splňující přísná omezení). Na základě modelu programu nástroj zkoumá, jaké přesné podmínky musí nastat pro průchod programu dle zadané stopy. Pro nalezení vhodných hodnot využívá existující pokročilý nástroj řešič SMT specializovaný na řešení problému splnitelnosti. Nástroj využívá knihovny překladačového rámce LLVM pro práci s modelem programu a knihovnu Z3 pro práci s řešičem SMT. Výsledkem této práce je návrh architektury nástroje pro generování testových vstupů, který dokáže vygenerovat vstupy pro vykonání zadané stopy programu díky analýzování modelu programu, a implementace jeho prototypu.
|
|
|
Dynamická analýza použití knihovních volání
Malík, Viktor ; Peringer, Petr (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato bakalářská práce se zabývá vývojem dynamického analyzátoru, který sleduje používání knihovních volání analyzovaným programem. Analyzátor dále tato volání automaticky ovládá za účelem vytváření různých běhů programu, které pak agreguje do výsledného grafu toku řízení. Pro sledovaní a ovládání volání používá analyzátor vlastní sdílenou knihovnu pro operační systém GNU/Linux. Součástí práce je jak podrobný návrh celé aplikace, tak i její implementace v~jazycích C/C++ zaměřující se na sledování standardních knihovních volání nad souborovým systémem.
|
|
|
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.
|
|
|
Performance Testing of Linux Kernel Scheduler
Vozár, Jiří ; Rogalewicz, Adam (oponent) ; Malík, Viktor (vedoucí práce)
Performance of process scheduler in a kernel of an operating system significantly influences throughput and latency of all applications running above it. Any performance drop can have critical consequences on the applications. With the arrival of every new technology (e.g. symetric multiprocesing) the code of the scheduler evolves and grows. This requires not only functional, but also performance regression testing. This work presents methods of performance testing used in the Red Hat, Inc. company. It describes how one can measure performance of the Linux process scheduler in the Linux kernel, collect statistics about its behavior, store the collected data, and visualize them. The goal of this work is to design and implement a new technique of visualization of long-term measurements and utilization of machine learning for automatic classification of performance degradation between different results.
|
host ::
RSS.