|
|
Hledání regulárních výrazů s využitím technologie FPGA
Kubiš, Juraj ; Fukač, Tomáš (oponent) ; Matoušek, Denis (vedoucí práce)
Bakalárska práca sa zaoberá možnosťami hardvérovej akcelerácie vyhľadávania regulárnych výrazov. Obsahom práce je analýza už existujúcich hardvérových architektúr a zhodnotenie ich pozitívnych a negatívnych vlastností. Na základe týchto poznatkov je navrhnutá architektúra. Tá je založená na deterministických konečných automatoch s implicitnými prechodmi (D2FA), je implementovaná v jazyku VHDL a je vykonaná jej syntéza. Výsledky syntézy sú analyzované za účelom zistenia celkovej priepustnosti architektúry. Je navrhnuté programové vybavenie na prevod regulárnych výrazov do podoby D2FA a na optimalizovanie tohoto automatu s cieľom minimalizovania pamäťových nárokov. Implementácia je overená a je zhodnotený prínos jednotlivých optimalizačných techník na redukciu pamäťových nárokov.
|
|
|
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.
|
|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
In this work we deal with regular model checking which is a technique for analyzing programs whose state space can be infinite due to dealing with, e.g. unbounded queues, parameters, dynamically linked data structures, recursive procedures, or strings. The goal of this work was to implement improvements to the existing prototype tool ASMA implementing regular model checking over the Microsoft Automata library. We analysed the source code of ASMA and reran analyses of all available benchmark programs. We identified some bottlenecks and have tackled several of them. In particular, we integrated a library containing additional reduction algorithms into ASMA, created several new versions of the reverse concatenation operation, which tuned out to be very costly in the benchmarks, improved the command line interface of ASMA, and implemented some other optimizations for ASMA. The computation time was reduced by 90 % when analysing bigger programs.
|
|
|
Mnohaúrovňové automaty a jejich aplikace
Pšenák, Kamil ; Tomko, Martin (oponent) ; Meduna, Alexandr (vedoucí práce)
V tejto práci rozšírime zastarané prístupy v teoretickej informatike. Ukážeme si, že je možný paralelizmus v konečných automatoch zavedením viacúrovňového konceptu. Priblížime si proces kompilácie a stavbu kompilátoru, aby sme mali reálny príklad pre viacúrovňové konečné automaty. Posunieme sa hlbšie do teoretickej informatiky a vysvetlíme si paralelné pravo-lineárne gramatiky a jazyky. Následne si na príklade aj s návrhom implementácie dokážeme tvrdenie. Na záver si spomenieme ďalšie možné odvetvia, kde by sa tento koncept dal využiť.
|
|
|
Srovnání efektivity různých programovacích jazyků při práci s automaty
Polanský, Ondřej ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
V této práci jsou srovnány jazyky C++, C#, OCaml a Python na základě rychlosti, paměťové náročnosti a programátorské přívětivosti. Práce si klade otázku, jak moc se liší programy pracující s konečnými automaty, pokud jsou zapsané v různých jazycích. V každém jazyce je implementována stejná sada základních a pokročilých automatových algoritmů a následně je měřena jejich efektivita na vzorku 200 konečných automatů na unixovém operačním systému. Závěrem jsou prezentovány výsledky a je diskutována vhodnost jednotlivých jazyků pro práci s automaty. Tato práce může posloužit například při výběru jazyka pro tvorbu knihoven pro práci s automaty nebo při návrhu programů a prototypů algoritmů pracujících s automaty.
|
|
|
Strojové učení pro odvozování modelů formálních jazyků
Bardonek, Petr ; Kocman, Radim (oponent) ; Křivka, Zbyněk (vedoucí práce)
Tato bakalářská práce se zabývá odvozováním modelů formálních jazyků. Jedná se o vědní disciplínu na poli výzkumu umělé inteligence. Cílem je vytvořit aplikaci umožňující automatické vytvoření modelu, v podobě konečného automatu, pro neznámý formální jazyk na základě množiny řetězců neznámého formálního jazyka s využitím upravené metody strojového učení.
|
|
|
Efektivní algoritmy pro konečné automaty
Kantor, Tomáš ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato práce prezentuje nový algoritmus pro komplementaci nedeterministických konečných automatů. Současné metody vyžadují převod na deterministický konečný automat, který může mít exponenciálně větší počet stavů. Navržený algoritmus pracuje iterativně po jednotlivých silně souvislých komponentách konečného automatu. Díky tomu umožňuje jednotlivé části efektivněji komplementovat, redukovat a následně propojit s ostatními částmi automatu. Tento algoritmus je tak efektivnější než současné metody pro určité typy konečných automatů.
|
|
|
Detekce narušení počítačové sítě
Hank, Andrej ; Martínek, Tomáš (oponent) ; Kořenek, Jan (vedoucí práce)
Stále rastúce rozšírenie a priepustnosť počitačových sietí prináša mnoho bezpečnostných hrozieb. Jedným z prostriedkov zabezpečenia sú systémy detekcie narušenia (IDS). Nízka priepustnosť softwérových IDS vyúsťuje vo vývoj hardwérových akcelerátorov. Konkrétnym je sonda Traffic Scanner projektu Liberouter využívajúca technológiu FPGA. Jadro akcelerácie spočíva vo vyhľadávaní jednoduchých reťazcov v obsahu paketu. Komplexný popis reťazcov zaručujú regulárne výrazy. Táto práca obohacuje sondu Traffic Scanner o možnosť pokročilého vyhľadávania reťazcov pomocou Perl Compatible Regular Expressions (PCRE) implementovaným transformátorom. Ďalej prináša návrh a implementáciu programového vybavenia umožňujúceho využiť funkcionalitu akcelerátoru užívateľom. Podáva koncepciu detekcie narušenia sieťe s využítím sondy Traffic Scanner a možnosti spolupráce s inými bezpečnostnými zariadeniami.
|
|
|
Multidimensionální jazyky a jejich automaty
Dibďák, Lukáš ; Martiško, Jakub (oponent) ; Meduna, Alexandr (vedoucí práce)
Práce seznamuje s teorií formálních jazyků a konečných automatů. Popisuje zobecnění této teorie do dvou rozměrů. Představuje základní typy dvoudimensionálních automatů, přede- vším teselační automaty. Pro teselační automaty jsou nabídnuty algoritmy k jejich determinizaci. Jeden z algoritmů je následně používán přiloženou aplikací pro determinizaci.
|
|
|
Implementace jednotky pro vyhledávání vzorů v FPGA
Košař, Vlastimil ; Kořenek, Jan (oponent) ; Kaštil, Jan (vedoucí práce)
Tato práce pojednává o algoritmech pro vyhledávání vzorů používaných v moderních systémech pro detekci nežádoucího provozu, přičemž se zaměřuje na algoritmy umožňující vyhledávání regulárních výrazů. Zabývá se přístupy založenými na deterministických a nedeterministických konečných automatech, hybridními přístupy a přístupem založeným na regulárních výrazech jako programovacím jazyku speciálních procesorů. Dále popisuje návrh implementace jednotek pro vyhledávání vzorů popsaných regulárními výrazy založených na několika z popsaných přístupů včetně metodiky odhadu zabraných zdrojů. V další části je popsán vyvinutý softwarový systém pro generování jednotek. V následující části jsou ukázány a diskutovány dosažené výsledky.
|
host ::
RSS.