Runtime Policy Monitoring and Enforcement

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 their compliance is particularly acute as many of our modern infrastructures (communication, entertainment, finance and banking, social networks, etc.) are based on IT 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 policy. Our research project is concerned with developing efficient and scalabale runtime monitoring techniques for expressive policy specification languages. Most of our results have focused on a safety fragment of metric first-order temporal logic (MFOTL). 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 [13] and it implements the algorithms presented in [1,2,3]. MonPoly can be download from https://sourceforge.net/projects/monpoly/.

Publications

  1. Monitoring of Temporal First-order Properties with Aggregations
    David Basin, Felix Klaedtke, Samuel Müller, and Eugen Zălinescu
    To appear in Formal Methods in System Design.
    [This is the journal version of the RV 2013 paper.]
  2. Monitoring Metric First-order Temporal Properties
    David Basin, Felix Klaedtke, Samuel Müller, and Eugen Zălinescu
    To appear in Journal of the ACM.
    [This is the journal version of the FSTTCS 2008 paper.]
  3. Greedily computing associative aggregations on sliding windows
    David Basin, Felix Klaedtke, and Eugen Zălinescu
    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.]
  4. On Real-time Monitoring with Imprecise Timestamps
    David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zălinescu
    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.]
  5. Deciding Safety and Liveness in TPTL
    David Basin, Carlos Cotrini Jimenez, Felix Klaedtke, and Eugen Zălinescu
    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.]
  6. Scalable Offline Monitoring
    David Basin, Germano Caronni, Sarah Ereth, Matúš Harvan, Felix Klaedtke and Heiko Mantel
    In the Proceedings of the 5th International Conference on Runtime Verification (RV 2014).
    Best Paper Award.
    [This is the conference version of the technical report below.]
  7. Checking System Compliance by Slicing and Monitoring Logs
    Matus Harvan, David Basin, Germano Caronni, Sarah Ereth, Felix Klaedtke, and Heiko Mantel
    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.]
  8. Monitoring Data Usage in Distributed Systems.
    David Basin, Felix Klaedtke, Matus Harvan, and Eugen Zalinescu
    IEEE Transactions on Software Engineering, 39(10):1403-1426, 2013.
    [This is the journal version of the TIME 2012 paper.]
  9. Enforceable Security Policies Revisited
    David Basin, Vincent Juge, Felix Klaedtke, and Eugen Zalinescu
    ACM Transactions on Information and System Security, Volume 16, Issue 1, 2013.
    [This is the journal version of the POST 2012 paper.]
  10. Monitoring of Temporal First-order Properties with Aggregations
    David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zalinescu
    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".]
  11. Monitoring Compliance Policies over Incomplete and Disagreeing Logs
    David Basin, Felix Klaedtke, Srdjan Marinovic, and Eugen Zalinescu
    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.]
  12. Enforceable Security Policies Revisited
    David Basin, Felix Klaedtke, Vincent Juge, and Eugen Zalinescu
    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.]
  13. MONPOLY: Monitoring Usage-control Policies
    David Basin, Felix Klaedtke, Matus Harvan, and Eugen Zalinescu
    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.]
  14. Algorithms for Monitoring Real-time Properties
    David Basin, Felix Klaedtke, and Eugen Zalinescu
    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.]
  15. Monitoring Usage-control Policies in Distributed Systems
    David Basin, Felix Klaedtke, Matus Harvan, and Eugen Zalinescu
    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.]
  16. Policy Monitoring in First-Order Temporal Logic
    David Basin, Felix Klaedtke, and Samuel Müller
    In the Proceedings of the 22nd International Conference on Computer Aided Verification (CAV 2010).
    [This is an invited paper that presents our monitoring approach.]
  17. Monitoring Security Policies with Metric First-order Temporal Logic
    David Basin, Felix Klaedtke, and Samuel Müller
    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.]
  18. Runtime Monitoring of Metric First-order Temporal Properties
    David Basin, Felix Klaedtke, Samuel Müller, and Birgit Pfitzmann
    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.]
 
Page URL: http://www.infsec.ethz.ch/research/projects/mon_enf.html
31.03.2015
© 2015 Eidgenössische Technische Hochschule Zürich