Título: Especificación Formal del Módulo de Control de Acceso de MIDP 2.0 para Dispositivos Móviles Interactivos

Marco de Trabajo: Investigación

Área de desarrollo: Métodos Formales

Autor: Carlos Luna

Contacto: cluna@fing.edu.uy

Día: JUEVES

Hora: 13:15

Palabras Claves: Seguridad Informática, Métodos Formales

Resumen:
Trabajo en el marco de un proyecto de grado en Argentina. Los dispositivos portátiles permiten almacenar información confiencial y establecer comunicaciones con entidades externas. En esta clase de dispositivos es importante garantizar la confidencialidad e integridad de los datos almacenados, así como la disponibilidad del servicio. La tecnología Java provee el estándar MIDP que facilita el desarrollo de aplicaciones y cuenta con un modelo de seguridad que intenta preservar estas propiedades. Esta charla presenta una especificación formal del módulo de control de acceso de MIDP 2.0 de J2ME, encargado de manejar autorizaciones a recursos sensibles. El trabajo extiende una especificación desarrollada en Coq del modelo de seguridad de MIDP; formaliza el evento de llamada a funciones del dispositivo por parte de una aplicación, demuestra que la extensión es conservativa y analiza propiedades relevantes de seguridad. Finalmente, se refina la especificación a un modelo ejecutable y se certifica un algoritmo escrito en Coq como una implementación del módulo de control de acceso.