Development of graphical tools for security verification

Výzva	Štipendiá pre excelentných výskumníkov a výskumníčky R2-R4
Hlavný riešiteľ	Damas Gruska
Prijímateľ	Univerzita Komenského v Bratislave
Celkový rozpočet	109 757,40 €
Príspevok poskytovateľa	109 757,40 €
Zdroj financovania	Plán obnovy a odolnosti
Začiatok realizácie	august 2026
Koniec realizácie	august 2026
Kategória výskumníka	R3
Vedná oblasť	Fyzikálne, technické vedy a matematika

Anotácia

Grafické modely (Petriho siete, časované automaty atď.) sú osvedčenými nástrojmi pre formálne špecifikácie. Niektoré z nich sú vhodné najmä na overovanie bezpečnostných systémov, ako napríklad Attack Trees, no na druhej strane im chýba podpora automatického alebo poloautomatického overovania bezpečnostných prvkov. Cieľom projektu je vyvinúť metódu, ako môžu byť bezpečnostné prvky (vyjadrené absenciou informačného toku) reprezentované vhodným typom útočných stromov a následne formálne overené, alebo v prípade prítomnosti bezpečnostných dier tieto budú byť graficky označené. Na tento účel plánujeme integrovať rôzne formálne modely a softvérové nástroje, napríklad rôzne typy Attack trees, Timed Automata, TESSLA, UPPAAL atď