May 5, 2017
Estudiantes: Julio Pérez
Tutores: <a href=https://www.fing.edu.uy/inco/grupos/gsi/team/gustavo-betarte/>Gustavo Betarte</a>, <a href=https://www.fing.edu.uy/inco/grupos/gsi/team/carlos-luna/>Carlos Luna</a>
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.