October 23, 2024
Estudiantes: Carlos Luna
Tutores: <a href=https://www.fing.edu.uy/inco/grupos/gsi/team/gustavo-betarte/>Gustavo Betarte</a>
En esta tesis investigamos la seguridad de aplicaciones de seguridad críticas, es decir aplicaciones en las cuales una falla podría producir consecuencias inaceptables. Consideramos tres áreas: dispositivos móviles, plataformas de virtualización y sistemas de nombres de dominio.La plataforma Java Micro Edition define el Perfil para Dispositivos de Información Móviles (MIDP) para facilitar el desarrollo de aplicaciones para dispositivos móviles, como teléfonos celulares y asistentes digitales personales. En este trabajo primero estudiamos y comparamos formalmente diversas variantes del modelo de seguridad especificado por MIDP para acceder a recursos sensibles de un dispositivo móvil.Los hipervisores permiten que múltiples sistemas operativos se ejecuten en un hardware compartido y ofrecen un medio para establecer mejoras de seguridad y flexibilidad de sistemas de software. En esta tesis formalizamos un modelo de hipervisor y establecemos (formalmente) que el hipervisor asegura propiedades de aislamiento entre los diferentes sistemas operativos de la plataforma, y que las solicitudes de estos sistemas son atendidas siempre. Demostramos también que las plataformas virtualizadas son transparentes, es decir, que un sistema operativo no puede distinguir si ejecuta sólo en la plataforma o si lo hace junto con otros sistemas operativos.Las Extensiones de Seguridad para el Sistema de Nombres de Dominio (DNSSEC) constituyen un conjunto de especificaciones que proporcionan servicios de aseguramiento de autenticación e integridad de origen de datos DNS. Finalmente, presentamos una especificación minimalista de un modelo de DNSSEC que proporciona los fundamentos necesarios para formalmente establecer y verificar propiedades de seguridad relacionadas con la cadena de confianza del árbol de DNSSEC.Desarrollamos todas nuestras formalizaciones en el Cálculo de Construcciones Inductivas —lenguaje formal que combina una lógica de orden superior y un lenguaje de programación funcional tipado— utilizando el asistente de pruebas Coq.
Palabras clave: Modelos formales, Propiedades de seguridad, Asistente de pruebas Coq, JME-MIDP, Virtualización, DNSSEC.