|
|
Symbolic Automata for Analysing String Manipulating Programs
Kotoun, Michal ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Many software applications receive, send and process data in a text form. Correct and safe processing of these data is usually ensured by so-called string sanitization. With the help of methods of formal verification, we can analyse these string operations and check whether they are correctly designed and implemented. The goal of this work is to create a tool for analysis of systems whose configurations can be encoded as words over a suitable alphabet, as well as its specialization for analysing string manipulating programs. First, we describe finite automata and transducers in general and characterize various classes and sub-classes of symbolic transducers, especially their limitations. Based on this study, a new class of symbolic transducers is proposed for use in the program analysis. Later, we introduce regular model checking, especially its variant based on abstraction over automata, the so called ARMC, which was proved to be able to quite successfully fight the state explosion problem in the size of the automata and allows us to reach a fix-point. We then design an analysis of programs written in imperative languages, especially those that manipulate strings, using the principles of ARMC. Finally, the implementation of the tool is presented, highlighting its practical aspects and discussing relevant parts of AutomataDotNet library it is based on. The work completes debating the experimental evaluation of the tool using test inputs from LibStranger project.
|
|
|
Efektivní algoritmy pro práci s Büchiho automaty
Laščák, Tomáš ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Cílem této práce je rozšířit existující knihovnu VATA o modul pro práci s Büchiho automaty, které se řadí mezi konečně stavové automaty nad nekonečnými slovy. Tyto automaty jsou využívány v různých oblastech informatiky, mimo jiné také ve formální verifikaci, při LTL model checkingu. LTL model checking se provádí typicky za pomocí operace testování jazykové inkluze mezi dvěma Büchiho automaty. Protože jazyková inkluze může být výpočetně velmi náročná, vzniklo několik optimalizovaných algoritmů pro tento problém, jako je například přístup založený na Ramseyho větě. Předkládaná práce je zaměřena na tento přístup, jehož implementace je přidána do nově vytvořeného rozšíření knihovny VATA. Mimo to jsou do tohoto nového rozšíření přidány také další operace nad Büchiho automaty, jako jsou sjednocení, průnik nebo redukce počtu stavů.
|
|
|
Generování protipříkladů při analýze Markovových modelů
Molek, Martin ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
Tato práce se zabývá generováním protipříkladů v kontextu verifikace pravděpodobnostních systémů. Protipříklady jsou generovány nad Markovovými modely (přesněji DTMC). Specifikace vlastností modelu jsou zadávány pomocí logiky PCTL, která je v této práci popsána. Pro generování protipříkladů byly použity dva různé algoritmy (Best-first search a Recursive Enumration Algorithm). Práce obsahuje popis implementace algoritmů do verifikačního nástroje STORM. Výsledky experimentů ukazují, že REA je schopen pracovat s modely obsahující miliony stavů.
|
|
|
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.
|
|
|
Model checking nekonečně stavových systémů založený na inferenci jazyků
Rozehnal, Pavel ; Křena, Bohuslav (oponent) ; Vojnar, Tomáš (vedoucí práce)
Regulární model checking je metoda pro verifikaci nekonečně stavových systémů. Je založena na kódování jejich konfigurace jako slov nad konečnou abecedou, množiny konfigurací jako konečného automatu a přechodů jako konečných transducerů. Je zde představen nový přístup k regulárnímu model checkingu založený na odvozování regulárních jazyků. Metoda je založena na prozkoumávání nekonečně stavového systému, jehož chování může být modelováno použitím transducerů, které zachovávají délku řetězců a jejich aplikací je možné získat všechny dosažitelné konfigurace systému. Naše metoda regulárního model checkingu je založena na odvozování regulárních jazyků pomocí algoritmu Angluin, který je použit pro nalezení vhodného invariantu (nadaproximace), který je schopen zodpovedět otázku zachování či porušení nějaké vlastnosti. Je zde také uveden úvod do teorie konečných automatů, model checkingu, SAT problémů a popis Angluinova a Biermanova algoritmu pro učení konečných automatů.
|
|
|
Hledání řídicích strategií pomocí UPPAAL STRATEGO
Hruška, Filip ; Hrubý, Martin (oponent) ; Strnadel, Josef (vedoucí práce)
Tato práce se zabývá hledáním řídicích strategií v předem vybraných problémech z různých oblastí pomocí nástroje Uppaal Stratego. Byly vybrány čtyři oblasti k řešení, jmenovitě šachy, hanojské věže, posuvné pole a kinematický problém zahrnující balíček, auto a letadlo. Pro zvolené problémy a oblasti byla navržena a vytvořena sada jim odpovídajícím modelů. U hanojských věží a posuvného pole bylo možné úspěšně vyhodnotit relevantní strategie, zvedající pravděpodobnosti úspěchu až na více než 90 %. U dalších modelů byl nalezen problém ve velikosti stavového prostoru a strategie nebylo možné vyhodnotit, protože maximální kapacita paměti, kterou nástroj využívá, nebyla dostatečná. U kinematického problému se po omezení a zjednodušení modelu podařilo strategie vyhodnotit, ovšem u šachů to nebylo možné ani po významném zjednodušení.
|
|
|
Databáze specifikací bezpečnostních protokolů
Ondráček, David ; Trchalík, Roman (oponent) ; Očenášek, Pavel (vedoucí práce)
Původní protokoly, které vznikaly v počátcích vývoje počítačových sítí, již nejsou pro zajištění potřebné bezpečnosti dostačující. Proto se stále vyvíjejí a implementují protokoly nové. Důležitou součástí tohoto procesu je formální verifikace. Jde o analýzu protokolu po formální stránce, kdy se zjišťuje, zda lze protokol úspěšně napadnout. Diplomová práce se zabývá analýzou vybraných bezpečnostních protokolů a nástrojů pro jejich formální verifikaci. Výstupem praktické části je databáze specifikací protokolů v LySa kalkulu a výsledky jejich verifikace nástrojem LySatool.
|
|
|
Překladač jazyka VHDL pro potřeby formální verifikace
Matyáš, Jiří ; Smrčka, Aleš (oponent) ; Charvát, Lukáš (vedoucí práce)
Cílem této bakalářské práce je navrhnout a implementovat překladač, který umožňuje převod popisu hardware z jazyka VHDL do grafové reprezentace v jazyce VAM (Variable Assignment Language). Program je určen pro potřeby formální verifikace výzkumné skupiny VeriFIT Fakulty informačních technologií VUT Brno. Důvodem vypracování této práce je poskytnutí možnosti formálně verifikovat návrh hardware s využitím vysokoúrovňových návrhových jazyků, jakým je například jazyk VHDL.
|
|
|
Refactoring and Verification of the Code of mkfs xfs
Ťulák, Jan ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work describes the processes of refactoring mkfs.xfs program for a purpose of refining its code and cleaning the technical debt accumulated over 20 years of the program’s existence. The mkfs.xfs source code is then a subject to static analysis and the used tools (CppCheck, Coverity, Codacy, GCC, Clang) are compared in terms of the number and type of the found defects.
|
|
|
Verifikace programů s ukazateli založená na detekci vzorů
Kubíček, Jan ; Erlebach, Pavel (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce navazuje na výsledky studií v oblasti verifikace nekonečně stavových systémů. Konkrétně se jedná o oblast abstraktního model checkingu. Seznámili jsme se s metodou založenou na abstrakci paměťové konfigurace pomocí paměťových vzorů. Tato metoda byla navržena pro verifikaci programů pracujících s dynamickými paměťovými strukturami jako například seznamy. Na dynamické paměťové struktury je nahlíženo jako na orientované grafy. Verifikace na základě paměťových vzorů abstrahuje obecně libovolné množství vytvořených uzlů do jednoho sumarizovaného uzlu. Tím se dosáhne reprezentace obecně neukončeného grafu konečným zápisem. Poté je možno efektivně provést verifikaci nad tímto abstrahovaným grafem. V naší práci se zabýváme tvorbou modelu pro nástroj implementující verifikaci na základě paměťových vzorů. Model programu je vytvořen z podmnožiny jazyka C. Hlavním přínosem práce je automatizace tvorby modelu pro verifikaci a tím dosáhnutí úplné automatizovanosti procesu verifikace. Je tak možné verifikovat programy napsané v běžném programovacím jazyce. V této práci je diskutována syntaxe vstupního jazyka i implementační detaily překladu.
|
host ::
RSS.