FIT works together with Microsoft Research on protection against DoS attacks

Members of the VeriFIT group (Lenka Turoňová, Lukáš Holík, Ondřej Lengál, and Tomáš Vojnar) and their colleague Margus Veanes from Microsoft Research (Redmond, USA) found an innovative approach to protection against a class of DoS attacks. DoS attacks overwhelm the target service with such amount of traffic that it depletes its resources and makes the service unavailable for legitimate users. VeriFIT focuses primarily on ReDoS attacks, i.e. attacks against services using regular expressions.

Regular expressions are supported in all common programming languages. They allow searching for patterns, replace text and also validate user input. If a regular expression is used, for example, to look for patterns in network traffic (e.g. within an intrusion detection system (IDS)) or to validate user input to a network service, hackers can attack it and, for instance, shut down the target service or the intrusion detection system (and then do whatever they want on the network without running the risk of being detected).

First, the hacker tries to create an input string so that it takes a disproportionately long time to validate against the regular expression. If, for example, the login when creating a new user of a service is authenticated using the regular expression /(([\-.]|[_]+)?([a-zA-Z0-9]+)){10,30}/, a ReDoS attack could be caused by the string "aaaaaaaaaaaaaaaaaaaaaaaa!". This is because validators based on backtracking and non-deterministic finite automata will search through all possibilities to split the input string into 10 to 30 substrings before rejecting it. This type of attack shut down Stack Overflow for several days, for example.

Validators based on deterministic finite automata do not suffer from this problem, but they have another issue: deterministic finite automata can be huge (e.g. the smallest deterministic automaton accepting the language of the regular expression /[ab]*a[ab]{300}/ has more states than the estimated number of atoms in the observable universe).

Developed as part of basic research into automata theory in collaboration between VeriFIT and Microsoft Research, the method can verify input efficiently using a newly introduced formal model called counting-set automaton. It is a special type of deterministic automaton, in which the configuration of the automaton contains the status and also certain counting sets, which can effectively represent limited repetition in regular expressions (e.g. the part with the number 300 in the expression/[ab]*a[ab]{300}/). Thanks to these counting sets, a compact automaton can be created even for regular expressions that contain large repetition values, which can then be used for pattern searching or validation. For a certain class of regular expressions, this method provides a more robust pattern-searching algorithm than, for example, the well-known grep tool or Google's optimised RE2 library.

This innovation by the VeriFIT group shows that the theory of finite automata, which was conceived 70 years ago and is often considered to be an unchanging fundamental pillar of theoretical computer science, is still subject to rapid developments with many practical applications.

A video presentation by Lenka Turoňová, who was able to spend her summer at an internship in Microsoft thanks to the co-operation, is available here and the paper on the method is provided at this link.