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 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.
This work was partly supported by Google Inc.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alpern, B., Schneider, F.B.: Defining liveness. Inform. Process. Lett. 21(4), 181–185 (1985)
Alur, R., Henzinger, T.A.: Logics and Models of Real Time: A Survey. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)
Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–203 (1994)
Basin, D., Harvan, M., Klaedtke, F., Zălinescu, E.: Monitoring usage-control policies in distributed systems. In: Proceedings of the 18th International Symposium on Temporal Representation and Reasoning, pp. 88–95. IEEE Computer Society (2011)
Basin, D., Klaedtke, F., Müller, S.: Monitoring security policies with metric first-order temporal logic. In: Proceedings of the 15th ACM Symposium on Access Control Models and Technologies, pp. 23–33. ACM Press (2010)
Basin, D., Olderog, E.-R., Sevinç, P.E.: Specifying and analyzing security automata using CSP-OZ. In: Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security, pp. 70–81. ACM Press (2007)
Chang, E.Y., Manna, Z., Pnueli, A.: Characterization of Temporal Property Classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 474–486. Springer, Heidelberg (1992)
Dax, C., Klaedtke, F., Lange, M.: On regular temporal logics with past. Acta Inform. 47(4), 251–277 (2010)
Ehlers, R., Finkbeiner, B.: Reactive safety. In: Proceedings of 2nd International Symposium on Games, Logics and Formal Verification. Electronic Proceedings in Theoretical Computer Science, vol. 54, pp. 178–191 (2011), eptcs.org
Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with Temporal Logic on Truncated Paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)
Erlingsson, Ú.: The inlined reference monitor approach to security policy enforcement. PhD thesis, Cornell University, Ithaca, NY, USA (2004)
Erlingsson, Ú., Schneider, F.B.: SASI enforcement of security policies: A retrospective. In: Proceedings of the 1999 Workshop on New Security Paradigms, pp. 87–95. ACM Press (1999)
Erlingsson, Ú., Schneider, F.B.: IRM enforcement of Java stack inspection. In: Proceedings of the 2000 IEEE Symposium on Security and Privacy, pp. 246–255. IEEE Computer Society (2000)
Falcone, Y., Mounier, L., Fernandez, J.-C., Richier, J.-L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Form. Methods Syst. Des. 38(2), 223–262 (2011)
Fong, P.W.: Access control by tracking shallow execution history. In: Proceedings of the 2004 IEEE Symposium on Security and Privacy, pp. 43–55. IEEE Computer Society (2004)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Company (1979)
Garg, D., Jia, L., Datta, A.: Policy auditing over incomplete logs: Theory, implementation and applications. In: Proceedings of the 18th ACM Conference on Computer and Communications Security, pp. 151–162. ACM Press (2011)
Hamlen, K.W., Morrisett, G., Schneider, F.B.: Computability classes for enforcement mechanisms. ACM Trans. Progr. Lang. Syst. 28(1), 175–205 (2006)
Henzinger, T.A.: Sooner is safer than later. Inform. Process. Lett. 43(3), 135–141 (1992)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979)
Jones, N.D.: Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11(1), 68–85 (1975)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2), 125–143 (1977)
Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. 4(1-2), 2–16 (2005)
Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM Trans. Inform. Syst. Secur. 12(3) (2009)
Ligatti, J., Reddy, S.: A Theory of Runtime Enforcement, with Results. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 87–100. Springer, Heidelberg (2010)
Paul, M., Siegert, H.J., Alford, M.W., Ansart, J.P., Hommel, G., Lamport, L., Liskov, B., Mullery, G.P., Schneider, F.B.: Distributed Systems—Methods and Tools for Specification: An Advanced Course. LNCS, vol. 190. Springer, Heidelberg (1985)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE Computer Society (1977)
Schneider, F.B.: Enforceable security policies. ACM Trans. Inform. Syst. Secur. 3(1), 30–50 (2000)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. J. ACM 32(3), 733–749 (1985)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)
Viswanathan, M.: Foundations for the run-time analysis of software systems. PhD thesis, University of Pennsylvania, Philadelphia, PA, USA (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basin, D., Jugé, V., Klaedtke, F., Zălinescu, E. (2012). Enforceable Security Policies Revisited. In: Degano, P., Guttman, J.D. (eds) Principles of Security and Trust. POST 2012. Lecture Notes in Computer Science, vol 7215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28641-4_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-28641-4_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28640-7
Online ISBN: 978-3-642-28641-4
eBook Packages: Computer ScienceComputer Science (R0)