Carlos|
Luna|
cluna@fing.edu.uy|
InCo|
Formalización de arquitecturas de seguridad en dispositivos móviles y en plataformas de virtualización|
métodos formales, seguridad informática|
INVESTIGACION|
charla propuesta para el track de seguridad (y métodos formales)|
Los dispositivos portátiles, tales como teléfonos celulares y asistentes de datos personales, 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. En 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 que extiende los permisos presentes en MIDP ha sido propuesto por Besson, Dufay y Jensen. Este modelo introduce una noción de multiplicidad asociada a los permisos y flexibiliza la forma en la que el usuario puede conceder acceso a los recursos del dispositivo, a las aplicaciones que son utilizadas en el mismo. 

En esta charla se comentarán algunos trabajos realizados, en el contexto de los grupos Métodos Formales y Seguridad del InCo, sobre la especificación y el análisis formal de componentes de modelos de seguridad para dispositivos móviles interactivos. En particular, se describirán experiencias relacionadas con las tres generaciones de MIDP y se presentará un framework que permite definir y comprar formalmente políticas de control de acceso, que pueden ser aplicadas por variantes de los modelos de seguridad considerados.

Finalmente, se describirá un trabajo en progreso que aborda el estudio del comportamiento de plataformas de computación virtuales. Concretamente, se focaliza en la especificación y verificación formal de determinadas propiedades de seguridad, que es deseable sean garantidas por plataformas de virtualización sobre las que son ejecutadas variedades de máquinas virtuales que ofician de hosts a sistemas operativos, sean estos confiables o no. En particular, interesa modelar formalmente la interacción de diferentes sistemas operativos ejecutando sobre una misma plataforma virtualizada y establecer cuáles son los mecanismos que garantizan determinadas propiedades de no interferencia, particularmente en relación a los datos manejados por los sistemas que ejecutan concurrentemente sobre esa plataforma.
|