Ověřit platnost přístupových práv do cloudových řešení, verifikovat řídicí systémy pro letecký průmysl či odhalit zranitelnosti v kódu webových aplikací. To vše brzy dokáže nástroj Davida Chocholatého a jeho týmu z FIT VUT, který využívá technologii řešení omezení nad řetězci založenou na automatové teorii. Doktorand za něj získal i cenu Brno Ph.D. Talent.

Projekt Davida Chocholatého vychází z aplikované matematiky a informatiky. Jeho cílem je zlepšit kyberbezpečnost pomocí inovativních metod využívajících automatové technologie a řešení omezení nad řetězci – tzv. string solving.

„Snažíme se zajistit bezpečnější přístup na webové stránky pro běžné uživatele. Zamezit zneužití zranitelnosti při přihlašování se do aplikací webového bankovnictví a dalších. Ověřujeme, že když uživatel vyplní údaje do formuláře, nemohl nikdo tato data odcizit nebo zneužít – například je smazat nebo přeprodat,“ vysvětluje doktorand.

Právě k tomu na FIT VUT využívají string solvingu, který nadále zlepšují a vyvíjejí zapojením metod automatových technologií. Automaty jsou reprezentace procesů a je jimi možné kódovat postupy či algoritmy. „Jsme schopni zjistit, zda v takovém automatu, který modeluje průběh programu, existuje vztah označovaný za škodlivý,“ pokouší se přiblížit výzkumník.

Projekt se primárně zabývá zvýšením bezpečnosti na webových stránkách, využití ale může najít i u zvýšení bezpečnosti administrátorského rozhraní pro správu serverů, jako je Amazon Web Services. „Kdekoliv běží aplikace, v níž uživatel vyplňuje do prázdných polí text, tak je to jeden z možných cílů hackera,“ vysvětluje.

Na vývoji nástroje proto tým spolupracuje také s leteckou společností Honeywell Aerospace. Experti zde modelují řídicí systémy do kokpitů letadla Airbus. „Na nás je pohlídat, zda jsou tyto programy správné. Generujeme automatické testy, které ověřují, že všechny tyto programy jsou bezpečné a nenachází se v nich chyba. Pilot tak třeba nedostane pokyn k vypnutí motoru, pokud by to ohrozilo bezpečnost letu,“ dodává.

Metoda, kterou na FIT VUT vyvíjejí, je aktuálně nejrychlejší na světě. „Existují globálně uznávané databáze problémů, které string solver umí řešit. A k jejich řešení se pořádají i soutěže – my jsme v roce 2024 vyhráli soutěž String Solving ­– konkrétně divizi SMT-COMP 24. Výpočetních problémů jsme ve srovnání se všemi ostatními nástroji na světě vyřešili nejvíce, nejrychleji a s nejmenšími výpočetními zdroji. A to přesto, že nástroj vyvíjíme pouze dva roky, zatímco ostatní technologie vznikaly desetiletí,“ říká Chocholatý.

Důvodem úspěchu je podle něj využití inovativních metod a aplikace automatové teorie do praxe. „Většina nástrojů automaty nepoužívá, jsou považovány za těžkopádné a neefektivní. My v našem výzkumu ukazujeme, že pokud jsou implementovány kvalitně a správně, dokážou být efektivnější než existující metody. Ty už jsou staré a vyzkoušené, proto řada z nich vyčerpala prostor pro zlepšování a optimalizaci,“ popisuje.

Nástroj, který na základě metody automatové teorie nyní na FIT VUT vzniká, se jmenuje Z3-Noodler a automatová knihovna Mata. „Snažíme se, aby náš nástroj byl nejen co nejrychlejší, ale i aplikovatelný na reálné problémy. Je to velmi obecná metoda, která dokáže pokrýt škálu problémů – nejen ty, které jsme zmínili. Potenciál uplatnění tohoto řešení je téměř nekonečný. Dokázal by vydat na několik životů. Je to příležitost pro mě i moji výzkumnou skupinu. Teď můžeme tuto vizi posunout i do praxe,“ zhodnotil doktorand.

„Ocenění v soutěži Brno Ph.D. Talent není jen osobní úspěch. Je to potvrzení, že můj výzkum má praktické využití a smysl. Je to maják, že tímto směrem má smysl pokračovat, protože hodnotu projektu vidí nejen lidé v akademické sféře, ale i v praxi. A já mám možnost zlepšit kyberbezpečnost pro všechny lidi pracující na počítači připojeném k internetu,“ uzavřel Chocholatý.

(mar)