by Peter Bezděk, Nikola Beneš, Vojtěch Havel, Jiří Barnat, Ivana Černá, A full version of the paper presented at conference ICTAC 2014. June 2014, 27 pages.
FIMU-RS-2014-04. Available as Postscript, PDF.
We introduce the Clock-Aware Linear Temporal Logic (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a~timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique.
by Holger Hermanns, Jan Krčál, Jan Křetínský, April 2014, 36 pages.
FIMU-RS-2014-03. Available as Postscript, PDF.
In contrast to the usual understanding of probabilistic systems as
by Vit Bukac, April 2014, 83 pages.
FIMU-RS-2014-02. Available as Postscript, PDF.
Denial of service (DoS) attacks is an ever growing threat to the availability of computer systems. Numerous solutions have been proposed both for DoS attacks detection and mitigation. However, their evaluation and mutual comparison is complicated due to scarcity of representative contemporary input data. In academia, proposed DoS detection systems are frequently evaluated with obsolete and in practice no longer used tools. Such discrepancy can lead to distinctly different detection efficiency in evaluation environment and real environment. To address this issue, we provide a comparative analysis of traffic features of DoS attacks that were generated by state-of-the-art standalone DoS attack tools. We list frequently used traffic features and verify their presence in analyzed attack traffic. Common denominator of all attack traffic is the presence of repeated similar yet independent operations. Therefore, we propose a new research area for the detection of DoS attacks the source end, based on repeated attack patterns recognition.
by Andriy Stetsko, Tobias Smolka, Václav Matyáš, Martin Stehlik, March 2014, 29 pages.
FIMU-RS-2014-01. Available as Postscript, PDF.
A considerable amount of research has been undertaken in the field of intrusion detection in wireless sensor networks. Researchers proposed a number of relevant mechanisms, and it is not an easy task to select the right ones for a given application scenario. Even when a network operator knows what mechanism to use, it remains an open issue how to configure this particular mechanism in such a way that it is efficient for the particular needs. We propose a framework that optimizes the configuration of an intrusion detection system in terms of detection accuracy and memory usage. There is a variety of scenarios, and a single set of configuration values is not optimal for all of them. Therefore, we believe, such a framework is of a great value for a network operator who needs to optimize an intrusion detection system for his particular needs, e.g., attacker model, environment, node parameters.