Abstract
This paper presents, to the best of our knowledge, the first formal specification of the application security model defined by the Mobile Information Device Profile 2.0 for Java 2 Micro Edition. The specification, which has been formalized in Coq, provides an abstract representation of the state of a device and the security-related events that allows to reason about the security properties of the platform where the model is deployed. We state and sketch the proof of some desirable properties of the security model. Although the abstract specification is not executable, we describe a refinement methodology that leads to an executable prototype.
This work is partially funded by the IST program of the European Commission, FET under the MOBIUS project, the INRIA-Microsoft Joint Research Laboratory, and STIC-AmSud under the ReSeCo project.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
JSR 37 Expert Group: Mobile Information Device Profile for Java 2 Micro Edition. Version 1.0. Sun Microsystems, Inc. (2000)
JSR 118 Expert Group: Mobile Information Device Profile for Java 2 Micro Edition. Version 2.0. Sun Microsystems, Inc. and Motorola, Inc. (2002)
Kolsi, O., Virtanen, T.: MIDP 2.0 security enhancements. In: Proceedings of the 37th Annual Hawaii International Conference on System Sciences, Washington, DC, USA. IEEE Computer Society, Los Alamitos (2004) 90287.3
Debbabi, M., Saleh, M., Talhi, C., Zhioua, S.: Security analysis of wireless Java. In: Proceedings of the 3rd Annual Conference on Privacy, Security and Trust (2005)
The Coq Development Team: The Coq Proof Assistant Reference Manual – Version V8.0. (2004)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science, Springer, Heidelberg (2004)
Zanella Béguelin, S.: Especificación formal del modelo de seguridad de MIDP 2.0 en el Cálculo de Construcciones Inductivas. Master’s thesis, Universidad Nacional de Rosario (2006)
Zanella Béguelin, S., Betarte, G., Luna, C.: A formal specification of the MIDP 2.0 security model. Technical Report 06-09, Instituto de Computación, Facultad de Ingeniería, Universidad de la República, Uruguay (2006)
Spivey, J.M.: The Z Notation: A Reference Manual. In: International Series in Computer Science, Prentice Hall, Hemel Hempstead, Hertfordshire, UK (1989)
Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. In: Graduate Texts in Computer Science, Springer, Heidelberg (1998)
Morgan, C.: Programming from specifications. Prentice-Hall Inc., Upper Saddle River (1990)
Besson, F., Dufay, G., Jensen, T.: A formal model of access control for mobile interactive devices. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, Springer, Heidelberg (2006) (to appear)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zanella Béguelin, S., Betarte, G., Luna, C. (2007). A Formal Specification of the MIDP 2.0 Security Model. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds) Formal Aspects in Security and Trust. FAST 2006. Lecture Notes in Computer Science, vol 4691. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75227-1_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-75227-1_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75226-4
Online ISBN: 978-3-540-75227-1
eBook Packages: Computer ScienceComputer Science (R0)