La nueva arquitectura informática protege los datos privados confidenciales

Dado que nuestros datos personales se utilizan cada vez más en muchas aplicaciones, desde publicidad hasta finanzas y atención médica, la protección de la información confidencial se ha convertido en una característica esencial para las arquitecturas informáticas. Las aplicaciones que procesan dichos datos deben confiar en el software del sistema en el que confían, como los sistemas operativos y los hipervisores, pero dicho software del sistema es complejo y, a menudo, tiene vulnerabilidades que pueden poner en riesgo la confidencialidad e integridad de los datos.

En los últimos dos años, los investigadores de Columbia Engineering han estado trabajando con Arm, una empresa líder en diseño de software e IP de semiconductores, para abordar estas vulnerabilidades. El equipo ahora ha presentado tecnologías de verificación clave para Arm Confidential Compute Architecture (Arm CCA), una nueva característica de la arquitectura Armv9-A. El documento, presentado el 12 de julio en el 16º Simposio USENIX sobre Diseño e Implementación de Sistemas Operativos (OSDI ’22) en Carlsbad, CA, demuestra la primera verificación formal de un prototipo de firmware Arm CCA.

Arm CCA se basa en el firmware para administrar el hardware y hacer cumplir sus garantías de seguridad, por lo que es esencial que el firmware sea correcto y seguro. Si bien muchos sistemas anteriores se basan en el firmware, ninguno de ellos puede garantizar que el firmware no tenga errores. La verificación formal es una metodología relativamente nueva que ahora se utiliza para garantizar la corrección del software/hardware. En lugar de realizar pruebas, la verificación formal utiliza modelos matemáticos para demostrar que el software y el hardware son absolutamente correctos y, por lo tanto, proporciona el más alto nivel de garantía de corrección.

«Hemos demostrado, por primera vez, que el firmware es correcto y seguro, lo que resultó en la primera demostración de una arquitectura informática confidencial respaldada por un firmware formalmente verificado», dijo el autor principal del estudio, Xupeng Li, Ph.D. estudiante de Ronghui Gu, profesor asistente de informática de la familia Tang, y Jason Nieh, profesor de informática y codirector del Laboratorio de Sistemas de Software.

Si bien existen muchos enfoques para verificar la corrección de programas simples, no son adecuados para algo tan complejo como el firmware CCA, por lo que los investigadores tuvieron que desarrollar nuevas técnicas de verificación para hacer posible la verificación del firmware Arm CCA. Por ejemplo, el firmware CCA está diseñado para la escalabilidad y el rendimiento, por lo que permite una operación altamente simultánea y combina código C y ensamblador. La operación simultánea es posible mediante el uso de métodos de sincronización de grano fino y código con razas de datos.

Es un principio de diseño de Arm CCA que el software que no es de confianza debe mantener el control de la gestión de los recursos de hardware, por lo que un desafío clave es demostrar que el sistema sigue siendo seguro, aunque el software que no es de confianza puede quitarle los recursos de hardware a su antojo. Los enfoques anteriores no han podido verificar programas con tales propiedades. Esta nueva técnica de verificación es lo suficientemente potente como para verificar el firmware simultáneo con código C y ensamblador.

«Los errores son realmente difíciles de encontrar a través de las técnicas clásicas de prueba de software», dijo Xuheng Li, otro Ph.D. estudiante de Nieh y Gu, coautor del trabajo. «Así que mostramos la importancia y el valor de nuestras técnicas de verificación formal y el resultado final fue la primera demostración de una arquitectura informática confidencial respaldada por firmware verificado».

El equipo está muy entusiasmado con las nuevas tecnologías de verificación que se pueden usar para probar la corrección de las implementaciones del firmware subyacente de Arm CCA. Las CPU Arm ya están implementadas en miles de millones de dispositivos en todo el mundo. A medida que Arm CCA se usa más comúnmente para proteger los datos privados de los usuarios, especialmente en los servicios en la nube y más allá, las técnicas de verificación demostradas en este documento proporcionarán una mejora significativa en la protección y seguridad de los datos.

Uno de los desafíos de las metodologías formales aplicadas al software es la necesidad de adaptar las pruebas cuando se actualiza el software. Los investigadores están trabajando en nuevas tecnologías para ayudarlos a verificar de manera incremental y rápida las actualizaciones del firmware Arm CCA y garantizar que siempre se verifique el último firmware disponible.

Gu y Nieh agregaron que «ven el poder y el potencial de la verificación formal de nuestro trabajo, y estamos convencidos de que la verificación formal es una técnica esencial que, en un futuro cercano, suplantará las pruebas de software en uso actual».