|
| |
|
|
Comparing Languages and Reducing Automata Used in Network Traffic Filtering
Havlena, Vojtěch ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
The focus of this thesis is the comparison of languages and the reduction of automata used in network traffic monitoring. In this work, several approaches for approximate (language non-preserving) reduction of automata and comparison of their languages are proposed. The reductions are based on either under-approximating the languages of automata by pruning their states, or over-approximating the language by introducing new self-loops (and pruning redundant states later). The proposed approximate reduction methods and the proposed probabilistic distance utilize information from a network traffic. Formal guarantees with respect to a model of network traffic, represented using a probabilistic automaton are provided. The methods were implemented and evaluated on automata used in network traffic filtering.
|
|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Cílem této práce je vývoj technik umožňujících praktické využití nedeterministických konečných automatů, zejména nedeterministických stromových automatů. Jde zvláště o techniky pro redukci velikosti a testování jazykové inkluze, jež hrají zásadní roli v mnoha oblastech aplikace konečných automatů. V oblasti redukce velikosti vycházíme z dobře známých metod pro slovní automaty které jsou založeny na relacích simulace. Navrhli jsme efektivní algoritmy pro výpočet stromových variant simulačních relací a identifikovali jsme nový typ relace založený na kombinaci takzvaných horních a dolních simulací nad stromovými automaty. Tyto kombinované relace jsou zvláště vhodné pro redukci velikosti automatů slučováním stavů. Navržený princip kombinace relací simulace je relevantní i pro slovní automaty. Náš přínos v oblasti testování jazykové inkluze je dvojí. Nejprve jsme zobecnili na stromové automaty takzvané protiřetězcové algoritmy, které byly původně navrženy pro slovními automaty. Dále se nám podařilo použitím simulačních relací výrazně zefektivnit protiřetězcové algoritmy pro testování jazykové inkluze jak pro slovní, tak pro stromové automaty. Relevanci našich technik pro praxi jsme demonstrovali jejich nasazením v rámci regulárního stromového model checkingu, což je verifikační metoda založená na stromových automatech. Použití našich algoritmů zde vedlo k výraznému zrychlení a zvětšení škálovatelnosti celé metody. Základní myšlenky našich algoritmů pro redukci velikosti automatů a testování jazykové inkluze jsou aplikovatelné i na jiné typy automatů. Příkladem jsou naše redukční techniky pro alternující Büchiho automaty prezentované v poslední části práce.
|
|
|
Reducing Size of Nondeterministic Automata with SAT Solvers
Šedý, Michal ; Havlena, Vojtěch (referee) ; Holík, Lukáš (advisor)
Nedeterministické konečné automaty (NKA) jsou široce využívány v počítačové vědě, například v oblasti formálních jazyků pro reprezentaci regulárních jazyků, k monitorování vysokorychlostních sítí, rozpoznávání obrazu, modelování hardware, nebo dokonce v bioinformatice pro vyhledávání sekvencí nukleotidových kyselin v DNA. NKA jsou také používány v abstraktním regulárním model checkingu, dále ve verifikaci programů manupulujících s řetězci, ve verifikaci programů využívajících ukazatele, pro konstrukci lineárních rovnic a nerovnic, v rozhodovacích procedurách WS1S a WS2S logiky a mnohých dalších. Minimalizace automatů je základní technikou, která pomáhá snižovat nároky na zdroje (paměť, čas nebo množství hardwarových komponentů) a urychlovat operace prováděné na automatech. Běžně používané minimalizační techniky, jakými jsou slučování stavů, odstraňování hran přechodů nebo saturace, mohou v automatech zanechat potenciální minimalizovatelné podgrafy obsahující duplicitní jazykovou informaci. Tyto fragmenty sestávají ze skupiny stavů, kde je již část jazyka jednoho stavu pokryta jazyky ostatních stavů z této skupiny. Tato práce popisuje novou techniku využívající SAT solver, který poskytuje informaci umožňující minimalizovat tyto doposud neminimalizovatelné části automatů. Nově vyvíjená metoda, která využívá pouze informaci od SAT solveru a slučování stavů minimalizuje automaty podobně efektivně, a v případě automatů s nízkým počtem přechodů dokonce rychleji než nástroj RABIT/Reduce, který využívá slučování stavů a odstraňování hran.
|
|
|
Reductions of Automata Used in Network Traffic Filtering
Semrič, Jakub ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
The aim of this work is to propose scalable methods for reducing non-deterministic finite automata used in network traffic filtering. We introduce two approaches of NFAs reduction based on states elimination. To achieve a substantial reduction of automata, we use language non-preserving techniques with a primary focus on language over-approximation, since language preserving methods may not provide sufficient reduction. We implemented the methods and evaluated the accuracy of the reduced automata on real traffic. Our approach does not provide any formal guarantee wrt unseen input traffic, but on the other hand, it can be smoothly used on automata of any size, which is a significant problem for existing methods that have very high time complexity and cannot be applied on really large automata.
|
|
|
Aproximate String Matching
Toth, Róbert ; Košař, Vlastimil (referee) ; Kaštil, Jan (advisor)
This thesis deals with the problem of approximate string matching, ie. string matching allowing errors. Initially, we will define the problem itself and demonstrate variety of it's applications, followed by short survey of different approaches to cope with this problem. The remaining part of the work is focused on algorithms based on the use of deterministic finite automatons. Main algorithms in this area will be presented. Those will be implemented in Python programming language and thoroughly compared in series of experiments.
|
|
|
Efficient Automata Techniques and Their Applications
Havlena, Vojtěch ; Jančar, Petr (referee) ; Mayr, Richard (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá vývojem efektivních technik pro konečné automaty a jejich aplikace. Zejména se věnujeme konečným automatům použitých pří detekci útoků v síťovém provozu a automatům v rozhodovacích procedurách a verifikaci. V první části práce navrhujeme techniky přibližné redukce nedeterministických automatů, které snižují spotřebu zdrojů v hardwarově akcelerovaném zkoumání obsahu paketů. Druhá část práce je je věnována automatům v rozhodovacích procedurách, zejména slabé monadické logice druhého řádů k následníků (WSkS) a teorie nad řetězci. Navrhujeme novou rozhodovací proceduru pro WS2S založenou na automatových termech, umožňující efektivně prořezávat stavový prostor. Dále studujeme techniky předzpracování WSkS formulí za účelem snížení velikosti konstruovaných automatů. Automaty jsme také aplikovali v rozhodovací proceduře teorie nad řetězci pro efektivní reprezentaci důkazového stromu. V poslední části práce potom navrhujeme optimalizace rank-based komplementace Buchiho automatů, které snižuje počet generovaných stavů během konstrukce komplementu.
|
|
|
Construction of Effective Automata for Regex Matching in HW
Frejlach, Jakub ; Havlena, Vojtěch (referee) ; Češka, Milan (advisor)
This thesis is motivated by the application of REs in domains requiring fast matching such has deep packet inspections. To ensure sufficient speed a HW acceleration is typically employed. During the acceleration, REs are in the form of NFA synthesized on FPGA. Although HW acceleration solves the speed problems, it suffers from increased consumption of the FPGA components, specifically LUT. The goal of this thesis is to design, implement and experimentally evaluate heuristic method for approximation of FA in context of HW accelerated RE matching. The purpose of this approximation is to lower consumption of LUT components during FPGA synthesis. The key idea of the method is to add some transitions allowing to construct a smaller number of character classes and thus to reduce the number of LUT implementing the transition relation while reducing the error by modifying only less significant parts of FA. Proposed method together with evaluation pipeline is implemented in TOFA tool. Technique was evaluated on both synthetic and real data. Results of experiments shows, that transitional approximation works especially well on automatas with large number of equivalence character classes.
|
|
|
Visualization of Finite Automata, Pushdown Automata and Turing Machines Work
Syrový, Ondřej ; Láník, Aleš (referee) ; Zuzaňák, Jiří (advisor)
This bachelor`s thesis is focusing on concept and development of computer application for demonstration of finite automata, pushdown automata and Turing machines work. Theoretic volume of this work deals with theories of formal languages and grammars and automata theory. Created program allows to load deterministic and nondeterministic automata variants from the text file, their graphic representation by state diagram and stepping their calculation process.
|
|
|
Fast Regular Expression Matching Using FPGA
Kubiš, Juraj ; Fukač, Tomáš (referee) ; Matoušek, Denis (advisor)
Bachelor thesis deals with the possibility of hardware acceleration of regular expression matches. The content of the thesis is to analyze existing hardware architectures and evaluate their positive and negative properties. Based on this knowledge, the architecture is designed. It is based on deterministic finite automata with implicit transitions (D2FA), is implemented in VHDL and is synthesized. The synthesis results are analyzed to determine the overall throughput of the architecture. It is designed software to convert regular expressions into a D2FA and to optimize this automaton in order to minimize memory requirements. The implementation is verified and the benefits of individual optimization techniques to reduce memory requirements are evaluated.
|
guest ::
