VirtualCert: Hacia una Plataforma Certificada de Virtualización - Fase II

El presente proyecto establece líneas de trabajo que han sido identificadas en el proyecto de Investigación Fundamental Fondo Clemente Estable VirtualCert: Hacia una Plataforma Certificada de Virtualización. La actividad de investigación realizada en ese proyecto se focalizó en el estudio de plataformas de virtualización. En una plataforma de este tipo, el Virtual Machine Monitor o hypervisor es el componente que provee a las máquinas virtuales guests (VMs) que ejecutan sobre la plataforma el acceso a los recursos del hardware subyacente, es decir, el ambiente computacional sobre el que opera cada máquina. En particular, el hypervisor 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 especialmente 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. Como resultado del trabajo de investigación desarrollado en el proyecto VirtualCert ya se cuenta con una versión completamente formalizada y verificada usando el asistente de pruebas Coq de un modelo idealizado de plataforma de virtualización y se han probado propiedades de seguridad que garantizan que esos sistemas solamente tienen acceso a la memoria que les pertenece. Estas últimas propiedades han sido formuladas como propiedades de no interferencia, o más precisamente, no influencia. Adicionalmente, se ha desarrollado una extensión al modelo originalmente propuesto que consiste en incorporar la noción de memoria cache y TLB (Translation Lookahead Buffers). Esto permite modelar comportamiento relativo a la gestión, y particularmente al acceso, de la memoria de la plataforma. Las líneas de investigación del proyecto que aquí se presenta continúan y complementan el trabajo realizado en el proyecto VirtualCert. En particular, el esfuerzo de investigación se dirigirá al desarrollo de tres líneas principales de trabajo, a saber: (1) el modelado de estructuras de cache alternativas, como las de tipo VIPT (Virtually Indexed Physically Tagged), así como de diferentes políticas de escritura de estos componentes de memoria (write-back, write-through) con el objetivo de probar formalmente que las propiedades de no influencia para el modelo actual son preservadas en presencia de estas estructuras y políticas de escritura, (2) el desarrollo de la prueba de no influencia para un prototipo del hypervisor implementado en código C, y (3) el desarrollo de una extensión del modelo que permita establecer y probar formalmente propiedades de seguridad relacionadas con ataques basados en la observación de la gestión de la memoria cache de la plataforma de virtualización. Esta segunda fase de VirtualCert se propone capitalizar el conocimiento adquirido previamente, difundido en prestigiosos eventos internacionales, realizando extensiones significativas que permitirán establecer y validar propiedades de seguridad críticas concernientes tanto al modelo idealizado de virtualización como al código de bajo nivel.