|
|
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.
|
|
|
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.
|
|
|
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.
|
|
|
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.
|
|
|
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.
|
|
|
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.
|
|
|
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.
|
|
|
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.
|
|
|
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.
|
|
|
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.
|
host ::
RSS.