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

dc.contributor.advisorLuna, Carlos D.
dc.contributor.advisorBetarte, Gustavo
dc.contributor.authorCrespo, Juan Manuel
dc.date.accessioned2013-03-25T19:39:02Z
dc.date.available2013-03-25T19:39:02Z
dc.date.issued2009-04
dc.description.abstractLos 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.description.affiliationFil: 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.
dc.description.peerreviewedPeer reviewedes
dc.identifier.urihttp://hdl.handle.net/2133/2330
dc.language.isospaes
dc.publisherFacultad de Ciencias Exactas, Ingenieria y Agrimensura. Universidad Nacional de Rosarioes
dc.relation.publisherversionhttp://www.fceia.unr.edu.ar/lcc/t523/uploads/15.pdfes
dc.rightsopenAccesses
dc.subjectDispositivos Móvileses
dc.subjectControl de Accesoes
dc.subjectModelos de Seguridad para Dispositivos Móvileses
dc.subjectModelo de Seguridad JME-MIDPes
dc.subjectModelo alternativoes
dc.titleUn Framework para el Análisis Formal de Modelos de Control de Acceso para Dispositivos Móviles Interactivos
dc.typebachelorThesis
dc.typetesis de grado
dc.typepublishedVersion

Archivos

Bloque original
Mostrando 1 - 1 de 1
Cargando...
Miniatura
Nombre:
15.pdf
Tamaño:
301.25 KB
Formato:
Adobe Portable Document Format
Bloque de licencias
Mostrando 1 - 1 de 1
Nombre:
license.txt
Tamaño:
2.95 KB
Formato:
Item-specific license agreed upon to submission
Descripción: