El proyecto VirtualCert aborda el estudio del comportamiento de plataformas de computación virtuales. En un ambiente virtualizado, el Virtual Machine Monitor (VMM) (por ejemplo VMWare Workstation, Microsoft Virtual Server, Xen) es el componente que provee a las máquinas virtuales (VMs) el acceso a los recursos del hardware subyacente, es decir, el ambiente computacional sobre el que opera cada máquina. Este ambiente incluye el microprocesador, la memoria, los dispositivos de E/S, entre otros. Por lo tanto, y en particular, el VMM es el responsable de que estos recursos sean compartidos por las diferentes VMs en forma segura. El acceso compartido a los recursos de memoria de la plataforma es un tema crítico, en particular si las diferentes VMs pueden potencialmente hostear diferentes sistemas operativos y, consecuentemente, los aplicativos que son ejecutados sobre los mismos. En una plataforma virtualizada, sobre la que por ejemplo se implanten los diferentes sistemas de información de una organización, pueden llegar a convivir en tiempo de ejecución sistemas y aplicativos de orígenes diversos, con comportamientos no necesariamente controlados y de diferentes niveles de confianza.
El entendimiento y modelado de mecanismos de control de acceso y gestión de memoria en plataformas virtualizadas constituye un desafío de interés científico que, al menos para nuestro conocimiento, no ha sido hasta ahora abordado sistemáticamente haciendo uso de herramientas de especificación y verificación formal.
El objetivo principal del proyecto VirtualCert es, en primer lugar, definir y especificar formalmente un modelo idealizado de una plataforma de virtualización, donde el VMM es un hypervisor à la Xen (\cite XenP, Chi07), las VMs básicamente operan de hosts de sistemas operativos, y donde interesa modelar y verificar formalmente el correcto comportamiento de los mecanismos de gestión de los recursos de memoria de la plataforma.
Este proyecto se está desarrollando en colaboración con el Dr. Gilles Barthe de IMDEA Software de España.