News

The split 4th-10th place of the IT Spy competition went to Roman Andriushchenko from FIT. His diploma thesis, supervised by Milan Češka Jr., deals with computer-aided synthesis of probabilistic models. The work significantly increases the speed and accuracy of probability programs. These play a significant part in various areas of engineering and in fact represent the design of programs whose goal is to determine unknown parameters in order to achieve a given result. These programs can be used, for example, to design a communication protocol capable of transferring a specified amount of data, or to find optimal strategies for areas such as energy consumption management. The expert jury, made up of leading academics and business representatives, selected the best works out of over 1,400 diploma theses in the field of computer science from Czech and Slovak universities.

Interaktivní výstavu na téma robotiky připravilo Technické muzeum v Brně ke stému výročí prvního vydání dramatu Karla Čapka R. U. R., v němž autor poprvé použil tehdy nové slovo "robot". Výstava představuje význam robotiky v průmyslu, vědě a technice, ale také v kultuře a umění. Mezi stovkou exponátů najdou návštěvníci také roboty z FIT. For more information, read the article. 

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.