Abstract
This paper presents an access control model for programming applications in which the access control to resources can employ user interaction to obtain the necessary permissions. This model is inspired by and improves on the Java security architecture used in Java-enabled mobile telephones. We consider access control permissions with multiplicities in order to allow to use a permission a certain number of times. An operational semantics of the model and a formal definition of what it means for an application to respect the security model is given. A static analysis which enforces the security model is defined and proved correct. A constraint solving algorithm implementing the analysis is presented.
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
Bartoletti, M., Degano, P., Ferrari, G.L.: Static analysis for stack inspection. Electronic Notes in Computer Science, 54 (2001)
Bartolett, M., Degano, P., Ferrari, G.-L.: History-based access control with local policies. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 316–332. Springer, Heidelberg (2005)
Besson, F., Jensen, T., Le Métayer, D., Thorn, T.: Model ckecking security properties of control flow graphs. Journal of Computer Security 9, 217–250 (2001)
Chander, A., Espinosa, D., Islam, N., Lee, P., Necula, G.C.: Enforcing resource bounds via static verification of dynamic checks. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 311–325. Springer, Heidelberg (2005)
Fournet, C., Gordon, A.: Stack inspection: theory and variants. In: Proceedings of the 29th ACM Symp. on Principles of Programming Languages (POPL 2002). ACM Press, New York (2002)
Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Information and Computation 173(1), 82–120 (2002)
Igarashi, A., Kobayashi, N.: Resource usage analysis. In: Proceedings of the 29th ACM Symp. on Principles of Programming Languages (POPL 2002), pp. 331–342 (2002)
Jensen, T., Le Métayer, D., Thorn, T.: Verification of control flow based security properties. In: Proceedings of the 20th IEEE Symp. on Security and Privacy, pp. 89–103. IEEE Computer Society, New York (1999)
Miné, A.: The octogon abstract domain. In: Proceedings of the 8th Working Conference On Reverse Engineering (WCRE 2001), pp. 310–320. IEEE, Los Alamitos (2001)
Necula, G.C.: Proof-carrying code. In: Jones, N.D. (ed.) Proceedings of the 24th ACM Symp. on Principles of Programming Languages (POPL 1997), Paris, France, pp. 106–119. ACM Press, New York (1997)
Pottier, F., Skalka, C., Smith, S.F.: A systematic approach to static access control. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 30–45. Springer, Heidelberg (2001)
Saltzer, J.H., Schroeder, M.D.: The protection of information in computer systems. Proceedings of the IEEE 63, 1278–1308 (1975)
Sun Microsystems, Inc., Palo Alto/CA, USA. Mobile Information Device Profile (MIDP) Specification for Java 2 Micro Edition, Version 2.0 (2002)
Tamaki, H., Sato, T.: OLD resolution with tabulation. In: Shapiro, E. (ed.) ICLP 1986. LNCS, vol. 225, pp. 84–98. Springer, Heidelberg (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Besson, F., Dufay, G., Jensen, T. (2006). A Formal Model of Access Control for Mobile Interactive Devices. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds) Computer Security – ESORICS 2006. ESORICS 2006. Lecture Notes in Computer Science, vol 4189. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11863908_8
Download citation
DOI: https://doi.org/10.1007/11863908_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44601-9
Online ISBN: 978-3-540-44605-7
eBook Packages: Computer ScienceComputer Science (R0)