Monitoring of Temporal First-Order Properties with Aggregations - Runtime Verification - page 40

Monitoring of Temporal First-Order Properties
with Aggregations
David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zalinescu
Institute of Information Security, ETH Zurich, Switzerland
Abstract. Compliance policies often stipulate conditions on aggregated
data. Current policy monitoring approaches are limited in the kind of
aggregations that they can handle. We rectify this as follows. First, we
extend metric first-order temporal logic with aggregation operators. This
extension is inspired by the aggregation operators common in database
query languages like SQL. Second, we provide a monitoring algorithm
for this enriched policy specification language. Finally, we experimentally
evaluate our monitor's performance.
1 Introduction
Motivation. Compliance policies represent normative regulations, which specify
permissive and obligatory actions for agents. Both public and private compa-
nies are increasingly required to monitor whether agents using their IT systems,
i.e., users and their processes, comply with such policies. For example, US hos-
pitals must follow the US Health Insurance Portability and Accountability Act
(HIPAA) and financial services must conform to the Sarbanes-Oxley Act (SOX).
First-order temporal logics are not only well-suited for formalizing such regula-
tions, they also admit ecient monitoring. When used online, these monitors
observe the agents' actions as they are made and promptly report violations.
Alternatively, the actions are logged and the monitor checks them later, such as
during an audit. See, for example, [6,18].
Current logic-based monitoring approaches are limited in their support for
expressing and monitoring aggregation conditions. Such conditions are often
needed for compliance policies, such as the following simple example from fraud
prevention: A user must not withdraw more than $10,000 within a 30 day pe-
riod from his credit card account. To formalize this policy, we need an operator
to express the aggregation of the withdrawal amounts over the specified time
window, grouped by the users. In this paper, we address the problem of express-
ing and monitoring first-order temporal properties built from such aggregation
operators.
Solution. First, we extend metric first-order temporal logic (MFOTL) with ag-
gregation operators and with functions. This follows Hella et al.'s [19] exten-
sion of first-order logic with aggregations. We also ensure that the semantics
of aggregations and grouping operations in our language mimics that of SQL.