|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout vylepšený mechanismus rozbalování smyček pro analyzátor 2LS. 2LS je nástroj pro statickou analýzu C programů založený na usuzování o programech pomocí SMT solveru. Kombinuje několik běžných verifikačních technik do algoritmu zvaného k I k I. Jednou z klíčových součástí tohoto algoritmu je rozbalování smyček programu. Současné řešení bohužel neumožňuje správně rozbalovat smyčky obsahující operace s dynamicky alokovanou pamětí. Námi navrhované řešení je založeno na rozbalování smyček v GOTO programu namísto SSA formy, díky čemuž je možné správně pracovat s dynamickými objekty a operacemi s nimi. Navržené řešení bylo implementováno v nástroji 2LS a naše experimenty na sadě testů z mezinárodní soutěže ve verifikaci software (SV-COMP) ukazují, že zvyšuje korektnost analýzy programů pracujících s dynamickými objekty.
|
|
|
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á.
|
|
|
Static Analysis Using Facebook Infer Focused on Errors in RCU-Based Synchronisation
Marek, Daniel ; Malík, Viktor (referee) ; Vojnar, Tomáš (advisor)
Read Copy Update (RCU) je synchronizační mechanismus, který se primárně používa v jádře Linuxu. Mezi jeho vyhledávané vlastnosti patří téměř nulová režie a vysoká rychlost při čtení sdílené paměti. RCU má soubor pravidel používaní, která je potřeba dodržovat, aby synchronizace fungovala správně. Náš výzkum ukázal, že neexistuje žádný analyzátor, který by pořádně kontroloval dodržování pravidel používaní RCU. K překonání tohoto problému jsme navrhli nový analyzátor, který se zaměřuje na porušování pravidel používaní RCU. Analyzátor je založen na statické analýze a implementován jako modul pro nástroj pro statickou analýzu Facebook/Meta Infer. Tato platforma byla vybrána, protože poskytuje škálovatelnost, která je potřebná při práci s tak rozsáhlým softwarem, jakým je Linuxové jádro. Navržený analyzátor je schopen detekovat více porušení pravidel používaní RCU, z nichž každé vede buď na race condition, nebo uváznutí. Je také schopen generovat varování pro situace, kdy je použito volání zastaralé funkce nebo když jsou detekována nekompatibilní primitiva RCU čtecího a zapisovacího procesu. Analyzátor je první svého druhu a může se stát základem pro budoucí vývoj analyzátorů v oblasti Read Copy Update. Kromě toho může být použit jako testovací nástroj v cyklu vývoje jádra Linuxu.
|
|
|
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.
|
|
|
Web-Viewer of Reports of Source Code Analysis
Dolejší, Jakub ; Malík, Viktor (referee) ; Smrčka, Aleš (advisor)
This bachelor thesis deals with design and development of web a application named RepView. The tool is used for interactive revision of source code based on a report of the source code analysis. The Application contains two main services that are running in separate docker containers. The main goal of the application is to simplify interpretation of a report and it's context with source code. The result is achieved by using modern web technologies (Vuejs, Quasar), which allow perform friendly source code revision.
|
|
|
Fuzz Testing of REST API
Segedy, Patrik ; Rogalewicz, Adam (referee) ; Malík, Viktor (advisor)
Táto práca sa zaoberá fuzz testovaním REST API. Po prezentovaní prehľadu techník používaných pri fuzz testovaní a posúdení aktuálnych nástrojov a výskumu zameraného na REST API fuzz testovanie, sme pristúpili k návrhu a implementácii nášho REST API fuzzeru. Základom nášho riešenia je odvodzovanie závislostí z OpenAPI formátu popisu REST API, umožňujúce stavové testovanie aplikácie. Náš fuzzer minimalizuje počet po sebe nasledujúcich 404 odpovedí od aplikácie a testuje aplikáciu viac do hĺbky. Problém prehľadávania dostupných stavov aplikácie je riešený pomocou usporiadania závislostí tak, aby sa maximalizovala pravdepodobnosť získania potrebných vstupných dát pre povinné parametre, v kombinácii s rozhodovaním, ktoré povinné parametre môžu využívať aj náhodne generované hodnoty. Implementácia je rozšírením Schemathesis projektu, ktorý generuje vstupy za pomoci Hypothesis knižnice. Implementovaný fuzzer je použitý na testovanie Red Hat Insights aplikácie, kde našiel 32 chýb, z čoho jednu chybu je možné reprodukovať len za pomoci stavového testovania.
|
|
|
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.
|
|
|
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.
|
|
|
Practical Application of Facebook Infer on Systems Code
Beránek, Tomáš ; Malík, Viktor (referee) ; Vojnar, Tomáš (advisor)
Statická analýza je dnes často využívána ve vývojovém procesu pro hledání defektů v produkovaném softwaru. I když nástroje na statickou analýzu dokáží hledat defekty v softwarech o miliónech řádků kódu, mají také řadu nevýhod. Hlavními nevýhodami jsou náročnost nasazení nástroj na vyvíjený projekt, vysoký počet falešných hlášení a časové i paměťové požadavky. Tato práce se zaměřuje na zmírnění těchto negativních vlastností u nástroje Facebook Infer, zejména pro analýzu Linuxových nástrojů v podobě SRPM balíčků. Pro zjednodušení nasazení byl vytvořen modul pro nástroj csmock, který umožňuje automaticky spouštět statické analyzátory nad balíčky pro CentOS a Fedoru. Pro snížení počtu falešných hlášení byl vytvořen filtr, který filtruje výstup Inferu podle heuristik, které byly navrženy na základě zkušeností získaných kontrolou hlášení z Inferu. Filtr byl také zapojen do modulu pro csmock a otestován na řadě balíčků. Na analyzovaných balíčcích filtr dokázal odstranit 60 % falešných hlášení se ztrátou 2.5 % skutečných defektů. Doba potřebná pro běh analýzy může být zkrácena použitím inkrementální analýzy. U inkrementální analýzy Inferu byly experimentálně zjištěny nedostatky, proto se tato práce věnuje také vytvoření nástavby nad Inferem, která nahrazuje inkrementální analýzu v Inferu.
|
|
|
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.
|
guest ::
RSS feed.