Formal Specification and Analysis of the MIDP 3.0 Security Model

Author

Mazeikis, Gustavo ; Betarte, Gustavo ; Luna, Carlos

Author_Institution

Fac. de Ing., Univ. de la Republica, Montevideo, Uruguay

fYear

2009

fDate

10-12 Nov. 2009

Firstpage

59

Lastpage

66

Abstract

The Mobile Information Device Profile (MIDP) of the Java Platform Micro Edition (JME), provides a standard run-time environment for mobile phones and personal digital assistants. The third and latest version of MIDP introduces anew dimension in the security model of MIDP at the application level. For the second version of MIDP, Zanella, Betarte and Luna had proposed a formal specification of the security model in the Calculus of Inductive Constructions using the Coq Proof Assistant. This paper presents an extension of that formal specification that incorporates the changes introduced in the third version of MIDP. The obtained specification it is proven to preserve the security properties of the second version of MIDP and enables the research of new security properties for the version 3.0 of the profile.

Keywords

Calculus; Computer science; Formal specifications; Information security; Java; Mobile handsets; Personal digital assistants; Protection; Runtime environment; Virtual machining; Formal model; MIDP; mobile devices;

fLanguage

English

Publisher

ieee

Conference_Titel

Chilean Computer Science Society (SCCC), 2009 International Conference of the

Conference_Location

Santiago, TBD, Chile

ISSN

1522-4902

Print_ISBN

978-1-4244-7752-4

Type

conf

DOI

10.1109/SCCC.2009.18

Filename

5532412