Abstract
An extension of the λ-calculus is proposed, to study history-based access control. It allows for security policies with a possibly nested, local scope. We define a type and effect system that, given a program, extracts a history expression, i.e. a correct approximation to the set of histories obtainable at run-time. Validity of history expressions is non-regular, because the scope of policies can be nested. Nevertheless, a transformation of history expressions is presented, that makes verification possible through standard model checking techniques. A program will never fail at run-time if its history expression, extracted at compile-time, is valid.
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
Abadi, M., Fournet, C.: Access control based on execution history. In: Proc. 10th Annual Network and Distributed System Security Symposium (2003)
Banerjee, A., Naumann, D.A.: History-based access control and secure information flow. In: Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Cards (CASSIS) (2004)
Bartoletti, M.: PhD thesis, Università di Pisa (submitted)
Bartoletti, M., Degano, P., Ferrari, G.L.: Method inlining in the presence of stack inspection. In: Workshop on Issues in the Theory of Security (2004)
Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoretical Computer Science 37, 77–121 (1985)
Besson, F., Jensen, T., Le Métayer, D., Thorn, T.: Model checking security properties of control flow graphs. Journal of Computer Security 9, 217–250 (2001)
Colcombet, T., Fradet, P.: Enforcing trace properties by program transformation. In: Proc. 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2000)
Edjlali, G., Acharya, A., Chaudhary, V.: History-based access control for mobile code. In: Vitek, J. (ed.) Secure Internet Programming. LNCS, vol. 1603. Springer, Heidelberg (1999)
Esparza, J.: On the decidability of model checking for several μ-calculi and Petri nets. In: Proc. 19th Int. Colloquium on Trees in Algebra and Programming (1994)
Fong, P.W.: Access control by tracking shallow execution history. In: IEEE Symposium on Security and Privacy (2004)
Fournet, C., Gordon, A.D.: Stack inspection: theory and variants. ACM Transactions on Programming Languages and Systems 25(3), 360–399 (2003)
Igarashi, A., Kobayashi, N.: Resource usage analysis. In: Proc. 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2002)
Marriott, K., Stuckey, P.J., Sulzmann, M.: Resource usage verification. In: Proc. First Asian Programming Languages Symposium (2003)
Sabelfeld, A., Myers, A.C.: Language-based information flow security. IEEE Journal on selected areas in communication 21(1) (2003)
Samarati, P., de Capitani di Vimercati, S.: Access control: Policies, models, and mechanisms. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, p. 137. Springer, Heidelberg (2001)
Schneider, F., Morrisett, G., Harper, R.: A language-based approach to security. In: Informatics: 10 Years Back, 10 Years Ahead. Springer, Heidelberg (2001)
Schneider, F.B.: Enforceable security policies. ACM Transactions on Information and System Security (TISSEC) 3(1), 30–50 (2000)
Skalka, C., Smith, S.: History effects and verification. In: Asian Programming Languages Symposium (2004)
Talpin, J.-P., Jouvelot, P.: The type and effect discipline. In: Proc. 7th IEEE Symposium on Logic in Computer Science (1992)
Tan, G., Ou, X., Walker, D.: Resource usage analysis via scoped methods. In: Foundations of Object-Oriented Languages (2003)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Proc. Banff Higher order workshop conference on Logics for concurrency (1996)
Walker, D.: A type system for expressive security policies. In: Proc. 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bartoletti, M., Degano, P., Ferrari, G.L. (2005). History-Based Access Control with Local Policies. In: Sassone, V. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2005. Lecture Notes in Computer Science, vol 3441. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31982-5_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-31982-5_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25388-4
Online ISBN: 978-3-540-31982-5
eBook Packages: Computer ScienceComputer Science (R0)