FIT spolupracuje s Microsoft Research na ochraně před DoS útoky

Členové skupiny VeriFIT (Lenka Turoňová, Lukáš Holík, Ondřej Lengál a Tomáš Vojnar) ve spolupráci s Margusem Veanesem z Microsoft Research (Redmond, USA) vytvořili inovativní přístup k ochraně před třídou DoS útoků. Princip DoS útoků spočívají v tom, že se útočník snaží zahltit cílovou službu takovým provozem, aby došlo k vyčerpání systémových prostředků a služba se tak stala nedostupná pro legitimní uživatele. Výzkum skupiny VeriFIT se zaměřuje konkrétně na tzv. ReDoS útoky, což jsou útoky na služby využívající regulární výrazy.

S podporou regulárních výrazů se setkáte ve všech běžně používaných programovacích jazycích. Regulární výrazy umožňují vyhledávat vzory, nahrazovat text a také validovat uživatelské vstupy. Pokud je regulární výraz použit např. pro hledání vzorů v síťovém provozu (například v rámci systému detekce napadení, tzv. IDS) nebo pro validaci uživatelských vstupů síťové služby, mohou na něj zaútočit hackeři a například odstavit systém detekce napadení (a pak si v síti dělat, co chtějí, bez nebezpečí odhalení) nebo cílovou službu.

Takovýto útok probíhá následovně: útočník se snaží vytvořit vstupní řetězec tak, aby jeho ověření vzhledem k danému regulárním výrazu trvalo neúměrně dlouho. Pokud by byl např. login při vytváření nového uživatele  nějaké služby ověřován pomocí regulárního výrazu /(([\-.]|[_]+)?([a-zA-Z0-9]+)){10,30}/, ReDoS útok by mohl být způsoben např. řetězcem  "aaaaaaaaaaaaaaaaaaaaaaaa!". Důvodem je, že validátory postavené na backtrackingu a nedeterministických konečných automatech budou prohledávat všechny možnosti, jak rozdělit vstupní řetězec na 10 až 30 podřetězců, než ho odmítnou. Tento typ útoku způsobil např. několikadenní odstávku známého serveru Stack Overflow.

Validátory postavené na deterministických konečných automatech tímto neduhem netrpí, ale mají jiný problém: deterministické konečné automaty mohou být obrovské (např. nejmenší deterministický automat přijímající jazyk regulárního výrazu /[ab]*a[ab]{300}/ má více stavů, než je odhadovaný počet atomů v pozorovatelném vesmíru). 

Metoda vyvinutá v rámci základního výzkumu v teorii automatů ve spolupráci VeriFITu s Microsoft Research dokáže ověřovat vstup efektivně pomocí nově zavedeného formálního modelu, tzv. automatu s čítacími množinami (counting-set automaton). Jde o speciální typ deterministického automatu, ve kterém konfigurace automatu kromě stavu obsahuje i tzv. čítací množiny, které dokážou efektivně reprezentovat omezené opakování v regulárních výrazech (např. ve výrazu /[ab]*a[ab]{300}/ jde o část s číslem 300). Díky těmto čítacím množinám jde i pro regulární výrazy, které obsahují velké hodnoty opakování, vytvořit kompaktní automat a ten použít pro hledání vzorů nebo validaci. Vzniklý přístup dává pro jistou třídu regulárních výrazů robustnější algoritmus vyhledávání vzorů než např. známý nástroj grep nebo optimalizovaná knihovna RE2 od Googlu.

Tento výsledek skupiny VeriFIT ukazuje, že v teorii konečných automatů, která vznikla před 70 lety a často je považována za neměnný základní pilíř teoretické informatiky, stále probíhá bouřlivý vývoj s mnoha praktickými aplikacemi. 

Na video prezentaci Lenky Turoňové, která si díky spolupráci mohla vyzkoušet, jaké to je strávit léto na stáži v Microsoftu, se můžete podívat tady a na článek na tomto odkazu.