Título:
A Certified Access Controller for JME-MIDP 2.0 enabled Mobile Devices
Otros títulos:
Coordinador:
Director:
Compilador:
Autor:
Roushani Oskui, Ramin
Betarte, Gustavo
Luna, Carlos
Betarte, Gustavo
Luna, Carlos
Tutor:
Tipo de documento:
Reporte técnico
Editor:
Palabras clave:
Java Micro Edition
Calculus of Inductive Constructions
Information Integrity
Calculus of Inductive Constructions
Information Integrity
Descriptores:
Año de publicación:
2008
Contenido:
Resumen:
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.
Descripción:
Editorial:
UR. FI – INCO.
EN:
Reportes Técnicos 08-06
Financiadores:
Citación:
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.
Citación:
metadata.cc.license.name:
Documento del Gobiberno:
URI:
http://hdl.handle.net/20.500.12008/3413
ISBN:
e-ISBN:
ISSN:
0797-6410
ISMN:
Otros identificadores:
Título Obtenido:
Facultad o Servicio que otorga el Título:
Licencia:
Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)
Cobertura geográfica:
Cobertura temporal:
metadata.dc.relation.IsVersionOf:
Clasificación:
Es versión de:
Colecciones:
| Ficheros | Descripción | Tamaño | Formato | ||
|---|---|---|---|---|---|
| TR0806.pdf | — | 192.38 KB | Adobe PDF |