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

research-article

Enforceable Security Policies Revisited

Authors:

Felix Klaedtke,

Eugen ZălinescuAuthors Info & Claims

ACM Transactions on Information and System Security (TISSEC), Volume 16, Issue 1

Article No.: 3, Pages 1 - 26

https://doi.org/10.1145/2487222.2487225

Published: 01 June 2013 Publication History

Abstract

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, that is, the enforcement mechanism sees them but cannot prevent their execution. For this refined setting, we give necessary and sufficient conditions on when a security policy is enforceable. To state these conditions, we generalize the standard notion of safety properties. Our classification of system actions also allows one, for example, to reason about the enforceability of policies that involve timing constraints. Furthermore, for different specification languages, we investigate the decision problem of whether a given policy is enforceable. We provide complexity results and show how to synthesize an enforcement mechanism from an enforceable policy.

References

[1]

Alpern, B. and Schneider, F. B. 1985. Defining liveness. Inf. Process. Lett. 21, 4, 181--185.

[2]

Alur, R. and Henzinger, T. A. 1992. Logics and models of real time: A survey. In Proceedings of the REX Workshop on Real-Time: Theory in Practice. Lecture Notes in Computer Science, vol. 600, Springer, 74--106.

Digital Library

[3]

Alur, R. and Henzinger, T. A. 1994. A really temporal logic. J. ACM 41, 1, 181--203.

Digital Library

[4]

American National Standards Institute, Inc. 2004. Role Based Access Control. American National Standards Institute, Inc., Washington, DC.

[5]

Barringer, H., Goldberg, A., Havelund, K., and Sen, K. 2004. Rule-based runtime verification. In Proceedings of the 5th International Conference on Verification, Model Checking and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2937, Springer, 44--57.

[6]

Basin, D., Olderog, E.-R., and Sevinç, P. E. 2007. Specifying and analyzing security automata using CSP-OZ. In Proceedings of the ACM Symposium on Information, Computer and Communications Security. ACM Press, New York, 70--81.

Digital Library

[7]

Basin, D., Klaedtke, F., Müller, S., and Pfitzmann, B. 2008. Runtime monitoring of metric first-order temporal properties. In Proceedings of the 28th Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics Series, vol. 2, Schloss Dagstuhl - Leibniz Center for Informatics, 49--60.

[8]

Basin, D., Klaedtke, F., and Müller, S. 2010. Monitoring security policies with metric first-order temporal logic. In Proceedings of the 15th ACM Symposium on Access Control Models and Technologies. ACM Press, New York, 23--33.

Digital Library

[9]

Basin, D., Harvan, M., Klaedtke, F., and Zălinescu, E. 2011. Monitoring usage-control policies in distributed systems. In Proceedings of the 18th International Symposium on Temporal Representation and Reasoning. IEEE Computer Society, 88--95.

Digital Library

[10]

Basin, D., Jugé, V., Klaedtke, F., and Zălinescu, E. 2012a. Enforceable security policies revisited. In Proceedings of the 1st Conference on Principles of Security and Trust. Lecture Notes in Computer Science, vol. 7215, Springer, 309--328.

Digital Library

[11]

Basin, D., Klaedtke, F., and Zălinescu, E. 2012b. Algorithms for monitoring real-time properties. In Proceedings of the 2nd International Conference on Runtime Verification. Lecture Notes in Computer Science, vol. 7186, Springer, 260--275.

Digital Library

[12]

Benveniste, A. and Berry, G. 1991. The synchronous approach to reactive and real-time systems. Proc. IEEE 79, 9, 1270--1282.

[13]

Chabot, H., Khoury, R., and Tawbi, N. 2011. Extending the enforcement power of truncation monitors using static analysis. Comput. Secur. 30, 4, 194--207.

Digital Library

[14]

Chang, E. Y., Manna, Z., and Pnueli, A. 1992. Characterization of temporal property classes. In Proceedings of the 19th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 623, Springer, 474--486.

Digital Library

[15]

Clarke, E. M., Emerson, E. A., and Sifakis, J. 2007. Model checking: Algorithmic verification and debugging. Comm. ACM 52, 11, 75--84.

Digital Library

[16]

Clarkson, M. R. and Schneider, F. B. 2010. Hyperproperties. J. Comput. Secur. 18, 6, 1157--1210.

[17]

Dax, C., Klaedtke, F., and Lange, M. 2010. On regular temporal logics with past. Acta Inf. 47, 4, 251--277.

Digital Library

[18]

Ehlers, R. and Finkbeiner, B. 2011. Reactive safety. In Proceedings of 2nd International Symposium on Games, Logics and Formal Verification. Electronic Proceedings in Theoretical Computer Science, vol. 54, 178--191.

[19]

Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., and Van Campenhout, D. 2003. Reasoning with temporal logic on truncated paths. In Proceedings of the 15th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 2725, Springer, 27--39.

[20]

Erlingsson, Ú. 2004. The inlined reference monitor approach to security policy enforcement. Ph.D. thesis, Cornell University, Ithaca, NY.

Digital Library

[21]

Erlingsson, Ú. and Schneider, F. B. 1999. SASI enforcement of security policies: A retrospective. In Proceedings of the Workshop on New Security Paradigms. ACM Press, New York, 87--95.

Digital Library

[22]

Erlingsson, Ú. and Schneider, F. B. 2000. IRM enforcement of Java stack inspection. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 246--255.

Digital Library

[23]

Falcone, Y., Mounier, L., Fernandez, J.-C., and Richier, J.-L. 2011. Runtime enforcement monitors: Composition, synthesis, and enforcement abilities. Form. Methods Syst. Des. 38, 2, 223--262.

Digital Library

[24]

Fong, P. W. 2004. Access control by tracking shallow execution history. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 43--55.

[25]

Garg, D., Jia, L., and Datta, A. 2011. Policy auditing over incomplete logs: Theory, implementation and applications. In Proceedings of the 18th ACM Conference on Computer and Communications Security. ACM Press, New York, 151--162.

Digital Library

[26]

Hallé, S. and Villemaire, R. 2012. Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5, 2, 192--206.

Digital Library

[27]

Hamlen, K. W., Morrisett, G., and Schneider, F. B. 2006. Computability classes for enforcement mechanisms. ACM Trans. Progr. Lang. Syst. 28, 1, 175--205.

Digital Library

[28]

Havelund, K. 2000. Using runtime analysis to guide model checking of java programs. In Proceedings of the 7th International SPIN Workshop. Lecture Notes in Computer Science, vol. 1885, Springer, 245--264.

Digital Library

[29]

Havelund, K. and Roşu, G. 2001. Monitoring programs using rewriting. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering. IEEE Computer Society, 135--143.

Digital Library

[30]

Henzinger, T. A. 1992. Sooner is safer than later. Inform. Process. Lett. 43, 3, 135--141.

Digital Library

[31]

Hopcroft, J. E. 1971. An n log n algorithm for minimizing the states in a finite automaton. In Proceedings of the International Symposium on Theory of Machines and Computations. Z. Kohavi and A. Paz Eds., Academic Press, 189--196.

[32]

Hopcroft, J. E. and Ullman, J. D. 1979. Introduction to Automata Theory, Languages and Computation. Addison-Wesley Longman, Boston, MA.

Digital Library

[33]

Jones, N. D. 1975. Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11, 1, 68--85.

Digital Library

[34]

Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., and Sokolsky, O. 1999. Formally specified monitoring of temporal properties. In Proceedings of the 11th Euromicro Conference on Real-Time Systems. IEEE Computer Society, 114--122.

[35]

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

Digital Library

[36]

Lamport, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Engin. 3, 2, 125--143.

Digital Library

[37]

Ligatti, J. and Reddy, S. 2010. A theory of runtime enforcement, with results. In Proceedings of the 15th European Symposium on Research in Computer Security. Lecture Notes in Computer Science, vol. 6345. Springer, 87--100.

Digital Library

[38]

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

Digital Library

[39]

Ligatti, J., Bauer, L., and Walker, D. 2009. Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur. 12, 3.

Digital Library

[40]

McNaughton, R. and Papert, S. 1971. Counter-Free Automata. Research Monograph Series, vol. 65, The MIT Press, Cambridge, MA.

Digital Library

[41]

Paul, M., Siegert, H. J., Alford, M. W., Ansart, J. P., Hommel, G., Lamport, L., Liskov, B., Mullery, G. P., and Schneider, F. B. 1985. Distributed Systems: Methods and Tools for Specification: An Advanced Course. Lecture Notes in Computer Science, vol. 190, Springer.

Digital Library

[42]

Pnueli, A. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science. IEEE Computer Society, 46--57.

Digital Library

[43]

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

Digital Library

[44]

Rabin, M. O. and Scott, D. 1959. Finite automata and their decision problems. IBM J. Res. Dev. 3, 2, 114--125.

Digital Library

[45]

Ramadge, P. J. and Wonham, W. M. 1987. Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25, 1, 206--230.

Digital Library

[46]

Schneider, F. B. 2000. Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3, 1, 30--50.

Digital Library

[47]

Sistla, A. P. and Clarke, E. M. 1985. The complexity of propositional linear temporal logic. J. ACM 32, 3, 733--749.

Digital Library

[48]

Talhi, C., Tawbi, N., and Debbabi, M. 2008. Execution monitoring enforcement under memory-limitation constraints. Inf. Comput. 206, 2--4, 158--184.

Digital Library

[49]

Vardi, M. Y. 1995. An automata-theoretic approach to linear temporal logic. In Proceedings of the 8th Banff Higher Order Workshop on Logics for Concurrency: Structure Versus Automata. Lecture Notes in Computer Science, vol. 1043, Springer, 238--266.

Digital Library

[50]

Vardi, M. Y. 2007. Automata-theoretic model checking revisited. In Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 4349, Springer, 137--150.

Digital Library

[51]

Vardi, M. Y. and Wolper, P. 1994. Reasoning about infinite computations. Inf. Comput. 115, 1, 1--37.

Digital Library

[52]

Viswanathan, M. 2000. Foundations for the run-time analysis of software systems. Ph.D. thesis, University of Pennsylvania, Philadelphia, PA.

Digital Library

Cited By

Cimmino ACano-Benito JGarcía-Castro R(2025)Open Digital Rights Enforcement framework (ODRE): From descriptive to enforceable policiesComputers & Security10.1016/j.cose.2024.104282150(104282)Online publication date: Mar-2025
https://doi.org/10.1016/j.cose.2024.104282
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
Gehring MMantel H(2024)Towards a More Sustainable Re-engineering of Heterogeneous Distributed Systems Using Cooperating Run-Time MonitorsLeveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies10.1007/978-3-031-75387-9_9(132-152)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75387-9_9
Show More Cited By

Index Terms

Enforceable Security Policies Revisited

Recommendations

Run-Time Enforcement of Nonsafety Policies

A common mechanism for ensuring that software behaves securely is to monitor programs at run time and check that they dynamically adhere to constraints specified by a security policy. Whenever a program monitor detects that untrusted software is ...
Security policies for downgrading
CCS '04: Proceedings of the 11th ACM conference on Computer and communications security

A long-standing problem in information security is how to specify and enforce expressive security policies that control information flow while also permitting information release (i.e., declassification) where appropriate. This paper presents security ...
Enforceable security policies

A precise characterization is given for the class of security policies enforceable with mechanisms that work by monitoring system execution, and automata are introduced for specifying exactly that class of security policies. Techniques to enforce ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Information and System Security

ACM Transactions on Information and System Security Volume 16, Issue 1

June 2013

113 pages

ISSN:1094-9224

EISSN:1557-7406

DOI:10.1145/2487222

Issue’s Table of Contents

Copyright © 2013 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 June 2013

Accepted: 01 February 2013

Revised: 01 December 2012

Received: 01 June 2012

Published in TISSEC Volume 16, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Google

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

46
Total Citations
View Citations
1,013
Total Downloads

Downloads (Last 12 months)20
Downloads (Last 6 weeks)1

Reflects downloads up to 26 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Cimmino ACano-Benito JGarcía-Castro R(2025)Open Digital Rights Enforcement framework (ODRE): From descriptive to enforceable policiesComputers & Security10.1016/j.cose.2024.104282150(104282)Online publication date: Mar-2025
https://doi.org/10.1016/j.cose.2024.104282
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
Gehring MMantel H(2024)Towards a More Sustainable Re-engineering of Heterogeneous Distributed Systems Using Cooperating Run-Time MonitorsLeveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies10.1007/978-3-031-75387-9_9(132-152)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75387-9_9
Hublet FLima LBasin DKrstić STraytel D(2024)Proactive Real-Time First-Order EnforcementComputer Aided Verification10.1007/978-3-031-65630-9_8(156-181)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65630-9_8
Castañeda ARodríguez GOshman RNolin AHalldorsson MBalliu A(2023)Asynchronous Wait-Free Runtime Verification and Enforcement of LinearizabilityProceedings of the 2023 ACM Symposium on Principles of Distributed Computing10.1145/3583668.3594563(90-101)Online publication date: 19-Jun-2023
https://dl.acm.org/doi/10.1145/3583668.3594563
Hublet FBasin DKrstić S(2022)Real-Time Policy Enforcement with Metric First-Order Temporal LogicComputer Security – ESORICS 202210.1007/978-3-031-17146-8_11(211-232)Online publication date: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-17146-8_11
Pinisetty SAllen NPearce HTrew MSingh Gaur MRoop P(2022) Formal Methods for the Security of Medical Devices 1 Applied Smart Health Care Informatics10.1002/9781119743187.ch3(31-65)Online publication date: 25-Feb-2022
https://doi.org/10.1002/9781119743187.ch3
Gallay FFalcone Y(2021)Decentralized LTL EnforcementElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.346.9346(135-151)Online publication date: 17-Sep-2021
https://doi.org/10.4204/EPTCS.346.9
Palombo HDolzhenko ELigatti JZheng H(2020)Stream-Monitoring AutomataProceedings of the 2020 9th International Conference on Software and Computer Applications10.1145/3384544.3384609(313-320)Online publication date: 18-Feb-2020
https://dl.acm.org/doi/10.1145/3384544.3384609
Zhang YCheng B(2020)Event Detection on Monitoring Internet of Things Services by Fusing Multiple Observations2020 IEEE International Conference on Web Services (ICWS)10.1109/ICWS49710.2020.00068(463-467)Online publication date: Oct-2020
https://doi.org/10.1109/ICWS49710.2020.00068
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 Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents