May 5, 2017
Estudiantes: Felipe Gorostiaga (Universidad de Rosario, Argentina)
Tutores: Gustavo Betarte, Carlos Luna
La vasta cantidad de dispositivos móviles ejecutando Android y las facilidades de distribución de software de terceros que ofrece hacen de este sistema operativo un objetivo tentador para ciberdelincuentes, cuyas acciones tienen el potencial de afectar a miles de millones de personas. Esta situación ha puesto a Android bajo la lupa de los investigadores, quienes pretenden poner a prueba la robustez de su sistema de seguridad y minimizar los vectores de ataque. En este trabajo se extiende un modelo preexistente del sistema de seguridad de Android para considerar los cambios introducidos en su versión 6.0 y especificar el comportamiento del sistema frente a la ejecución de operaciones erróneas. También se presenta un programa que implementa tal modelo y se demuestra formalmente su corrección. Además se postulan y demuestran propiedades de seguridad sobre el modelo y el código ejecutable referidos. Finalmente se explica la manera en que la implementación certificada puede utilizarse a modo de oráculo de referencia para verificar la corrección de una plataforma real, y cómo permitiría la posterior programación de un monitor de seguridad capaz de supervisar una plataforma en tiempo real.