|
|
Chaos Testing of the Strimzi Project Using the Litmus Platform
Zrnčík, Henrich ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
Posledná dekáda v poli softwarového inžinierstva sa niesla v duchu automatizácie a abstrakcie. Vzostup nového spôsobu písania a menežovania softwaru (taktiež známeho ako architektúra mikroslužieb) so sebou taktiež priniesol nové výzvy v rámci zaručovania kvality softwaru. Beh systému v cloudovom prostredí s množstvom komponentov, ktoré sú roztrúsene po rôznych uzloch vyžaduje uvažovanie o závislostiach medzi týmito komponentami a dodatočné testovanie ktoré potvrdí odolnosť systému. Riešením je chaos inžinierstvo, často považované za logický krok po testovaní systému ako celku. Táto práca sa zaoberá riešením problému nedostatočných možností pre aplikáciu chaosu (a to prostredníctvom projektu Litmus) do produktu Apache Kafka, ktorý je nasadený na Kubernetes platforme ako súčasť projektu Strimzi. Inými slovami, aby sme mohli aplikovať chaos na projekte Strimzi, či iných systémoch ktoré ho používajú, musíme vytvoriť úplne nové časti Litmusu. Čo sa samotnej aplikácie chaosu týka, fakt že Strimzi je systém sám o sebe, avšak často súčasť iných systémov, znamená že budeme potrebovať vytvoriť rozšírenejšie riešenia. Práca je zavŕšená výslednými experimentami a potvrdením odolnosťi projektu v reálnom nasadení.
|
|
|
Methods of Linux Kernel Hacking
Procházka, Boris ; Malinka, Kamil (referee) ; Vojnar, Tomáš (advisor)
This bachelor thesis focuses on the Linux kernel security from the attacker perspective. It tries to identify and map all key features and methods used by nowadays cyber-terrorists. One of its aims is to give a comprehensive overview of this topic. At final, it can serve as a small reference for everybody who wants to broaden his knowledge of Linux kernel security. The work consists of four parts. The first part repeats and defines basic notions and taxonomy of operation systems. The second and third part form the core. They cover principles and methods used to hide processes, files, connections, etc. The last chaper is devoted to related issues. A supplement of this bachelor thesis is a set of demonstrating modules, which implement discussed problems involved, and tables, where can be found a comparison of nowadays rootkits.
|
|
|
Symbolic Automata for Analysing String Manipulating Programs
Kotoun, Michal ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Mnoho aplikací přijímá, odesílá a zpracovává data v textové podobě. Správné a bezpečné zpracování těchto dat je typicky zajištěno tzv. ošetřením řetězců (string sanitization). Pomocí metod formální verifikace je možné analyzovat takovéto operace s řetězci a prověřit, zda jsou správně navržené či implementované. Naším cílem je vytvořit obecný nástroj pro analýzu systémů jejichž konfigurace lze kódovat pomocí slov z vhodné abecedy, a také jeho specializaci pro analýzu programů pracujících s řetězci. Nejprve jsou popsaný konečné automaty a převodníky a poté různé třídy a podtřídy symbolických převodníků, zejména pak jejich omezení. Na základě těchto informací je pak pro použití v analýze programů navržen nový typ symbolických převodníků. Dále je popsán regulární model checking, speciálně pak jeho variantu založenou na abstrakci automatů, tzv. ARMC, u kterého je známo že dokáže velmi úspěšně překonat problém stavové exploze u automatů a umožňuje nám tzv. dosáhnout pevného bodu v analýze. Poté je navržena vlastní analýza programů psaných v imperativním paradigmatu, a to zejména programů manipulujících s řetězci, založená na principech ARMC. Následuje popis vlastní implementace nástroje s důrazem na jeho praktické vlastnosti. Rovněž jsou popsaný důležité části knihovny AutomataDotNet, na které nástroj staví. Práci je uzavřena diskuzí experimentů s nástrojem provedených na příkladech z knihovny LibStranger.
|
|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
V této práci se zabýváme regulárním model checkingem, což je technika pro analýzu programů, jejíchž stavový prostor může být nekonečný v důsledku práce například s neomezenými frontami, parametry, dynamicky propojenými datovými strukturami, rekurzivními procedurami nebo řetězci. Cílem této práce bylo implementovat vylepšení stávajícího prototypu nástroje ASMA implementujícího regulárním model checking nad knihovnou Automata of Microsoftu. Provedli jsme analýzu zdrojového kódu nástroje ASMA a zopakovaly analýzy všech dostupných srovnávacích programů. Identifikovali jsme některá úzká místa a několik z nich jsme vyřešili. Zejména jsme integrovali knihovnu obsahující další redukční algoritmy do nástroje ASMA, vytvořili několik nových verzí operace reverzní konkatenace, která se v benchmarcích ukázala jako velmi nákladná, vylepšili rozhraní příkazového řádku ASMA a implementovali některé další optimalizace. Výpočetní čas se při analýze větších programů snížil o 90 %.
|
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (referee) ; Křetínský, Mojmír (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.
|
|
|
A Decision Procedure for Strong-Separation Logic
Dacík, Tomáš ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Separační logika (SL) patří mezi nejúspěšnější nástroje pro verifikaci programů pracujících s dynamicky alokovanou pamětí. Její vysoká expresivita ovšem přináší nerozhodnutelnost pokud formule kombinují více jejích spojek, především separační implikace. Jako řešení byla navrhnuta takzvaná silně-separační logika (SSL), která díky striktnější definici sémantiky rozšiřuje rozhodnutelný fragment a přitom zůstává vhodná pro verifikaci programů. V současnosti ale neexistuje žádná implementace rozhodovací procedury pro tuto logiku. Tato práce se zaměřuje na návrh a implementaci rozhodovací procedury pro SSL založené na překladu vstupní formule na formuli v prvořádové logice, jejíž splnitelnost je poté možné ověřit pomocí specializovaných nástrojů. Experimentální výsledky na omezeném fragmentu, kde SL a SSL splývají, ukazují, že navržený nástroj je schopen efektivně řešit formule pocházející z verifikačních nástrojů a výrazně překonává všechny ostatní existující rozhodovací procedury, které jsou také založené na překladu. Během experimentů jsme také odhalili několik případů nekorektnosti heuristik použitých v rozhodovací proceduře pro SL implementované v nástroji cvc5. Na základě našich hlášení byly tyto heuristiky opraveny.
|
|
|
Analysis and Testing of Concurrent Programs
Letko, Zdeněk ; Lourenco, Joao (referee) ; Sekanina, Lukáš (referee) ; Vojnar, Tomáš (advisor)
V disertační práci je nejprve uvedena taxonomie chyb v souběžném zpracování dat a přehled technik pro jejich dynamickou detekci. Následně jsou navrženy nové metriky pro měření synchronizace a souběžného chování programů společně s metodologií jejich odvozování. Tyto techniky se zejména uplatní v testování využívajícím techniky prohledávání prostoru a v saturačním testování. Práce dále představuje novou heuristiku vkládání šumu, jejímž cílem je maximalizace proložení instrukcí pozorovaných během testování. Tato heuristika je porovnána s již existujícími heuristikami na několika testech. Výsledky ukazují, že nová heuristika překonává ty existující v určitých případech. Nakonec práce představuje inovativní aplikaci stochastických optimalizačních algoritmů v procesu testování vícevláknových aplikací. Principem metody je hledání vhodných kombinací parametrů testů a metod vkládání šumu. Tato metoda byla prototypově implementována a otestována na množině testovacích příkladů. Výsledky ukazují, že metoda má potenciál vyznamně vylepšit testování vícevláknových programů.
|
|
|
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á.
|
|
|
A Converter between the LESS and SASS Stylesheet Formats
Večerek, Attila ; Janků, Petr (referee) ; Vojnar, Tomáš (advisor)
Cílem této bakalářské práce je výzkum rozdílů mezi CSS preprocesorovými jazyky, jmenovitě Less a Sass, a nalezení použitelných transormačních metod k implementaci překladače mezi jejich formáty. Nejprve je předložen koncept CSS preprocesorů a následuje detailní popis vlastností jazyků Less a Sass. V této práci jsou uvedené všechny zjištěné rozdíly, a pak jsou představeny nové konverzní metody s demonstrativními příklady. Následuje popis návrhu a implementace překladače. Součástí této práce je tvorba nástroje pro porovnávání CSS, který je postaven na základě transformace abstraktního syntaktického stromu. Návrh komparátoru je popsán spolu s procesem testování, jenž byl použitý pro verifikaci zavedených konverzních metod. V poslední části práce jsou shrnuty dosažené výsledky a je navržen budoucí vývoj překladače.
|
|
|
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.
|
guest ::
