|
|
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.
|
|
|
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.
|
|
|
System for Automatic Filtering of Tests
Lysoněk, Milan ; Smrčka, Aleš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this thesis is to create a system that automatically determines a set of tests that must be run when a change is done in the ComplianceAsCode project. The proposed method selects a set of tests based on static analysis of the changed sources, taking into account the internal structure of ComplianceAsCode. The created system is divided into four parts - obtaining changes from the versioning system, static analysis of different types of files, computing the set of files affected by the change, and computing the set of tests that must be run to test the given change. We implemented analysis of several types of files and our system is designed to be easily extended by other analyses for other file types. The created implementation is deployed on the server where it automatically analyzes new contributions to the ComplianceAsCode project. The automatic running informs contributors and developers about changes that it found and recommends which tests should be run for the change. This saves the time spent on verifying the correctness of contributions as well as the time spent on running tests.
|
|
|
Generic Template-Based Synthesis of Program Abstractions
Marušák, Matej ; Holík, Lukáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to design and to implement a generic strategy solver to the 2LS tool. 2LS is an analyser for a static verification of programs written in C language. A verified program is analysed by an SMT solver using abstract interpretation. Convertion from an abstract state of the program into a logical formula, that an SMT solver can work with, is done by a component called strategy solver. In the current implementation, there is one strategy solver for each abstract domain. Our approach introduces a single generic strategy solver, which makes creating new domains easier. Also, this approach enables migration of the existing domains and hence the codebase can be reduced.
|
|
|
Posouzení informačního systému firmy a návrh změn
Netolická, Lívia ; Malík, Viktor (oponent) ; Koch, Miloš (vedoucí práce)
Bakalárska práca sa zaoberá posúdením informačného systému spoločnosti Stredoslovenská distribučná, a.s. a následným návrhom zmien. V úvodnej časti práce je venovaná pozornosť poznatkom z teoretickej oblasti, ktoré sa spoločne s vypracovanými analýzami stali podkladom ako pre samotné posúdenie systému, tak pre navrhnutie zmien vedúcich k zlepšeniu konkrétnych procesov a čiastkových prvkov informačného systému.
|
|
|
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.
|
|
|
Performance Analysis Based on Noise Injection
Liščinský, Matúš ; Malík, Viktor (oponent) ; Fiedor, Tomáš (vedoucí práce)
In this work, we proposed a Perun-Blower framework which utilises the perfblowing technique: injecting of noise into the functions of the tested program, followed by collecting of runtime data of these functions from the program run and evaluating the impact of the noise on the program performance. We build on the dynamic binary instrumentation of the Pin framework to inject the noise into program. We then focus on finding functions with high impact on performance as well as estimate the thread run's potential acceleration when optimising the particular functions. Moreover, we have extended the existing Trace collector used in the Perun framework to collect the runtime of functions with a new so-called engine based on the Pin framework. We tested the functionality of our implementation on two non-trivial projects, where we were able to find functions (1) with considerable impact on performance, (2) with the most significant optimisation benefit, and (3) whose degradation forces the non-termination of the program after several hours of running.
|
|
|
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.
|
host ::
RSS.