english Icono del idioma   español Icono del idioma  

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12008/3413 How to cite
Title: A Certified Access Controller for JME-MIDP 2.0 enabled Mobile Devices
Authors: Roushani Oskui, Ramin
Betarte, Gustavo
Luna, Carlos
Type: Reporte técnico
Keywords: Java Micro Edition, Calculus of Inductive Constructions, Information Integrity
Issue Date: 2008
Abstract: Mobile devices, like cell phones and PDAs, allow to store information and to establish connections with external entities. In this sort of devices it is important to guarantee confidentiality and integrity of the stored data as well as ensure service availability. The JME platform, a Java enabled technology, provides the MIDP standard that facilitates applications development and specifies a security model for the controlled access to sensitive resources of the device. This paper describes a high level formal specification of an access controller for JME-MIDP 2.0. This formal definition of the controller has been obtained as an extension of a specification, developed using the Calculus of Inductive Constructions and the proof assistant Coq, of the MIDP 2.0 security model. The paper also discusses the refinement of the specification into an executable model and describes the algorithm which has been proven to be a correct implementation of the specified access controller.
Publisher: UR. FI – INCO.
Series or collection: Reportes Técnicos 08-06
ISSN: 0797-6410
Citation: ROUSHANI OSKUI, R., BETARTE, G., LUNA, C. "A Certified Access Controller for JME-MIDP 2.0 enabled Mobile Devices". Reportes Técnicos 08-06. UR. FI – INCO, 2008.
License: Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)
Appears in Collections:Reportes Técnicos - Instituto de Computación

Files in This Item:
File Description SizeFormat  
TR0806.pdf192,38 kBAdobe PDFView/Open


This item is licensed under a Creative Commons License Creative Commons