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

Project Lead

Project Duration

01/10/2014 - 31/03/2017

Project URL

Go to Website

Publications

2017

Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications

David M. Cerna , Wolfgang Schreiner

In: Epic series in computer science, Mohamed Mosbah, Michaël Rusinowitch (eds). (ed.), Proceedings of SCSS 2017, 8th International Symposium on Symbolic Computation in Software Science, Epic 45, pp. 1-15. April 2017. Easy chair, ISSN 2398-7340. [url] [pdf]
[bib]
@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}
}

MK-fuzzy Automata and MSO Logics

Manfred Droste, Temur Kutsia, George Rahonis, Wolfgang Schreiner

In: 8th Symposium on Games, Automata, Logics and Formal Verification (GandALF’17), P. Bouyer, A. Orlandini, P. San Pietro (ed.), Electronic Proceedings in Theoretical Computer Science (EPTCS) 256, pp. 106-120. September 2017. Rome, Italy, September 22-27, ISSN 2075-2180. [pdf]
[bib]
@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}
}

2016

Practical Event Monitoring in the LogicGuard Framework

Wolfgang Schreiner, David Cerna, Temur Kutsia, Michael Krieger, Bashar Ahmad, Helmut Otto, Martin Rummerstorfer, Thomas Gössl

In: embedded world Conference 2016, February 23-25 2016, Nürnberg, Germany, Matthias Sturm et al. (ed.), pp. -. February 2016. Design & Elektronik, Haar, Germany, ISBN 978-3-645-50159-0. [pdf]
[bib]
@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}
}

Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors

David M. Cerna, Wolfgang Schreiner, and Temur Kutsia

In: SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science, James H. Davenport and Fadoua Ghourabi (ed.), Proceedings of The 7th International Symposium on Symbolic Computation in Software Science, EPiC Series in Computing 39, pp. 29-41. 2016. EasyChair, ISSN 2040-557X. [url] [pdf]
[bib]
@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}
}

Predicting Space Requirements for a Stream Monitor Specification Language

David M. Cerna and Wolfgang Schreiner, Temur Kutsia

In: Runtime Verification - 16th International Conference, RV 2016, Madrid, Spain, September 23-30, 2016, Proceedings, Yliès Falcone and César Sánchez (ed.), Proceedings of Runtime Verification, pp. 135-151. September 2016. Springer International Publishing, 978-3-319-46981-2. [url] [pdf]
[bib]
@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}
}

2015

Securing Device Communication by Predicate Logic Specifications

Wolfgang Schreiner, Temur Kutsia, Michael Krieger, Bashar Ahmad, Helmut Otto, Martin Rummerstorfer

In: embedded world Conference 2015, February 24-26 2015, Nürnberg, Germany, Matthias Sturm et al. (ed.), pp. -. February 2015. Design&Elektronik, Haar, Germany, ISBN 978-3-645-50144-6. [pdf]
[bib]
@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}
}

Loading…