Monitoring Network Traffic by Predicate Logic

We present an approach to the runtime monitoring of network traffic for the violation of properties specified in classical predicate logic. The properties are expressed by quantified formulas which are interpreted over sequences of messages, i.e., the quantified variable denotes a position in the sequence. Using the ordering of stream positions and nested quantification, complex properties can be formulated. To raise the level of abstraction, we allow the definition of a higher-level stream from a lower-level stream by a notation analogous to classical set builders. A translator generates from the specification an executable monitor; a static analysis determines whether the generated monitor only requires a finite number of past messages to be preserved.