The Optimized Checking of Time-Quantified Logic Formulas with Applications in Computer Security [LogicGuard II]

@inproceedings{RISC5404,
author = {David M. Cerna and Wolfgang Schreiner},
title = {{Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications}},
booktitle = {{Epic series in computer science}},
language = {english},
abstract = {Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications},
series = {Epic},
volume = {45},
pages = {1--15},
publisher = {Easy chair},
isbn_issn = {ISSN 2398-7340},
year = {2017},
month = {April},
editor = {Mohamed Mosbah and Michaël Rusinowitch (eds).},
refereed = {yes},
length = {12},
conferencename = {SCSS 2017, 8th International Symposium on Symbolic Computation in Software Science},
url = {http://easychair.org/publications/download/Measuring_the_Gap_Algorithmic_Approximation_Bounds_for_the_Space_Complexity_of_Stream_Specifications}
}

@inproceedings{RISC5470,
author = {Manfred Droste and Temur Kutsia and George Rahonis and Wolfgang Schreiner},
title = {{MK-fuzzy Automata and MSO Logics}},
booktitle = {{8th Symposium on Games, Automata, Logics and Formal Verification (GandALF’17)}},
language = {english},
abstract = {We introduce MK-fuzzy automata over a bimonoid K which is related to the fuzzification of theMcCarthy-Kleene logic. Our automata are inspired by, and intend to contribute to, practical applicationsbeing in development in a project on runtime network monitoring based on predicate logic. We investigate closure propertiesof the class of recognizable MK-fuzzy languages accepted by MK-fuzzy automata as well asof deterministically recognizable MK-fuzzy languages accepted by their deterministic counterparts.Moreover, we establish a Nivat-like result for recognizable MK-fuzzy languages. We introduce anMK-fuzzy MSO logic and show the expressive equivalence of a fragment of this logic with MK-fuzzyautomata, i.e., a B¨uchi type theorem},
series = { Electronic Proceedings in Theoretical Computer Science (EPTCS)},
volume = {256},
pages = {106--120},
address = {Rome, Italy, September 22-27},
isbn_issn = {ISSN 2075-2180},
year = {2017},
month = {September},
editor = {P. Bouyer and A. Orlandini and P. San Pietro},
refereed = {yes},
keywords = {Many-valued logic, fuzzy logic, MSO logic, runtime monitoring.},
sponsor = {The project “LogicGuard II: The Optimized Checking of Time-Quantified Logic Formulas with Applications in Computer Security” is sponsored by the FFG BRIDGE program, project No. 846003.},
length = {15}
}

@inproceedings{RISC5261,
author = {Wolfgang Schreiner and David Cerna and Temur Kutsia and Michael Krieger and Bashar Ahmad and Helmut Otto and Martin Rummerstorfer and Thomas Gössl},
title = {{Practical Event Monitoring in the LogicGuard Framework}},
booktitle = {{embedded world Conference 2016, February 23-25 2016, Nürnberg, Germany}},
language = {english},
abstract = {We describe further progress on the previously introduced LogicGuard specification language and execution framework. This framework generates from a high-level logic specification of a desired property of a stream of events an executable program that observes the stream in real time for violations of the property. While previous presentations were based on an early and incomplete prototype, we are now able to report on some practical applications of the operational framework in the context of network security. As a startup example, we present the “Rogue DHCP” scenario where a device illicitly poses as a DHCP server in order to feed newly connected devices with wrong connectivity information; the monitor detects this attack by looking for duplicate offers to the same DHCP client, of which one is from the attacker. Our main scenario is “Dynamic DNS (DDNS) Cache Poisoining” where an attacker poses as a DDNS client and feeds the DDNS server with wrong DNS update information; the monitor detects this attack by learning about the frequency of legitimate DDNS updates and reporting updates that occur significantly earlier than expected.},
pages = {--},
publisher = {Design & Elektronik},
address = {Haar, Germany},
isbn_issn = {ISBN 978-3-645-50159-0},
year = {2016},
month = {February},
editor = {Matthias Sturm et al.},
refereed = {no},
keywords = {formal methods, runtime verification, event processing},
length = {7}
}

@inproceedings{RISC5264,
author = {David M. Cerna and Wolfgang Schreiner and and Temur Kutsia},
title = {{Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors}},
booktitle = {{SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science}},
language = {english},
abstract = {We analyze the space complexity of monitoring streams of messages whose expected behavior isspecified in a fragment of predicate logic; this fragment is the core of the LogicGuard specificationlanguage that has been developed in an industrial context for the runtime monitoring of network traffic.The execution of the monitors is defined by an operational semantics for the step-wise evaluation offormulas, which requires the preservation of formula instances in memory until their truth value can bedetermined. In the presented work, we analyze the number of instances that have to be preserved overtime for a significant fragment of the core language that involves only “future looking quantifiers”; thislays the foundations for the space analysis of the entire core language.},
series = {EPiC Series in Computing},
volume = {39},
pages = {29--41},
publisher = {EasyChair},
isbn_issn = {ISSN 2040-557X},
year = {2016},
editor = {James H. Davenport and Fadoua Ghourabi},
refereed = {yes},
length = {13},
conferencename = {The 7th International Symposium on Symbolic Computation in Software Science},
url = {http://easychair.org/publications/paper/Space_Analysis_of_a_Predicate_Logic_Fragment_for_the_Specification_of_Stream_Monitors}
}

@inproceedings{RISC5369,
author = {David M. Cerna and Wolfgang Schreiner and Temur Kutsia},
title = {{Predicting Space Requirements for a Stream Monitor Specification Language}},
booktitle = {{Runtime Verification - 16th International Conference, RV 2016, Madrid, Spain, September 23-30, 2016, Proceedings}},
language = {english},
pages = {135--151},
publisher = {Springer International Publishing},
isbn_issn = {978-3-319-46981-2},
year = {2016},
month = {September},
editor = {Yliès Falcone and César Sánchez},
refereed = {yes},
length = {17},
conferencename = {Runtime Verification},
url = {http://dx.doi.org/10.1007/978-3-319-46982-9_9}
}

@inproceedings{RISC5098,
author = {Wolfgang Schreiner and Temur Kutsia and Michael Krieger and Bashar Ahmad and Helmut Otto and Martin Rummerstorfer},
title = {{Securing Device Communication by Predicate Logic Specifications}},
booktitle = {{embedded world Conference 2015, February 24-26 2015, Nürnberg, Germany}},
language = {english},
abstract = {We present a novel approach to the runtime monitoring of network traffic where from a high-level specification of security properties an executable monitor is generated; this monitor observes the network traffic in real time for violation of the specified properties in order to report respectively prevent these violations. The specification formalism is purely based on the classical notions of predicate logic and set theory with the corresponding level of expressiveness; compared to other more restricted formalisms it has thus much stronger capabilities to describe properties of interest. Its high level of flexibility makes our approach also applicable to other problem areas and engineering domains such as process control where it is important to guarantee that sequences of events conform to a particular protocol.},
pages = {--},
publisher = {Design&Elektronik},
address = {Haar, Germany},
isbn_issn = {ISBN 978-3-645-50144-6},
year = {2015},
month = {February},
editor = {Matthias Sturm et al.},
refereed = {no},
keywords = {runtime monitoring; network security; event streams; predicate logic},
sponsor = {Supported by the Austrian Research Promotion Agency (FFG) in the frame of the BRIDGE program by the project 846003 “LogicGuard II”},
length = {9}
}