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}
}

Benchmarks and Performance Analysis of the LogicGuard Framework

Bashar Ahmad, Michael Krieger

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, June 2016. [pdf]
[bib]
@techreport{RISC5370,
author = {Bashar Ahmad and Michael Krieger},
title = {{Benchmarks and Performance Analysis of the LogicGuard Framework}},
language = {english},
abstract = {This paper presents benchmarks, performance measurements and analysisfor LogicGuard framework. The specification and data used to performthe benchmarks are all artificial and were designed to show variouscomplexity levels. For this purpose, a set of parameters was defined togenerate specifications and sample data, which include quantifier depth,search direction, windows size and delay. A set of tools was designed andimplemented to perform the benchmarks and the analysis of the results.In addition to the LogicGuard software, a tool to generate specificationsbased the performance parameters, a tool to process the measurementsand lastly a tool to analyse, extrapolate and plot the results were developed.The results presented show the resource cost in terms of processingtime per message, number of instances and memory usage. To be ableto capture the performance of LogicGuard specification as accurately aspossible, the external function used for monitoring was designed to returnas fast as possible such that the time needed for external processing canbe neglected. Further analysis using polynomial extrapolation is appliedto understand the behaviour of the framework.},
year = {2016},
month = {June},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
sponsor = {Supported by the FFG BRIDGE program by the project 846003 “LogicGuard II”.},
length = {26}
}

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}
}

MK-fuzzy automata

Temur Kutsia, George Rahonis, Wolfgang Schreiner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, May 2016. [pdf]
[bib]
@techreport{RISC5303,
author = {Temur Kutsia and George Rahonis and Wolfgang Schreiner},
title = {{MK-fuzzy automata}},
language = {english},
abstract = {We introduce MK-fuzzy automata over a bimonoid K which is related to the fuzzification of the McCarthy-Kleene logic. Our automata inspired by, and intend to contribute to, practical applications being in development in the LogicGuard project. We investigate closure properties of the class of MK-fuzzy languages accepted by MK-fuzzyautomata as well as by their deterministic counterparts.},
year = {2016},
month = {May},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, runtime verification, automata theory, fuzzy logic},
sponsor = {Supported by the Austrian Research Promotion Agency (FFG) in the frame of the BRIDGE program 846003 "LogicGuard II".},
length = {17}
}

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}
}

The LogicGuard Stream Monitor Specification Language Tutorial and Reference Manual

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

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, October 2015. Technical Report. [pdf]
[bib]
@techreport{RISC5193,
author = {Wolfgang Schreiner and Temur Kutsia and Davic Cerna and Michael Krieger and Bashar Ahmad and Helmut Otto and Martin Rummerstorfer and Thomas Gössl},
title = {{The LogicGuard Stream Monitor Specification Language Tutorial and Reference Manual}},
language = {english},
abstract = {This report describes the design and use of the LogicGuard language for specifyingstream monitors. These monitors observe streams of values (e.g., messages flowing througha network connection) and check whether the streams fulfill desired safety properties. Theseproperties are described on a very high level of abstraction in a purely declarative way by notionsthat are derived from classical predicate logic, in particular by logic formulas that arequantified over stream positions. To raise the level of abstraction, auxiliary internal streamscan be specified whose values are constructed from the values on the external streams bynotions that are thar are similar to classical set builders. From the abstract specificationsautomatically executable monitors are generated which surveil the streams in real time andtrigger warnings if violations of the specified properties are observed.},
year = {2015},
month = {October},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, runtime verification, event processing},
sponsor = {Supported by the Austrian Research Promotion Agency (FFG) in the frame of the BRIDGE program by the projects 832207 "LogicGuard" and 846003 "LogicGuard II".},
length = {54},
type = {Technical Report}
}

2014

Verifying the Soundness of Resource Analysis for LogicGuard Monitors (Revised Version)

Temur Kutsia, Wolfgang Schreiner

Technical report no. 14-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2014. [pdf]
[bib]
@techreport{RISC5056,
author = {Temur Kutsia and Wolfgang Schreiner},
title = {{Verifying the Soundness of Resource Analysis for LogicGuard Monitors (Revised Version) }},
language = {english},
number = {14-08},
year = {2014},
length = {148},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Loading…