Un Framework para el Análisis Formal de Modelos de Control de Acceso para Dispositivos Móviles Interactivos

DSpace/Manakin Repository

Show simple item record

dc.contributor.advisor Luna, Carlos D.
dc.contributor.advisor Betarte, Gustavo
dc.contributor.author Crespo, Juan Manuel
dc.date.accessioned 2013-03-25T19:39:02Z
dc.date.available 2013-03-25T19:39:02Z
dc.date.issued 2009-04
dc.identifier.uri http://hdl.handle.net/2133/2330
dc.description.abstract Los dispositivos portátiles tales como teléfonos celulares y asistentes personales de datos, permiten almacenar información confidencial y establecer comunicaciones con entidades externas. Generalmente, los usuarios pueden descargar e instalar nuevas aplicaciones de fuentes no confiables, que conviven junto con las instaladas por el fabricante del dispositivo o proveedor de servicios de comunicación. Ante este escenario, es importante garantizar la confidencialidad e integridad de los datos almacenados, así como la disponibilidad del servicio, aún cuando una aplicación maliciosa trate de hacer uso indebido de las funciones del dispositivo. La plataforma Java Micro Edition (JME), una tecnología para desarrollo de software Java, provee el estándar Mobile Information Device Profile (MIDP) que facilita el desarrollo de aplicaciones y especifica un modelo de seguridad para el acceso controlado a recursos sensibles del dispositivo. El modelo está construido sobre la noción de dominio de protección, que puede ser concebido como un conjunto de permisos. Un modelo alternativo ha sido propuesto, que extiende los permisos presentes en MIDP, introduciendo la noción de multiplicidad, y flexibilizando la forma en la que el usuario puede conceder a las aplicaciones que son utilizadas en el dispositivo, accesos a los recursos del mismo. Esta tesina presenta un framework, formalizado utilizando el asistente de pruebas Coq, adecuado para la definición y comparación formal de políticas de control de acceso que pueden ser aplicadas por variantes de esos modelos de seguridad y para el análisis y prueba de propiedades de seguridad que éstas satisfacen. Las pruebas de algunas de estas propiedades son dadas y discutidas en el trabajo. Además, se provee una generalización que abstrae el concepto de modelo de control de accesos y se define un concepto de generalidad que permite compararlos formalmente. es
dc.language.iso spa es
dc.publisher Facultad de Ciencias Exactas, Ingenieria y Agrimensura. Universidad Nacional de Rosario es
dc.rights openAccess es
dc.subject Dispositivos Móviles es
dc.subject Control de Acceso es
dc.subject Modelos de Seguridad para Dispositivos Móviles es
dc.subject Modelo de Seguridad JME-MIDP es
dc.subject Modelo alternativo es
dc.title Un Framework para el Análisis Formal de Modelos de Control de Acceso para Dispositivos Móviles Interactivos
dc.type bachelorThesis
dc.type tesis de grado
dc.type publishedVersion
dc.description.peerreviewed Peer reviewed es
dc.relation.publisherversion http://www.fceia.unr.edu.ar/lcc/t523/uploads/15.pdf es
dc.description.affiliation Fil: Crespo, Juan Manuel. Tesista del Departamento de Ciencias de la Computación. Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario; Argentina.


Files in this item

This item appears in the following Collection(s)

Show simple item record

My Account


Search DSpace


Browse