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

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

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

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

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