Por favor, use este identificador para citar o enlazar este ítem:
https://hdl.handle.net/20.500.12008/3413
Cómo citar
Registro completo de metadatos
Campo DC | Valor | Lengua/Idioma |
---|---|---|
dc.contributor.author | Roushani Oskui, Ramin | es |
dc.contributor.author | Betarte, Gustavo | es |
dc.contributor.author | Luna, Carlos | es |
dc.date.accessioned | 2014-12-02T16:05:37Z | - |
dc.date.available | 2014-12-02T16:05:37Z | - |
dc.date.issued | 2008 | es |
dc.date.submitted | 20141202 | es |
dc.identifier.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. | es |
dc.identifier.issn | 0797-6410 | es |
dc.identifier.uri | http://hdl.handle.net/20.500.12008/3413 | - |
dc.description.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. | es |
dc.format.extent | 12 p. | es |
dc.format.mimetype | application/pdf | es |
dc.language | in | es |
dc.publisher | UR. FI – INCO. | es |
dc.relation.ispartof | Reportes Técnicos 08-06 | es |
dc.rights | Las obras depositadas en el Repositorio se rigen por la Ordenanza de los Derechos de la Propiedad Intelectual de la Universidad De La República. (Res. Nº 91 de C.D.C. de 8/III/1994 – D.O. 7/IV/1994) y por la Ordenanza del Repositorio Abierto de la Universidad de la República (Res. Nº 16 de C.D.C. de 07/10/2014) | es |
dc.subject | Java Micro Edition | es |
dc.subject | Calculus of Inductive Constructions | es |
dc.subject | Information Integrity | es |
dc.title | A Certified Access Controller for JME-MIDP 2.0 enabled Mobile Devices | es |
dc.type | Reporte técnico | es |
dc.rights.licence | Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0) | es |
Aparece en las colecciones: | Reportes Técnicos - Instituto de Computación |
Ficheros en este ítem:
Fichero | Descripción | Tamaño | Formato | ||
---|---|---|---|---|---|
TR0806.pdf | 192,38 kB | Adobe PDF | Visualizar/Abrir |
Este ítem está sujeto a una licencia Creative Commons Licencia Creative Commons