More Web Proxy on the site http://driver.im/

research-article

Monitoring security policies with metric first-order temporal logic

Authors:

Felix Klaedtke,

Samuel MüllerAuthors Info & Claims

SACMAT '10: Proceedings of the 15th ACM symposium on Access control models and technologies

Pages 23 - 34

https://doi.org/10.1145/1809842.1809849

Published: 11 June 2010 Publication History

Abstract

We show the practical feasibility of monitoring complex security properties using a runtime monitoring approach for metric first-order temporal logic. In particular, we show how a wide variety of security policies can be naturally formalized in this expressive logic, ranging from traditional policies like Chinese Wall and separation of duty to more specialized usage-control and compliance requirements. We also explain how these formalizations can be directly used for monitoring and experimentally evaluate the performance of the resulting monitors.

References

[1]

Bank Secrecy Act of 1970, 1970. 31 USC 5311-5332 and 31 CFR 103.

[2]

The Health Insurance Portability and Accountability Act of 1996 (HIPAA), 1996. Public Law 104-191.

[3]

USA Patriot Act of 2001, 2001. Public Law 107-56, HR 3162 RDS.

[4]

S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases: The Logical Level. Addison Wesley, 1994.

Digital Library

[5]

B. Alpern and F. B. Schneider. Defining liveness. Inform. Process. Lett., 21(4):181--185, 1985.

[6]

R. Alur and T. A. Henzinger. Logics and models of real time: A survey. In Proceedings of the REX Workshop on Real Time: Theory in Practice, volume 600 of Lect. Notes Comput. Sci., pages 74--106, 1992.

Digital Library

[7]

H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Rule-based runtime verification. In Proceedings of the 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI '04), volume 2937 of Lect. Notes Comput. Sci., pages 44--57, 2004.

[8]

A. Barth, A. Datta, J. C. Mitchell, and H. Nissenbaum. Privacy and contextual integrity: Framework and applications. In Proceedings of the 2006 IEEE Symposium on Security and Privacy, pages 184--198, 2006.

Digital Library

[9]

D. Basin, F. Klaedtke, S. Muller, and B. Pfitzmann. Runtime monitoring of metric first-order temporal properties. In Proceedings of the 28th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS '08), Dagstuhl Seminar Proceedings, pages 49--60, 2008.

[10]

A. Bauer, M. Leucker, and C. Schallhart. Monitoring of real-time properties. In Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS '06), volume 4337 of Lect. Notes Comput. Sci., pages 260--272, 2006.

Digital Library

[11]

E. Bertino, C. Bettini, E. Ferrari, and P. Samarati. An access control model supportting periodicity and temporal reasoning. ACM Trans. Database Syst., 23(3):231--285, 1998.

Digital Library

[12]

C. Bettini, S. Jajodia, X. S. Wang, and D. Wijesekera. Provisions and obligations in policy rule management. J. Netw. Syst. Manage., 11(3):351--372, 2003.

Digital Library

[13]

D. F. Brewer and M. J. Nash. The Chinese Wall security policy. In Proceedings of the 1989 IEEE Symposium on Security and Privacy, pages 206--214, 1989.

[14]

J. Chomicki. Efficient checking of temporal integrity constraints using bounded history encoding. ACM Trans. Database Syst., 20(2):149--186, 1995.

Digital Library

[15]

B. D'Angelo, S. Sankaranarayanan, C. Sanchez, W. Robinson, B. Finkbeiner, H. B. Sipma, S. Mehrotra, and Z. Manna. LOLA: Runtime monitoring of synchronous systems. In Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME '05), pages 166--174, 2005.

Digital Library

[16]

N. Dinesh, A. Joshi, I. Lee, and O. Sokolsky. Checking traces for regulatory conformance. In Proceedings of the 8th Workshop on Runtime Verification (RV '08), volume 5289 of Lect. Notes Comput. Sci., pages 86--103, 2008.

Digital Library

[17]

D. F. Ferraiolo, R. S. Sandhu, S. I. Gavrila, D. R. Kuhn, and R. Chandramouli. Proposed NIST standard for role-based access control. ACM Trans. Inform. Syst. Secur., 4(3):224--274, 2001.

Digital Library

[18]

C. Giblin, A. Y. Liu, S. Muller, B. Pfitzmann, and X. Zhou. Regulations expressed as logical models (REALM). In Proceedings of the 18th Annual Conference on Legal Knowledge and Information Systems (JURIX '05), volume 134 of Frontiers Artifificial Intelligence Appl., pages 37--48, 2005.

Digital Library

[19]

S. Halle and R. Villemaire. Browser-based enforcement of interface contracts in web applications with BeepBeep. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV '09), volume 5643 of Lect. Notes Comput. Sci., pages 648--653, 2009.

Digital Library

[20]

K. Havelund and G. Rosu. Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Trans., 6(2):158--173, 2004.

Digital Library

[21]

M. Hilty, D. Basin, and A. Pretschner. On obligations. In Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS '05), volume 3679 of Lect. Notes Comput. Sci., pages 98--117, 2005.

Digital Library

[22]

S. Jajodia, P. Samarati, and V. S. Subrahmanian. A logical language for expressing authorizations. In Proceedings of the 1997 IEEE Symposium on Security and Privacy, pages 31--42, 1997.

Digital Library

[23]

H. Janicke, A. Cau, F. Siewe, and H. Zedan. Deriving enforcement mechanisms from polices. In Proceedings of the 8th IEEE International Workshop for Policies for Distributed Systems and Networks (POLICY '07), pages 161--172, 2007.

Digital Library

[24]

H. Janicke, A. Cau, and H. Zedan. A note on the formalisation of UCON. In Proceedings of the 12th ACM Symposium on Access Control Models and Technologies (SACMAT '07), pages 163--168, 2007.

Digital Library

[25]

R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255--299, 1990.

Digital Library

[26]

A. M. Law. Simulation, Modeling & Analysis. McGraw-Hill, 4th edition, 2007.

[27]

J. Ligatti, L. Bauer, and D. Walker. Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur., 4(1-2):2--16, 2005.

Digital Library

[28]

S. Muller. Theory and Applications of Runtime Monitoring Metric First-order Temporal Logic. PhD thesis, Swiss Federal Institute of Technology (ETH) Zurich, 2009.

[29]

D. Nickovic and O. Maler. AMT: A property-based monitoring tool for analog systems. In Proceedings of the 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS '07), volume 4763 of Lect. Notes Comput. Sci., pages 304--319, 2007.

Digital Library

[30]

A. Pretschner, M. Hilty, and D. Basin. Distributed usage control. Commun. ACM, 49:39--44, 2006.

Digital Library

[31]

C. Ribeiro, A. Zuquete, P. Ferreira, and P. Guedes. SPL: An access control language for security policies with complex constraints. In Proceedings of the Network and Distributed System Security Symposium (NDSS '01), 2001.

[32]

M. Roger and J. Goubault-Larrecq. Log auditing through model-checking. In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW '01), pages 220--234, 2001.

Digital Library

[33]

F. B. Schneider. Enforceable security policies. ACM Trans. Inform. Syst. Secur., 3(1):30--50, 2000.

Digital Library

[34]

F. Siewe, A. Cau, and H. Zedan. A compositional framework for access control policies enforcement. In Proceedings of the 2003 ACM Workshop on Formal Methods in Security Engineering (FMSE '03), pages 32--42, 2003.

Digital Library

[35]

A. P. Sistla and O. Wolfson. Temporal triggers in active databases. IEEE Trans. Knowl. Data Eng., 7(3):471--486, 1995.

Digital Library

[36]

O. Sokolsky, U. Sammapun, I. Lee, and J. Kim. Run-time checking of dynamic properties. Elec. Notes Theo. Comput. Sci., 144(4):91--108, 2006.

Digital Library

[37]

P. Thati and G. Rosu. Monitoring algorithms for metric temporal logic specifications. Elec. Notes Theo. Comput. Sci., 113:145--162, 2005.

Digital Library

[38]

X. Zhang, F. Parisi-Presicce, R. Sandhu, and J. Park. Formal model and policy specification of usage control. ACM Trans. Inform. Syst. Secur., 8(4):351--387, 2005.

Digital Library

Cited By

Basin DDebois SHildebrandt T(2024)Proactive enforcement of provisions and obligationsJournal of Computer Security10.3233/JCS-21007832:3(247-289)Online publication date: 17-Jun-2024
https://doi.org/10.3233/JCS-210078
Ganguly RXue YJonckheere ALjung PSchornstein BBonakdarpour BHerlihy M(2024)Distributed runtime verification of metric temporal propertiesJournal of Parallel and Distributed Computing10.1016/j.jpdc.2023.104801185:COnline publication date: 4-Mar-2024
https://dl.acm.org/doi/10.1016/j.jpdc.2023.104801
Brechelmacher ONičković DNießen TSallinger SWeissenbacher G(2024)Differential Property Monitoring for Backdoor DetectionFormal Methods and Software Engineering10.1007/978-981-96-0617-7_13(216-236)Online publication date: 29-Nov-2024
https://doi.org/10.1007/978-981-96-0617-7_13
Show More Cited By

Index Terms

Monitoring security policies with metric first-order temporal logic
1. Information systems
  1. Data management systems
    1. Middleware for databases
      1. Distributed transaction monitors
2. Software and its engineering

Recommendations

Enforceable Security Policies Revisited

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 ...
A decidable first-order logic for medical reasoning
KES'11: Proceedings of the 15th international conference on Knowledge-based and intelligent information and engineering systems - Volume Part II

This paper is intended to construct a decidable first-order logic for appropriately expressing medical reasoning which may require to express not only time-dependency, paraconsistency, constructiveness, resource-sensitivity, but also order-sensitivity. ...
Dynamic Security Policies Enforcement and Adaptation Using Aspects
TRUSTCOM '15: Proceedings of the 2015 IEEE Trustcom/BigDataSE/ISPA - Volume 01

Enforcing access and usage control requirements, like permissions and obligations, to govern distributed systems is a complex and error-prone task and notably hard to implement. In this paper, we claim that various enforcement modes are needed to obtain ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SACMAT '10: Proceedings of the 15th ACM symposium on Access control models and technologies

June 2010

212 pages

ISBN:9781450300490

DOI:10.1145/1809842

General Chair:
James Joshi
University of Pittsburgh, USA
,
Program Chair:
Barbara Carminati
University of Insubria, Italy

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 June 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SACMAT'10

Sponsor:

SIGSAC

SACMAT'10: 15th ACM Symposium on Access Control Models and Technologies

June 9 - 11, 2010

Pennsylvania, Pittsburgh, USA

Acceptance Rates

Overall Acceptance Rate 177 of 597 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

43
Total Citations
View Citations
698
Total Downloads

Downloads (Last 12 months)15
Downloads (Last 6 weeks)0

Reflects downloads up to 03 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Basin DDebois SHildebrandt T(2024)Proactive enforcement of provisions and obligationsJournal of Computer Security10.3233/JCS-21007832:3(247-289)Online publication date: 17-Jun-2024
https://doi.org/10.3233/JCS-210078
Ganguly RXue YJonckheere ALjung PSchornstein BBonakdarpour BHerlihy M(2024)Distributed runtime verification of metric temporal propertiesJournal of Parallel and Distributed Computing10.1016/j.jpdc.2023.104801185:COnline publication date: 4-Mar-2024
https://dl.acm.org/doi/10.1016/j.jpdc.2023.104801
Brechelmacher ONičković DNießen TSallinger SWeissenbacher G(2024)Differential Property Monitoring for Backdoor DetectionFormal Methods and Software Engineering10.1007/978-981-96-0617-7_13(216-236)Online publication date: 29-Nov-2024
https://doi.org/10.1007/978-981-96-0617-7_13
Lima LHuerta y Munive JTraytel D(2024)Explainable Online Monitoring of Metric First-Order Temporal LogicTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57246-3_16(288-307)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57246-3_16
Zuckmantel TZhou YDüdder BHildebrandt TZhou YChrysanthis PGulisano V(2022)Event-based data-centric semantics for consistent data management in microservicesProceedings of the 16th ACM International Conference on Distributed and Event-Based Systems10.1145/3524860.3539807(97-102)Online publication date: 27-Jun-2022
https://dl.acm.org/doi/10.1145/3524860.3539807
Skandylas CKhakpour N(2021)Design and Implementation of Self-Protecting systems: A Formal ApproachFuture Generation Computer Systems10.1016/j.future.2020.09.005115(421-437)Online publication date: Feb-2021
https://doi.org/10.1016/j.future.2020.09.005
Saniei R(2021)Challenges in the Implementation of Privacy Enhancing Semantic Technologies (PESTs) Supporting GDPRAI Approaches to the Complexity of Legal Systems XI-XII10.1007/978-3-030-89811-3_20(283-297)Online publication date: 27-Nov-2021
https://doi.org/10.1007/978-3-030-89811-3_20
Zeller SKhakpour NWeyns DDeogun DHoniden SNitto ECalinescu R(2020)Self-protection against business logic vulnerabilitiesProceedings of the IEEE/ACM 15th International Symposium on Software Engineering for Adaptive and Self-Managing Systems10.1145/3387939.3391609(174-180)Online publication date: 29-Jun-2020
https://dl.acm.org/doi/10.1145/3387939.3391609
Shvartzshnaider YPavlinovic ZBalashankar AWies TSubramanian LNissenbaum HMittal P(2019)VACCINE: Using Contextual Integrity For Data Leakage DetectionThe World Wide Web Conference10.1145/3308558.3313655(1702-1712)Online publication date: 13-May-2019
https://dl.acm.org/doi/10.1145/3308558.3313655
Arfelt EBasin DDebois S(2019)Monitoring the GDPRComputer Security – ESORICS 201910.1007/978-3-030-29959-0_33(681-699)Online publication date: 15-Sep-2019
https://doi.org/10.1007/978-3-030-29959-0_33
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents