Efficient Checking of Time-Quantified Logic Formulas with Applications in Computer Security [LogicGuard]

Project Lead

Project Duration

01/01/2012 - 31/12/2013

Project URL

Go to Website

Publications

2016

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{\`{e}}s Falcone and C{\'{e}}sar S{\'{a}}nchez (ed.), pp. 135-151. 2016. 978-3-319-46981-2. [url]
[bib]
@inproceedings{RISC5739,
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},
isbn_issn = {978-3-319-46981-2},
year = {2016},
editor = {Yli{\`{e}}s Falcone and C{\'{e}}sar S{\'{a}}nchez},
refereed = {yes},
length = {17},
url = {https://doi.org/10.1007/978-3-319-46982-9_9}
}

2014

Monitoring Network Traffic by Predicate Logic

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

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, September 2014. [pdf]
[bib]
@techreport{RISC5057,
author = {Wolfgang Schreiner and Temur Kutsia and Michael Krieger and Ahmad Bashar and Helmut Otto and Martin Rummerstorfer},
title = {{Monitoring Network Traffic by Predicate Logic}},
language = {english},
abstract = {We present an approach to the runtime monitoring of network traffic for theviolation of properties specified in classical predicate logic. The propertiesare expressed by quantified formulas which are interpreted over sequences ofmessages, i.e., the quantified variable denotes a position in the sequence.Using the ordering of stream positions and nested quantification, complexproperties can be formulated. To raise the level of abstraction, we allow thedefinition of a higher-level stream from a lower-level stream by a notationanalogous to classical set builders. A translator generates from thespecification an executable monitor; a static analysis determines whether thegenerated monitor only requires a finite number of past messages to bepreserved.},
year = {2014},
month = {September},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {runtime verification, predicate logic, network security},
sponsor = {Supported by the Austrian Research Promotion Agency (FFG) in the frame of the BRIDGE program by the project 832207 \enquote{LogicGuard}},
length = {15}
}

LogicGuard Type System

Bashar Ahmad and Michael Krieger

RISC Software GmbH, Unit Advanced Computing Technologies, Hagenberg, Austria. Technical report, February 2014. [pdf]
[bib]
@techreport{RISC4958,
author = {Bashar Ahmad and Michael Krieger},
title = {{LogicGuard Type System}},
language = {english},
abstract = {LogicGuard is a framework used to develop formalised specifications to verify and monitor network activities at runtime using predicate logic. This report describes the type system developed for the LogicGuard specification language. The LogicGuard specification language is a typed language and is statically type checked. Based on the language specification we derived the type system's judgments and rules, and accordingly the type checker was implemented.},
year = {2014},
month = {February},
institution = {RISC Software GmbH, Unit Advanced Computing Technologies, Hagenberg, Austria},
sponsor = {FFG BRIDGE Project 832207 "LogicGuard"},
length = {13}
}

2013

Proceedings of the Fifth International Symposium on Symbolic Computation in Software Science, SCSS 2013

Laura Kovacs, Temur Kutsia (ed.)

Technical report no. 13-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2013. [pdf]
[bib]
@techreport{RISC4737,
author = {Laura Kovacs and Temur Kutsia (ed.)},
title = {{Proceedings of the Fifth International Symposium on Symbolic Computation in Software Science, SCSS 2013}},
language = {english},
number = {13-06},
year = {2013},
length = {137},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Verifying the Soundness of Resource Analysis for LogicGuard Monitors, Part 1

Temur Kutsia, Wolfgang Schreiner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, December 16 2013. [pdf]
[bib]
@techreport{RISC4877,
author = {Temur Kutsia and Wolfgang Schreiner},
title = {{Verifying the Soundness of Resource Analysis for LogicGuard Monitors, Part 1}},
language = {english},
year = {2013},
month = {December 16},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
sponsor = {FFG BRIDGE Project 832207 "LogicGuard"},
length = {115}
}

A Resource Analysis for LogicGuard Monitors

Wolfgang Schreiner, Temur Kutsia

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, December 17 2013. [pdf]
[bib]
@techreport{RISC4940,
author = {Wolfgang Schreiner and Temur Kutsia},
title = {{A Resource Analysis for LogicGuard Monitors}},
language = {english},
abstract = {We describe a static analysis that we have devised to determine whether a specificationexpressed in the LogicGuard language gives rise to a monitor that can operate with a finiteamount of resources, notably with finite histories of the streams that are monitored.This information can be passed to the runtime system of the monitor such that after everyexecution step the histories of the monitored streams can be appropriately pruned and themonitor can operate for an indefinite amount of time with a limited amount of memory.First, the analysis is presented for an abstract core language that monitors a single stream;the soundness of the analysis with respect to a formal operational semantics is verified in acompanion paper. Second, we extend the analysis to an extended version of the languagethat can monitor multiple streams and supports the construction of virtual streams. This versionalready resembles the concrete LogicGuard language that is supported by the currentprototype implementation. For the purpose of the analysis, several features of the languagediffer between the abstract and the concrete form; before the analysis can be implemented,the concrete language has to be correspondingly revised.},
year = {2013},
month = {December 17},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, runtime verification, predicate logic},
sponsor = {FFG BRIDGE Project 832207 "LogicGuard"},
length = {45}
}

2012

LogicGuard Abstract Language

Temur Kutsia, Wolfgang Schreiner

Technical report no. 12-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2012. [pdf]
[bib]
@techreport{RISC4552,
author = {Temur Kutsia and Wolfgang Schreiner},
title = {{LogicGuard Abstract Language}},
language = {english},
number = {12-08},
year = {2012},
length = {44},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Translation Mechanism for the LogicGuard Abstract Language

Temur Kutsia, Wolfgang Schreiner

Technical report no. 12-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2012. [pdf]
[bib]
@techreport{RISC4601,
author = {Temur Kutsia and Wolfgang Schreiner},
title = {{Translation Mechanism for the LogicGuard Abstract Language}},
language = {english},
number = {12-11},
year = {2012},
length = {31},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Loading…