|
|
Učení se automatů pro rychlou detekci anomálií v síťovém provozu
Hošták, Viliam Samuel ; Matoušek, Petr (oponent) ; Holík, Lukáš (vedoucí práce)
Táto práca sa zaoberá rýchlou detekciou sieťových anomálií na základe učenia automatov. Popisuje a porovnáva niekoľko vybraných algoritmov učenia automatov, vrátane ich aplikácie na učenie sieťových charakteristík. Pre takto naučené automaty je navrhnutých niekoľko metód detekcie sieťových anomálií, ktoré umožňujú odhaliť tak sekvenčné, ako aj štatistické anomálie v rámci komunikácie. Za týmto účelom využívajú mechanizmy samotných automatov, ich transformáciu, či štatistickú analýzu. Navrhované metódy detekcie boli implementované a vyhodnotené na prevádzke protokolu IEC 60870-5-104 používaného v industriálnych kontrolných systémoch.
|
|
|
Nástroj pro abstraktní regulární model checking
Chalk, Matěj ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.
|
|
|
Knihovna pro konečné automaty a převodníky
Bieliková, Michaela ; Lengál, Ondřej (oponent) ; Hruška, Martin (vedoucí práce)
Konečné automaty majú široké uplatnenie v informatike, okrem iných vo formálnej verifikácii, modelovaní systémov a spracovaní prirodzeného jazyka. Avšak modely skutočne reprezentujúce realitu bývajú veľmi komplikované a môžu byť definované nad veľkými, v niektorých prípadoch až nekonečnými, abecedami, a teda môžu obsahovať veľký počet prechodov. V týchto prípadoch nemusí byť je použitie algoritmov na prácu s konečnými automatmi efektívne. Symbolické automaty poskytujú stručnejší zápis tak, že namiesto symbolov v prechodoch používajú predikáty. Konečné prevodníky tiež majú široké uplatnenie, od ligvistiky až po formálnu verifikáciu. Symbolické prevodníky nahradzujú symboly dvojicou predikátov - jeden predikát pre vstupné symboly a jeden pre výstupné. Cieľom tejto práce je návrh knižnice pre klasické a symbolické automaty a prevodníky, ktorá bude vhodná na rýchle prototypovanie nových algoritmov.
|
|
|
Simulace pro symbolické automaty
Síč, Juraj ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
Symbolické automaty sú podobné klasickým automatom s jedným veľkým rozdielom: prechody sú značené predikátmi definovanými v oddelenej teórii. Toto umožňuje použiť veľké abecedy s pouźitím oveľa menšieho miesta. V tejto práci sa zaoberáme výpočtom simulácie (binárnej relácie nad množinou stavov, ktorá aproximuje jazykovú inklúziu) pre tieto automaty. Táto relácia sa dá potom použiť pri redukovaní počtu stavov bez nutnosti determinizácie. Existuje niekoľko algoritomv pre výpočet simulácie pre Kripkeho štruktúry, ktoré boli neskôr modifikované pre označené prechodové systémy a klasické automaty. V tejto práci ukážeme ako sa dá jeden z týchto algoritmov modifikovať pre symbolické automaty použitím rozkladu domény abecedy ktorý je kompatibilný s predikátmi značiacimi prechody a použitím možností teórie abecedy.
|
|
|
Učení se automatů pro rychlou detekci anomálií v síťovém provozu
Hošták, Viliam Samuel ; Matoušek, Petr (oponent) ; Holík, Lukáš (vedoucí práce)
Táto práca sa zaoberá rýchlou detekciou sieťových anomálií na základe učenia automatov. Popisuje a porovnáva niekoľko vybraných algoritmov učenia automatov, vrátane ich aplikácie na učenie sieťových charakteristík. Pre takto naučené automaty je navrhnutých niekoľko metód detekcie sieťových anomálií, ktoré umožňujú odhaliť tak sekvenčné, ako aj štatistické anomálie v rámci komunikácie. Za týmto účelom využívajú mechanizmy samotných automatov, ich transformáciu, či štatistickú analýzu. Navrhované metódy detekcie boli implementované a vyhodnotené na prevádzke protokolu IEC 60870-5-104 používaného v industriálnych kontrolných systémoch.
|
|
|
Nástroj pro abstraktní regulární model checking
Chalk, Matěj ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.
|
|
|
Knihovna pro konečné automaty a převodníky
Bieliková, Michaela ; Lengál, Ondřej (oponent) ; Hruška, Martin (vedoucí práce)
Konečné automaty majú široké uplatnenie v informatike, okrem iných vo formálnej verifikácii, modelovaní systémov a spracovaní prirodzeného jazyka. Avšak modely skutočne reprezentujúce realitu bývajú veľmi komplikované a môžu byť definované nad veľkými, v niektorých prípadoch až nekonečnými, abecedami, a teda môžu obsahovať veľký počet prechodov. V týchto prípadoch nemusí byť je použitie algoritmov na prácu s konečnými automatmi efektívne. Symbolické automaty poskytujú stručnejší zápis tak, že namiesto symbolov v prechodoch používajú predikáty. Konečné prevodníky tiež majú široké uplatnenie, od ligvistiky až po formálnu verifikáciu. Symbolické prevodníky nahradzujú symboly dvojicou predikátov - jeden predikát pre vstupné symboly a jeden pre výstupné. Cieľom tejto práce je návrh knižnice pre klasické a symbolické automaty a prevodníky, ktorá bude vhodná na rýchle prototypovanie nových algoritmov.
|
|
|
Simulace pro symbolické automaty
Síč, Juraj ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
Symbolické automaty sú podobné klasickým automatom s jedným veľkým rozdielom: prechody sú značené predikátmi definovanými v oddelenej teórii. Toto umožňuje použiť veľké abecedy s pouźitím oveľa menšieho miesta. V tejto práci sa zaoberáme výpočtom simulácie (binárnej relácie nad množinou stavov, ktorá aproximuje jazykovú inklúziu) pre tieto automaty. Táto relácia sa dá potom použiť pri redukovaní počtu stavov bez nutnosti determinizácie. Existuje niekoľko algoritomv pre výpočet simulácie pre Kripkeho štruktúry, ktoré boli neskôr modifikované pre označené prechodové systémy a klasické automaty. V tejto práci ukážeme ako sa dá jeden z týchto algoritmov modifikovať pre symbolické automaty použitím rozkladu domény abecedy ktorý je kompatibilný s predikátmi značiacimi prechody a použitím možností teórie abecedy.
|
host ::
RSS.