|
|
Detection of Timing Side-Channels in TLS
Koscielniak, Jan ; Malík, Viktor (referee) ; Vojnar, Tomáš (advisor)
Protokol TLS je komplexní a jeho použití je široce rozšířené. Mnoho zařízení používá TLS na ustanovení bezpečné komunikace, vzniká tak potřeba tento protokol důkladně testovat. Tato diplomová práce se zaměřuje na útoky přes časové postranní kanály, které se znovu a znovu objevují jako variace na už známé útoky. Práce si klade za cíl usnadnit korektní odstranění těchto postranních kanálů a předcházet vzniku nových vytvořením automatizovaného frameworku, který pak bude integrován do nástroje tlsfuzzer, a vytvořením testovacích scénářů pro známé útoky postranními kanály. Vytvořené rozšíření využívá program tcpdump pro sběr časových údajů a statistické testy spolu s podpůrnými grafy k rozhodnutí, zda se jedná o možný postranní kanál. Rozšíření bylo zhodnoceno pomocí nových testovacích skriptů a byla předvedena jeho dobrá schopnost rozlišit postranní kanál. Rozšíření spolu s testy je nyní součástí nástroje tlsfuzzer.
|
|
|
Real Time Data Processing with Strimzi Project
Orsák, Maroš ; Malík, Viktor (referee) ; Rogalewicz, Adam (advisor)
Kontajnerové technológie sa v modernej dobe široko využívajú. Vo väčšine prevládajú aplikácie vytvorené na architektúre mikro služieb. Táto práca analyzuje návrh aplikácie, ktorá bude spracovávať údaje v reálnom čase. Aplikácia bude ďalej budovaná pomocou najmodernejších technológií používaných svetovými spoločnosťami ako Netflix, Uber. Používajú tieto systémy na spracovanie údajov v reálnom čase, ako je Apache Kafka, a v poslednom čase ich zavádzajú na vyššiu úroveň zapuzdrením tohto systému do kontajnerového prostredia, čo zaručuje ľahkú škálovateľnosť. Okrem toho využívaju najnovšie natívne technológie Kubernetes na spracovanie mnoho údajov pomocou programov Quarkus a Strimzi. Problém, ktorý sa objavuje, spočíva v tom, že testovanie týchto typov systémov na spracovanie údajov v reálnom čase uzavretých v kontajneroch je obzvlášť náročné. Hlavným cieľom práce je proof-of-concept aplikácie nad Strimzi testami. Táto práca tiež ukáže navrhnutý dlhodobý test applikácie a systému Strimzi, tiež známy ako Marathon, ktorý je ideálnou ukážkou užívateľských podmienok.
|
|
|
Generic Template-Based Synthesis of Program Abstractions
Marušák, Matej ; Holík, Lukáš (referee) ; Malík, Viktor (advisor)
Cieľom tejto práce je návrh a implementácia generického strategy solveru pre nástroj 2LS. 2LS je analyzátor na statickú verifikáciu programov napísaných v jazyku C. Verifikovaný program je za využita abstraktnej interpretácie analyzovaný SMT solverom. Prevod z ab- straktného stavu programu do logickej formule, s ktorou vie pracovať SMT solver vykonáva komponenta nazývaná strategy solver. Aktuálne pre každú doménu existuje jeden takýto solver. Navrhované riešenie vytvára jeden obecný strategy solver, ktorý zjednodušuje tvorbu nových domén. Zároveň navrhovaný spôsob umožnuje prevedenie existujúcich domén a teda zmenšuje program analyzátora.
|
|
|
Generating of Testing Models from Source Code
Kraut, Daniel ; Malík, Viktor (referee) ; Smrčka, Aleš (advisor)
The aim of the masters thesis is to design and implement a tool for automatic generation of paths in source code. Firstly was acquired a study of model based testing and possible design for the desired automatic generator based on coverage criteria defined on CFG model. The main point of the master theis is the tool design and description of its implementation. The tool supports many coverage criteria, which allows the user of such tool to focus on specific artefact of the system under test. Moreover, this tool is tuned to allow aditional requirements on the size of generated test suite, reflecting real world practical usage. The generator was implemented in C++ language and web interface for it in Python language, which at the same time is used to integrated the tool into Testos platform.
|
|
|
Improving Precision of Program Analysis in the 2LS Framework
Smutný, Martin ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout způsob vedoucí ke zvýšení přesnosti analýzy programů pomocí nástroje 2LS, založený na existujících konceptech, a to hlavně na syntézi invariant na základě šablon. 2LS je nástroj pro statickou analýzu programů napsaných v jazyce C, který využívá SMT solver a abstraktní interpretaci k automatickému odvození invariant. V případě kdy 2LS nedokáže rozhodnout zda je program správný, navrhované řešení analyzuje invarianty vypočítané v různých abstraktních doménách, a identifikuje takové části invariant, které mohou s největší pravděpodobností způsobit nejednoznačnost verifikace. Pomocí těchto získaných informací, dokáže navrhnutá metoda identifikovat proměnné původního programu, na kterých pravděpodobně závisí úspěch verifikace. Výstup tohoto řešení může posloužit jako zpětná vazba indikující proměnné, jejíchž problematické hodnoty by měly být omezeny. Také může být výstup využit vývojáři 2LS pro účely debugování při vývoji nových analýz. Řešení bylo implementováno v nástroji 2LS. Na základě různých experimentů mezinárodní soutěže ve verifikaci programů SV-COMP, dokáže řešení identifikovat proměnné způsobující nejednoznačnost verifikace ve více než polovině programů, na kterých verifikace momentálně selhává.
|
|
|
Performance Testing of Linux Kernel Scheduler
Vozár, Jiří ; Rogalewicz, Adam (referee) ; Malík, Viktor (advisor)
Výkon plánovače procesů v jádře operačního systému značně ovlivňuje rychlost a odezvu všech aplikací, které na něm běží. Jakýkoli propad výkonu pak může mít kritické důsledky na běhu aplikací. S příchodem každé nové technologie (např. symetrický multiprocesing) se kód plánovače vyvíjí a rozšiřuje. Proto jsou potřeba regresní testy nejen na jeho fukčnost, ale i výkon. Tato práce mapuje metody testování plánovače operačního systému Linux ve firmě Red Hat. Popisuje způsoby měření výkonu plánovače, sbírání informací o jeho chování, ukládání sesbíraných dat a jejich vizualizaci. Hlavním cílem práce je pak návrh a implementace nového způsobu vizualizace dlouhodobých měření a využití strojového učení pro automatické rozpoznání degradace výkonu mezi dvěma výsledky.
|
|
|
Generating Test Inputs Based on Program Trace
Sušovský, Tomáš ; Malík, Viktor (referee) ; Smrčka, Aleš (advisor)
This thesis focuses on design and implementation of a tool for automated generation of test inputs for a specified program trace. The aim of the thesis is to make development of testing suites (complying a given advanced coverage criteria) easier and more effective. These kinds of test suites are used in critical applications with code base written in low-level languages like C/C++ with strict restrictions applied. The tool investigates a program model and what conditions must be met to execute program in a way following provided trace. The tool uses advanced SMT-solver tool (software tool specialized for solving satisfiability problem) for generating fitting values. LLVM compiler framework libraries are used for modelling a program. Z3 library is used as a SMT-solver backend. This thesis brings results in architectural and implementation design of a tool capable of test inputs generation based on program analysis and provided program trace to cover.
|
|
|
Information System Assessment and Proposal of ICT Modification
Netolická, Lívia ; Malík, Viktor (referee) ; Koch, Miloš (advisor)
In this bachelor thesis author assesses information system of Stredoslovenská distribučná, a.s., energy distribution company, and designs potential changes. First part of the thesis is focused on theoretical knowledge of information systems, and it is further developed and used for assessment of the system itself. Theoretical part together with tailored analyses serves as a mean to design changes leading to improvement of specific processes and partial elements of the information system.
|
|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
Cieľom tejto práce je návrh analýzy tvaru haldy vhodnej pre potreby analyzátora 2LS. 2LS je nástroj pre analýzu C programov založený na automatickom odvodzovaní invariantov s použitím SMT solvera. Navrhované riešenie obsahuje spôsob reprezentácie tvaru programovej haldy pomocou logických formulí nad teóriou bitových vektorov. Tie sú následne využité v SMT solveri pre predikátovú logiku prvého rádu na odvodenie invariantov cyklov a súhrnov jednotlivých funkcií analyzovaného programu. Náš prístup je založený na ukazateľových prístupových cestách, ktoré vyjadrujú dosiahnuteľnosť objektov na halde z ukazateľových premenných. Informácie získané z analýzy môžu byť využité na dokázanie rôznych vlastností programu súvisiacich s prácou s dynamickýcmi dátovými štruktúrami. Riešenie bolo implementované v rámci nástroja 2LS. S jeho použitím došlo k výraznému zlepšeniu schopnosti 2LS analyzovať programy pracujúce s ukazateľmi a dynamickými dátovými štruktúrami. Toto je demonštrované na sade experimentov prevzatých zo známej medzinárodnej súťaže vo verifikácii programov SV-COMP a iných experimentoch.
|
|
|
Dynamic Analysis of Programs Using Library Calls
Malík, Viktor ; Peringer, Petr (referee) ; Smrčka, Aleš (advisor)
The objective of this bachelor's thesis is development of dynamic software analysis which monitors library calls of analysed program. The proposed analyser doubles library call routines in order to create different program runs. These runs are then aggregated into a single control flow graph which can be used for subsequent program analysis. Monitoring and controlling the calls is realised via stubs and wrappers encapsulated within a dynamic shared library for GNU/Linux operating system. The proof of concept is shown on dynamic analyser focused on file system library calls.
|
guest ::
RSS feed.