May 5, 2017
Estudiantes: Julio Pérez
Tutores: Gustavo Betarte, Carlos Luna
Este proyecto, que se enmarca en un proyecto de investigación más general, aborda el estudio del comportamiento de plataformas de computación virtuales. Concretamente, se focaliza en la especificación y verificación formal de determinadas propiedades de seguridad, que es deseable sean garantidas por plataformas de virtualización sobre las que son ejecutadas variedades de máquinas virtuales que ofician de hosts a sistemas operativos, sean estos confiables o no. En particular, interesa modelar formalmente la interacción de diferentes sistemas operativos ejecutando sobre una misma plataforma virtualizada y establecer cuáles son los mecanismos que garantizan determinadas propiedades de no interferencia, particularmente en relación a los datos manejados por los sistemas que ejecutan concurrentemente sobre esa plataforma.
El objetivo principal del proyecto es especificar formalmente un modelo idealizado de una plataforma de virtualización y verificar formalmente el correcto comportamiento de los mecanismos de gestión de los recursos de memoria de la plataforma.