|
|
Analýza výkonu programů v jazyce Go
Nešpor, Andrej ; Malík, Viktor (oponent) ; Pavela, Jiří (vedoucí práce)
Cílem této práce je rozšířit výkonnostní verzovací systém Perun implementací modulu pro profilování programů napsaných v jazyce Go. Tento modul implementuje profilovací nástroj technikou instrumentace volání a návratů funkcí pomocí technologie eBPF. Nástroj dokáže sbírat reálný čas běhu funkcí a jejich trasy volání. Zároveň byl implementován nový způsob vizualizace naměřených dat pomocí tzv. Sankey grafu, což usnadní jejich interpretaci. S vytvořeným profilovacím nástrojem pak provádíme pár experimentů, abychom ověřili jeho funkčnost a demonstrovali jeho použití.
|
|
|
Applying formal methods to analysis of semantic differences between versions of software
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an integration of formal methods into DiffKemp, a static analysis tool for analyzing semantic differences of large-scale C projects. The aim of this extension is to facilitate analysis of more complex code changes, which would typically be better handled by a tool based on formal methods, while also maintaining DiffKemp’s scalability to large projects. To achieve this, whenever a possible semantic change is found, the equivalence of the relevant instructions is encoded into an SMT problem instance and the difference is either confirmed or refuted using an SMT solver. The proposed solution has been implemented in DiffKemp and our experiments on a set of benchmarks called EqBench show that it extends the capabilities of DiffKemp, mainly with regards to sound analysis of refactorings of arithmetic expressions.
|
|
|
Generating Code Change Patterns from C
Kučma, Tomáš ; Pavela, Jiří (oponent) ; Malík, Viktor (vedoucí práce)
Ensuring the semantic stability of software projects is often a costly task. DiffKemp is a tool that automatizes this process, with a special emphasis placed on performance and usability in large-scale projects. A trade-off for its efficiency is a greater degree of inaccuracy compared to formal tools. To minimize this issue, DiffKemp allows users to define their own semantics-preserving patterns, describing what kind of changes are to be treated as equal. Currently, this support is restricted to patterns written in LLVM internal representation, which is not a user-friendly language. The purpose of this work is to extend this capability to patterns written in C, significantly simplifying the process of their creation. This includes a proposal of a representation of the patterns, which must be able to encode all necessary meta-information, and subsequent design, implementation, and testing of a DiffKemp extension that allows utilization of patterns encoded in C.
|
|
|
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.
|
host ::
RSS.