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 extendió un modelo preexistente del sistema de seguridad de Android considerando los cambios introducidos en su versión 6.0 y especificando el comportamiento del sistema frente a la ejecución de operaciones erróneas. También se desarrolló un programa que implementa tal modelo y se demostró formalmente su corrección. Además se postularon y demostraron propiedades de seguridad sobre el modelo y el código ejecutable referidos y finalmente se explicó 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.