Monitoring

monpoly

It is a growing concern for companies, administrations, and end users alike whether IT systems comply with policies regulating the usage of sensitive data. Checking compliance is particularly acute as many of our modern infrastructures (communication, entertainment, finance, social networks, etc.) are systems that collect, process, and share data.

A prominent approach to compliance checking is runtime monitoring. Here, system actions are observed and automatically checked for compliance against a given policy. A typical monitoring task from the domain of financial services reads as follows: given a stream of cash transfers and limit-raising events produced by a bank, ensure that the following policy always holds: “the total amount of money withdrawn by any customer in the last 30 days does not exceed 5000 CHF, except if the customer has previously received a higher credit limit”. Banks and other highly regulated companies are often faced with hundreds or thousands of such properties that they must comply to and demonstrate compliance to. The above policy demonstrates the need for the policy specification language to be expressive. In particular, it requires aggregations (“total amount”), quantification (“any customer”), Boolean connectives (“except if”), and qualitative (“has previously received”) and quantitative (“30 days”) temporal connectives.

Our research is concerned with developing efficient and scalable monitoring algorithms for expressive policy specification languages. Most of our results have focused on a safety fragment of metric first-order temporal logic , which incorporates all features used in the above example, and other extensions of temporal logics. The implementation of those algorithms gave rise to the efficient MonPoly and Aerial monitoring tools. We are also interested in policy enforcement, that is, preventing policy violations instead of only detecting them.

Software

MonPoly is a prototype monitoring tool that checks compliance of log files with respect to policies. Policies are specified by formulas in MFOTL. The tool is presented in the paper “MONPOLY: Monitoring Usage-control Policies” and it implements the algorithms presented in the papers “Monitoring of Temporal First-order Properties with Aggregations”, “Monitoring Metric First-order Temporal Properties”, and “Greedily computing associative aggregations on sliding windows”. MonPoly can be download from Sourceforge.

Publications

Joshua Schneider, David Basin, Frederik Brix, Srđan Krstić, and Dmitriy Traytel
Scalable Online First-Order Monitoring.
18th International Conference on Runtime Verification (RV 2018), Limassol, Cyprus, 2018.

David Basin, Felix Klaedtke and Eugen Zalinescu
The MonPoly Monitoring Tool
In the Proceedings of the 1st International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools Held in conjunction with the 17th International Conference on Runtime Verification (RV-CuBES 2017).

David Basin, Srđan Krstić, and Dmitriy Traytel
Aerial: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties
In the Proceedings of the 1st International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools Held in conjunction with the 17th International Conference on Runtime Verification (RV-CuBES 2017).

David Basin, Srđan Krstić, and Dmitriy Traytel
Almost Event-Rate Independent Monitoring of Metric Dynamic Logic
In the Proceedings of the 17th International Conference on Runtime Verification (RV), 2017.

David Basin, Felix Klaedtke, and Eugen Zalinescu
Runtime Verification of Temporal Properties over Out-of-order Data Streams
In the Proceedings of the 29th International Conference on Computer-Aided Verification (CAV), 2017.

David Basin, Bhargav Bhatt, and Dmitriy Traytel
Almost Event-Rate Independent Monitoring of Metric Temporal Logic
In the Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2017.

David Basin, Felix Klaedtke, and Eugen Zalinescu
Failure-aware Runtime Verification of Distributed Systems
In the Proceedings of the 35th Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTCCS), 2015.

David Basin, Germano Caronni, Sarah Ereth, Matus Harvan, Felix Klaedtke, and Heiko Mantel
Scalable Offline Monitoring of Temporal Specifications
Formal Methods in System Design, 49(1-2):75-108, 2016.

David Basin, Felix Klaedtke, Samuel Müller, and Eugen Zălinescu
Monitoring of Temporal First-order Properties with Aggregations
Formal Methods in System Design, 46(3):262-285, 2015.

David Basin, Felix Klaedtke, Samuel Müller, and Eugen Zălinescu
Monitoring Metric First-order Temporal Properties
Journal of the ACM, 62(2):15:1–15:45, 2015.

David Basin, Felix Klaedtke, and Eugen Zălinescu
Greedily computing associative aggregations on sliding windows
Information Processing Letters, 115(2):186-192, 2015.
[We present an algorithm for combining the elements of subsequences of a sequence with an associative operator. The subsequences are given by a sliding window of varying size. Our algorithm is greedy and computes the result with the minimal number of operator applications.]

David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zălinescu
On Real-time Monitoring with Imprecise Timestamps
In the Proceedings of the 5th International Conference on Runtime Verification (RV 2014).
[Existing real-time monitoring approaches assume traces with precise timestamps. Their correctness is thus indefinite when monitoring the behavior of systems with imprecise clocks. We address this problem for a metric temporal logic.]

David Basin, Carlos Cotrini Jimenez, Felix Klaedtke, and Eugen Zălinescu
Deciding Safety and Liveness in TPTL
Information Processing Letters, 114(12):680-688, 2014.
[In this paper we show that deciding whether a TPTL formula describes a safety property is EXPSPACE-complete. Moreover, deciding whether a TPTL formula describes a liveness property is in 2-EXPSPACE.]

David Basin, Germano Caronni, Sarah Ereth, Matúš Harvan, Felix Klaedtke and Heiko Mantel
Scalable Offline Monitoring
In the Proceedings of the 5th International Conference on Runtime Verification (RV 2014). Best Paper Award., 2014.

Matúš Harvan, David Basin, Germano Caronni, Sarah Ereth, Felix Klaedtke, and Heiko Mantel
Checking System Compliance by Slicing and Monitoring Logs
Technical Report 791, ETH Zurich, Department of Computer Science, July 2013.
[In this paper we show to parallelize our monitoring approach by using the MapReduce framework. We also provide a theoretical framework for slicing logs. Finally, we report on a real-world case study with Google.]

David Basin, Felix Klaedtke, Matus Harvan, and Eugen Zalinescu
Monitoring Data Usage in Distributed Systems
IEEE Transactions on Software Engineering, 39(10):1403-1426, 2013.
[This is the journal version of the TIME 2012 paper.]

David Basin, Vincent Juge, Felix Klaedtke, and Eugen Zalinescu
Enforceable Security Policies Revisited
ACM Transactions on Information and System Security, Volume 16, Issue 1, 2013.
[This is the journal version of the POST 2012 paper.]

David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zalinescu
Monitoring of Temporal First-order Properties with Aggregations
In the Proceedings of the 4th International Conference on Runtime Verification (RV 2013)
[In this paper we present and evaluate an extension of our monitoring approach that allows one to aggregate over data values. Aggregations often appear in regulations, e.g., “the sum of all withdrawals in the last month of each user must not exceed a given threshold”.]

David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zalinescu
Monitoring Compliance Policies over Incomplete and Disagreeing Logs
In the Proceedings of the 3rd International Conference on Runtime Verification (RV 2012)
[In this paper we extend our monitoring approach to cope with incomplete knowledge about system events, which may arise for instance from logging infrastructure failures and corrupted log files.]

David Basin, Felix Klaedtke, Vincent Juge, and Eugen Zalinescu
Enforceable Security Policies Revisited
In the Proceedings of the 1st Conference on Principles of Security and Trust (POST 2012).
[In this paper we revisit Schneider’s work on policy enforcement by execution monitoring. We overcome limitations of Schneider’s setting by distinguishing between system actions that are controllable by an enforcement mechanism and those actions that are only observable.]

David Basin, Felix Klaedtke, Matus Harvan, and Eugen Zalinescu
MONPOLY: Monitoring Usage-control Policies
In the Proceedings of the 2nd International Conference on Runtime Verification (RV 2011).
Best Tool Paper Award.
[This paper presents the prototype tool implementing our monitoring approach.]

David Basin, Felix Klaedtke, and Eugen Zalinescu
Algorithms for Monitoring Real-time Properties
In the Proceedings of the 2nd International Conference on Runtime Verification (RV 2011).
[In this paper we present and analyze monitoring algorithms for a safety fragment of metric temporal logics under different time models, which have either dense or discrete time domains and are either point-based or interval-based.]

David Basin, Felix Klaedtke, Matus Harvan, and Eugen Zalinescu
Monitoring Usage-control Policies in Distributed Systems
In the Proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME 2011).
[A major challenge when monitoring distributed systems, is to correctly and efficiently monitor the trace interleavings obtained by totally ordering actions that happen at the same time. We identify fragments of MFOTL for which compliance can be checked efficiently, namely, by monitoring a single representative trace in which actions are totally ordered. We also present a real-world case study in the context of a collaboration with Nokia Research.]

David Basin, Felix Klaedtke, and Samuel Müller
Policy Monitoring in First-Order Temporal Logic
In the Proceedings of the 22nd International Conference on Computer Aided Verification (CAV 2010).
[This is an invited paper that presents our monitoring approach.]

David Basin, Felix Klaedtke, and Samuel Müller
Monitoring Security Policies with Metric First-order Temporal Logic
In the Proceedings of the 15th ACM Symposium on Access Control Models and Technologies (SACMAT 2010).
[In this paper we show how a wide variety of security policies, ranging from traditional policies like Chinese Wall and separation of duty to more specialized usage-control and compliance requirements, can be naturally formalized in MFOTL.]

David Basin, Felix Klaedtke, Samuel Müller, and Birgit Pfitzmann
Runtime Monitoring of Metric First-order Temporal Properties
In the Proceedings of the 28th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008).
[This paper is the first to present our monitoring approach. In particular, we present an online algorithm for a safety fragment of metric first-order temporal logic that is considerably more expressive than the logics supported by prior monitoring methods.]