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

dc.contributor.advisorLuna, Carlos Daniel
dc.creatorPrince, Cristián Germán
dc.date.accessioned2015-02-18T14:45:38Z
dc.date.available2015-02-18T14:45:38Z
dc.date.issued2014-12-19
dc.description.abstractHoy 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.filFCEIA-UNRes
dc.description.peerreviewedPeer reviewed
dc.formatapplication/pdf
dc.formatapplication/octet-stream
dc.identifier.otherhttp://www.fceia.unr.edu.ar/lcc/t523/tesina.php?campo1=73
dc.identifier.urihttp://hdl.handle.net/2133/3825
dc.language.isospaes
dc.publisherFacultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosarioes
dc.rightsopenAccesses
dc.rights.urihttp://creativecommons.org/publicdomain/zero/1.0/*
dc.subjectMIDPes
dc.subjectInstalaciónes
dc.subjectEspecificaciónes
dc.subjectCelulareses
dc.subjectAplicacioneses
dc.titleAnálisis Formal de la Instalación de Aplicaciones en MIDP 3.0.es
dc.typebachelorThesis
dc.typetesis de grado
dc.typepublishedVersion
dc.type.collectiontesis

Archivos

Bloque original
Mostrando 1 - 2 de 2
Cargando...
Miniatura
Nombre:
Prince.pdf
Tamaño:
395.82 KB
Formato:
Adobe Portable Document Format
Descripción:
Tesina LCC
Nombre:
Código Tesina Cristián Prince.rar
Tamaño:
511.5 KB
Formato:
Unknown data format
Bloque de licencias
Mostrando 1 - 1 de 1
Nombre:
license.txt
Tamaño:
3.14 KB
Formato:
Item-specific license agreed upon to submission
Descripción: