Análisis Formal de la Instalación de Aplicaciones en MIDP 3.0.

Prince, Cristián Germán

Análisis Formal de la Instalación de Aplicaciones en MIDP 3.0.

dc.contributor.advisor	Luna, Carlos Daniel
dc.creator	Prince, Cristián Germán
dc.date.accessioned	2015-02-18T14:45:38Z
dc.date.available	2015-02-18T14:45:38Z
dc.date.issued	2014-12-19
dc.description.abstract	Hoy en día, la telefonía celular se ha vuelto imprescindible para el desarrollo de la vida cotidiana. Además de sus servicios básicos de comunicación, los dispositivos móviles permiten almacenar datos confidenciales y, descargar y ejecutar aplicaciones, lo que conlleva un riesgo para la integridad y privacidad de la información que uno tiene. Es por ello que la seguridad pasa a tener un rol fundamental en el desarrollo y en el éxito de las tecnologías móviles. En la plataforma Java Micro Edition, el ambiente de ejecución estándar para teléfonos celulares está provisto por el Perfil para Dispositivos de Información Móviles (MIDP, por sus siglas en Inglés). Para la versión 2.0 de MIDP, Zanella, Luna y Betarte, propusieron la primera especificación formal de su modelo de seguridad. Se construyó un modelo abstracto en el Cálculo de Construcciones Inductivas (CIC) del estado de un dispositivo y de los posibles eventos que inducen cambios en dicho estado. Además, se han demostrado propiedades deseables para cualquier implementación del estándar, lo que lo convierte en una poderosa herramienta para razonar sobre el modelo de seguridad y facilitar su comprensión. Una primera extensión de este modelo fue realizada por Gustavo Mazeikis, quien realizó la formalización del Modelo de Autorización para MIDP 3.0 (la más reciente versión del perfil) y demostró la preservación de las propiedades de seguridad consideradas para MIDP 2.0. En este trabajo se presenta una nueva extensión de la especificación formal referida. Este proyecto conserva las propiedades de seguridad demostradas por Mazeikis e incorpora el manejo y almacenamiento de vendedores y certificados en el dispositivo que son utilizados al momento de la instalación, como así también cambios sustanciales sobre la definición de este evento crítico. El aporte principal de este trabajo es la verificación sobre el vendedor de una aplicación y su certificado asociado, abarcando el caso en que éste no posea uno. De esta manera, un usuario puede instalar aplicaciones de vendedores cuyos certificados autentican que son confiables o aplicaciones de vendedores que no poseen dicha certificación, como podría ser el caso de un programador que desarrolla una aplicación para uso propio o compartido. En el marco del formalismo extendido, se propone un algoritmo para realizar la instalación de una aplicación y se demuestra su corrección.	es
dc.description.fil	FCEIA-UNR	es
dc.description.peerreviewed	Peer reviewed
dc.format	application/pdf
dc.format	application/octet-stream
dc.identifier.other	http://www.fceia.unr.edu.ar/lcc/t523/tesina.php?campo1=73
dc.identifier.uri	http://hdl.handle.net/2133/3825
dc.language.iso	spa	es
dc.publisher	Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario	es
dc.rights	openAccess	es
dc.rights.uri	http://creativecommons.org/publicdomain/zero/1.0/	*
dc.subject	MIDP	es
dc.subject	Instalación	es
dc.subject	Especificación	es
dc.subject	Celulares	es
dc.subject	Aplicaciones	es
dc.title	Análisis Formal de la Instalación de Aplicaciones en MIDP 3.0.	es
dc.type	bachelorThesis
dc.type	tesis de grado
dc.type	publishedVersion
dc.type.collection	tesis