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
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)