Technical Reports

A list with abstracts sorted by year - 2014

On Clock-Aware LTL Properties of Timed Automata

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.

Abstract:

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.

Probabilistic Bisimulation: Naturally on Distributions

by Holger Hermanns, Jan Krèál, Jan Køetínský, April 2014, 36 pages.

FIMU-RS-2014-03. Available as Postscript, PDF.

Abstract:

In contrast to the usual understanding of probabilistic systems as stochastic processes, recently these systems have also been regarded as transformers of probabilities. In this paper, we give a natural definition of strong bisimulation for probabilistic systems corresponding to this view that treats probability distributions as first-class citizens. Our definition applies in the same way to discrete systems as well as to systems with uncountable state and action spaces. Several examples demonstrate that our definition refines the understanding of behavioural equivalences of probabilistic systems. In particular, it solves a longstanding open problem concerning the representation of memoryless continuous time by memoryfull continuous time. Finally, we give algorithms for computing this bisimulation not only for finite but also for classes of uncountably infinite systems.

Traffic characteristics of common DoS tools

by Vit Bukac, April 2014, 83 pages.

FIMU-RS-2014-02. Available as Postscript, PDF.

Abstract:

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.

Improving Intrusion Detection Systems for Wireless Sensor Networks

by Andriy Stetsko, Tobias Smolka, Václav Matyá¹, Martin Stehlik, March 2014, 29 pages.

FIMU-RS-2014-01. Available as Postscript, PDF.

Abstract:

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.