Siempre que compra algo en Amazon, los datos de sus clientes se actualizan y almacenan automáticamente en miles de máquinas virtuales en la nube. Para empresas como Amazon, garantizar la seguridad y protección de los datos de sus millones de clientes es fundamental. Esto es válido tanto para organizaciones grandes como pequeñas. Pero hasta ahora, no ha habido forma de garantizar que un sistema de software esté a salvo de errores, piratas informáticos y vulnerabilidades.
Los investigadores de Columbia Engineering pueden haber resuelto este problema de seguridad. Han desarrollado SeKVM, el primer sistema que garantiza, mediante pruebas matemáticas, la seguridad de las máquinas virtuales en la nube. En un nuevo artículo que se presentará el 26 de mayo de 2021, en el 42 ° Simposio de IEEE sobre seguridad y privacidad, los investigadores esperan sentar las bases para futuras innovaciones en la verificación del software del sistema, lo que conducirá a una nueva generación de software de sistema ciberresiliente.
SeKVM es el primer sistema verificado formalmente para computación en la nube. La verificación formal es un paso crítico, ya que es el proceso de demostrar que el software es matemáticamente correcto, que el código del programa funciona como debería y que no hay errores de seguridad ocultos de los que preocuparse.
“Esta es la primera vez que se ha demostrado que un sistema de software multiprocesador del mundo real es matemáticamente correcto y seguro”, dijo Jason Nieh, profesor de ciencias de la computación y codirector del Laboratorio de Sistemas de Software. "Esto significa que los datos de los usuarios se administran correctamente mediante software que se ejecuta en la nube y están a salvo de errores de seguridad y piratas informáticos".
La construcción de un software de sistema correcto y seguro ha sido uno de los grandes desafíos de la informática. | Nieh ha trabajado en diferentes aspectos de los sistemas de software desde que se unió a Columbia Engineering en 1999. Cuando Ronghui Gu, profesor asistente de informática de la familia Tang y experto en verificación formal, se unió al departamento de informática en 2018, él y Nieh decidieron colaborar sobre la exploración de la verificación formal de los sistemas de software.
Su investigación ha despertado un gran interés: ambos investigadores ganaron un Premio de Investigación de Amazon, múltiples subvenciones de la National Science Foundation, así como un contrato multimillonario de la Agencia de Proyectos de Investigación Avanzada de Defensa (DARPA) para promover el desarrollo del proyecto SeKVM. Además, Nieh recibió una beca Guggenheim por este trabajo.
Durante los últimos doce años, se ha prestado mucha atención a la verificación formal, incluido el trabajo de verificación de sistemas operativos multiprocesador. "Pero toda esa investigación se ha realizado en pequeños sistemas similares a juguetes que nadie usa en la vida real", dijo Gu. "Se pensaba que verificar un sistema básico multiprocesador, un sistema de uso generalizado como Linux, era más o menos imposible".
El crecimiento exponencial de la computación en la nube ha permitido a las empresas y los usuarios trasladar sus datos y computación fuera del sitio a máquinas virtuales que se ejecutan en hosts en la nube. Los proveedores de computación en la nube, como Amazon, implementan hipervisores para admitir estas máquinas virtuales.
Un hipervisor es la pieza clave de software que hace posible la computación en la nube. La seguridad de los datos de la máquina virtual depende de la exactitud y confiabilidad del hipervisor. A pesar de su importancia, los hipervisores son complicados: pueden incluir un sistema operativo Linux completo. Un solo eslabón débil en el código, uno que es prácticamente imposible de detectar mediante las pruebas tradicionales, puede hacer que un sistema sea vulnerable a los piratas informáticos. Incluso si un hipervisor está escrito correctamente en un 99%, un pirata informático aún puede colarse en esa configuración particular del 1% y tomar el control del sistema.
El trabajo de Nieh y Gu es el primero en verificar un sistema de productos básicos, específicamente el hipervisor KVM ampliamente utilizado, que los proveedores de la nube como Amazon utilizan para ejecutar máquinas virtuales. Demostraron que SeKVM, que es KVM con algunos pequeños cambios, es seguro y garantiza que las computadoras virtuales estén aisladas unas de otras.
“Hemos demostrado que nuestro sistema puede proteger y asegurar los datos privados y la computación cargados en la nube con garantías matemáticas”, dijo Xupeng Li, Ph.D. de Gu. estudiante y coautor principal del artículo. "Esto nunca se ha hecho antes."
SeKVM se verificó utilizando MicroV, un nuevo marco para verificar las propiedades de seguridad de sistemas grandes. Se basa en la hipótesis de que pequeños cambios en el sistema pueden hacer que sea mucho más fácil de verificar, una nueva técnica que los investigadores denominan verificación MICR. Esta novedosa técnica de capas actualiza un sistema existente y extrae los componentes que refuerzan la seguridad en un pequeño núcleo que se verifica y garantiza la seguridad de todo el sistema.
Los cambios necesarios para modernizar un sistema grande son bastante modestos: los investigadores demostraron que si el núcleo pequeño del sistema más grande está intacto, entonces el sistema es seguro y no se filtrarán datos privados. Así fue como pudieron verificar un gran sistema como KVM, que antes se pensaba que era imposible.
"Piense en una casa: una grieta en el panel de yeso no significa que la integridad de la casa esté en riesgo", explicó Nieh. "Sigue siendo estructuralmente sólido y el sistema estructural clave es bueno".
Shih-Wei Li, Ph.D. de Nieh. El estudiante y coautor principal del estudio, agregó: "SeKVM servirá como salvaguardia en varios dominios, desde sistemas bancarios y dispositivos de Internet de las cosas hasta vehículos autónomos y criptomonedas".
Como el primer hipervisor de productos básicos verificado, SeKVM podría cambiar la forma en que se deben diseñar, desarrollar, implementar y confiar en los servicios en la nube. En un mundo donde la seguridad cibernética es una preocupación creciente, esta capacidad de recuperación tiene una gran demanda. Las principales empresas de la nube ya están explorando cómo pueden aprovechar SeKVM para satisfacer esta demanda.