|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
The goal of this work is to propose a shape analysis suitable for the context of the 2LS analyser. 2LS is a program analysis framework for C programs which is based on automatic invariant inference using an SMT solver. The proposed solution includes a way how the shape of a program heap can be described using logical formulae over bit-vectors and how a first-order SMT solver can be used to infer loop invariants and function summaries for each function of the analysed program. Our approach is based on pointer access paths that describe the shape of the heap by expressing the reachability of heap objects from pointer-typed program variables. The information obtained from the analysis can be used to prove various properties of programs manipulating dynamic data structures, mainly linked lists. The solution has been implemented in the 2LS framework and it brought a significant improvement in terms of the capabilities of 2LS in analysing heap-manipulating programs. This is demonstrated on benchmarks taken from the well-known International Competition on Software Verification (SV-COMP) as well as other benchmarks.
|
|
|
Framework for Testing Student Projects
Dižová, Natália ; Malík, Viktor (oponent) ; Smrčka, Aleš (vedoucí práce)
This Master's Thesis is about design and implementation of a framework, whose target is to improve effectiveness and simplify student project's evaluation process. Theoretical part of this Thesis is dedicated to software testing fundamentals and used principles. It also describes Linux containerization technology. In the next part, Thesis contains analysis of requirements for student project testing in various University courses. Core of the Thesis describes design and its implementation of a system, which satisfies analyzed requirements. Last part shows how implemented system was verified and shows possible future extensions of this work.
|
|
|
Generování modelů pro testy ze zdrojových kódů
Kraut, Daniel ; Malík, Viktor (oponent) ; Smrčka, Aleš (vedoucí práce)
ílem této diplomové práce je navrhnout a implementovat nástroj pro automatické generování cest ze zdrojových kódů. V rámci práce byla nastudována problematika testování založeného na modelech a navrženo možné řešení automatického generátoru, dle kritérií pokrytí definovaných nad modelem CFG. Stěžejním bodem diplomové práce je návrh a popisuje implementaci nástroje. Nástroj podporuje množství kritérií pokrytí, které umožňují uživateli navrhovaného nástroje zaměřit se na konkrétní aspekt zkoumaného systému, který chce pokrýt testy. Navíc je nástroj přizpůsoben pro další požadavky na velikost generované testovací sady, reflektující reálné požadavky s praktickým využitím. Generátor byl implementován v jazyce C++ a webové rozhraní k němu v jazyce Python, které zároveň slouží pro integraci do platformy Testos.
|
|
|
Applying Code Change Patterns during Analysis of Program Equivalence
Šilling, Petr ; Fiedor, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this thesis is to propose a static analysis method for recognition of code change patterns describing recurrent changes between different versions of low-level code. The thesis proposes an encoding method of patterns, which uses the LLVM intermediate representation, and a pattern matching algorithm based on gradual comparison of instructions according to their control flow. The proposed analysis has been implemented as an extension of DiffKemp, a tool for analysing semantic differences between versions of large C projects. Results of experiments conducted on three pairs of past versions of the Linux kernel show that the extension is able to eliminate a substantial amount of false-positive or generally undesirable differences from the output of DiffKemp, which would otherwise require manual inspection.
|
|
|
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.
|
host ::
RSS.