The Community for Technology Leaders
RSS Icon
Issue No.10 - Oct. (2013 vol.39)
pp: 1403-1426
David Basin , ETH Zurich, Zurich
Matus Harvan , ETH Zurich, Zurich
Felix Klaedtke , ETH Zurich, Zurich
Eugen Zalinescu , ETH Zurich, Zurich
IT systems manage increasing amounts of sensitive data and there is a growing concern that they comply with policies that regulate data usage. In this paper, we use temporal logic to express policies and runtime monitoring to check system compliance. While well-established methods for monitoring linearly ordered system behavior exist, a major challenge is monitoring distributed and concurrent systems where actions are locally observed in the different system parts. These observations can only be partially ordered, while policy compliance may depend on the actions' actual order of appearance. Technically speaking, it is in general intractable to check compliance of partially ordered traces. We identify fragments of our policy specification language for which compliance can be checked efficiently, namely, by monitoring a single representative trace in which the observed actions are totally ordered. Through a case study we show that the fragments are capable of expressing nontrivial policies and that monitoring representative traces is feasible on real-world data.
regulation, Monitors, temporal logic, verification, distributed systems,
David Basin, Matus Harvan, Felix Klaedtke, Eugen Zalinescu, "Monitoring Data Usage in Distributed Systems", IEEE Transactions on Software Engineering, vol.39, no. 10, pp. 1403-1426, Oct. 2013, doi:10.1109/TSE.2013.18
[1] D. Basin, M. Harvan, F. Klaedtke, and E. Zălinescu, "Monitoring Usage-Control Policies in Distributed Systems," Proc. 18th Int'l Symp. Temporal Representation and Reasoning, pp. 88-95, 2011.
[2] "The Health Insurance Portability and Accountability Act of 1996 (HIPAA)," 104th Congress, Public Law 104-191, 1996.
[3] "Sarbanes-Oxley Act of 2002,"  107th Congress, Public Law 107-204, 2002.
[4] "Directive 95/46/EC of the European Parliament and of the Council of 24 October 1995 on the Protection of Individuals with Regard to the Processing of Personal Data and on the Free Movement of Such Data," 1995.
[5] M. Roger and J. Goubault-Larrecq, "Log Auditing through Model-Checking," Proc. IEEE CS 14th Foundations Workshop, pp. 220-234, 2001.
[6] N. Dinesh, A.K. Joshi, I. Lee, and O. Sokolsky, "Checking Traces for Regulatory Conformance," Proc. Eigth Int'l Workshop Runtime Verification, pp. 86-103, 2008.
[7] A. Groce, K. Havelund, and M. Smith, "From Scripts to Specification: The Evaluation of a Flight Testing Effort," Proc. ACM/IEEE 32nd Int'l Conf. Software Eng., pp. 129-138, 2010.
[8] H. Barringer, A. Groce, K. Havelund, and M. Smith, "Formal Analysis of Log Files," J. Aerospace Computing, Information, and Comm., vol. 7, pp. 365-390, 2010.
[9] S. Hallé and R. Villemaire, "Runtime Enforcement of Web Service Message Contracts with Data," IEEE Trans. Services Computing, vol. 5, no. 2, pp. 192-206, Apr.-June 2012.
[10] D. Basin, F. Klaedtke, S. Müller, and B. Pfitzmann, "Runtime Monitoring of Metric First-Order Temporal Properties," Proc. 28th IARCS Ann. Conf. Foundations of Software Technology and Theoretical Computer Science, pp. 49-60, 2008.
[11] A.S. Tanenbaum and M. van Steen, Distributed Systems: Principles and Paradigms. Prentice Hall, 2002.
[12] A. Pnueli, "The Temporal Logic of Programs," Proc. 18th Ann. Symp. Foundations of Computer Science, pp. 46-57, 1977.
[13] R. Alur and T.A. Henzinger, "Logics and Models of Real Time: A Survey," Proc. REX Workshop Real Time: Theory in Practice, pp. 74-106, 1991.
[14] D. Basin, M. Harvan, F. Klaedtke, and E. Zălinescu, "MONPOLY: Monitoring Usage-Control Policies," Proc. Second Int'l Conf. Runtime Verification, pp. 360-364, 2012.
[15] D. Basin, F. Klaedtke, and S. Müller, "Monitoring Security Policies with Metric First-Order Temporal Logic," Proc. 15th ACM Symp. Access Control Models and Technologies, pp. 23-34, 2010.
[16] I. Aad and V. Niemi, "NRC Data Collection Campaign and the Privacy by Design Principles," Proc. Int'l Workshop Sensing for App Phones, 2010.
[17] S. Abiteboul, R. Hull, and V. Vianu, Foundations of Databases: The Logical Level. Addison Wesley, 1994.
[18] T. Massart, C. Meuter, and L. Van Begin, "On the Complexity of Partial Order Trace Model Checking," Information Processing Letters, vol. 106, no. 3, pp. 120-126, 2008.
[19] A. Genon, T. Massart, and C. Meuter, "Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces," Proc. 14th Int'l Symp. Formal Methods, pp. 557-572, 2006.
[20] C.M. Chase and V.K. Garg, "Detection of Global Predicates: Techniques and Their Limitations," Distributed Computing, vol. 11, pp. 191-201, 1998.
[21] L. Lamport, "What Good Is Temporal Logic?" Proc. IFIP Ninth World Computer Congress, pp. 657-668, 1983.
[22] J. Chomicki, "Efficient Checking of Temporal Integrity Constraints Using Bounded History Encoding," ACM Trans. Database Systems, vol. 20, no. 2, pp. 149-186, 1995.
[23] A. Goodloe and L. Pike, "Monitoring Distributed Real-Time Systems: A Survey and Future Directions," Technical Report NASA/CR-2010-216724, NASA Langley Research Center, July 2010.
[24] K. Sen, A. Vardhan, G. Agha, and G. Roşu, "Efficient Decentralized Monitoring of Safety in Distributed Systems," Proc. 26th Int'l Conf. Software Eng., pp. 418-427, 2004.
[25] R. Ramanujam, "Local Knowledge Assertions in a Changing World," Proc. Sixth Conf. Theoretical Aspects of Rationality and Knowledge, pp. 1-14, 1996.
[26] L. Lamport, "Time, Clocks, and the Ordering of Events in a Distributed System," Comm. ACM, vol. 21, no. 7, pp. 558-565, 1978.
[27] S. Wang, A. Ayoub, O. Sokolsky, and I. Lee, "Runtime Verification of Traces under Recording Uncertainty," Proc. Second Int'l Conf. Runtime Verification, pp. 442-456, 2012.
[28] A. Bauer and Y. Falcone, "Decentralised LTL Monitoring," Proc. 18th Int'l Symp. Formal Methods, pp. 85-100, 2012.
[29] A. Bauer, M. Leucker, and C. Schallhart, "Model-Based Runtime Analysis of Distributed Reactive Systems," Proc. Australian Software Eng. Conf., 2006.
[30] W. Zhou, O. Sokolsky, B.T. Loo, and I. Lee, "DMaC: Distributed Monitoring and Checking," Proc. Ninth Int'l Workshop Runtime Verification, pp. 184-201, 2009.
[31] V. Diekert and G. Rozenberg, eds., The Book of Traces. World Scientific Publishing Co., Inc., 1995.
[32] D. Peled, "Ten Years of Partial Order Reduction," Proc. 10th Int'l Conf. Computer Aided Verification, pp. 17-28, 1998.
[33] N. Markey and P. Schnoebelen, "Model Checking a Path," Proc. 14th Int'l Conf. Concurrency Theory, pp. 248-262, 2003.
[34] J.E. Hopcroft, R. Motwani, and J.D. Ullman, Introduction to Automata Theory, Languages, and Computation, second ed. Addison- Wesley, 2000.
276 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool