Título: Formalización y Análisis del Modelo de Seguridad de MIDP 3.0 para Dipositivos Móviles Interactivos

Marco de Trabajo: Proyecto de Grado

Área de desarrollo: Métodos Formales

Autor: Gustavo Mazeikis

Contacto: mazeikis@adinet.com.uy

Día: JUEVES

Hora: 13:45

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

Resumen:
Tutores: Gustavo Betarte y Carlos Luna
En la Plataforma Java Micro Edition, el Perfil para Dispositivos de Información Móviles (MIDP) provee el ambiente de ejecución estándar para teléfonos móviles y asistentes de datos personales. La tercera versión del perfil, de reciente publicación, introduce una nueva dimensión en el modelo de seguridad de MIDP: la seguridad a nivel de aplicación. Para la segunda versión de MIDP, Zanella, Betarte y Luna proponen una especificación formal del modelo de seguridad en el Cálculo de Construcciones Inductivas, usando el asistente de pruebas Coq. Este trabajo presenta una extensión de la especificación referida, para incorporar los cambios planteados por la tercera versión de MIDP. La extensión planteada conserva las propiedades de seguridad demostradas en el modelo anterior y permite seguir razonando sobre nuevas propiedades relevantes de seguridad.