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

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.