Investigadores de la Universidad de Princeton, la Universidad de Michigan y el Lafayette College publicaron un artículo técnico titulado «Verificación de seguridad de arquitecturas de baja confianza».
Resumen:
«Las arquitecturas de menor confianza, desde una perspectiva de software, manejan datos siempre cifrados y reducen significativamente la cantidad de confianza del hardware en un pequeño componente enclave libre de software. En este documento, proporcionamos una verificación formal completa de una arquitectura lean específica. , la arquitectura Sequestered Encryption (SE), para mostrar que el diseño es seguro contra todos los programas posibles contra divulgaciones directas de datos y canales laterales digitales. Primero, definimos los requisitos de seguridad de la arquitectura SE ISA de baja confianza. Mirando hacia arriba, esta ISA sirve como una abstracción de software-hardware, y cualquier código que incluya estas instrucciones se usa para mostrar que el programa no puede filtrar información, incluso a través de canales laterales digitales. Mirando hacia abajo Esta ISA es una especificación para hardware y se usa para definir las obligaciones de prueba para cualquier implementación RTL derivada de los requisitos de seguridad de nivel ISA. Estos cubren las fugas funcionales y digitales del canal lateral. A continuación mostramos cómo se pueden cumplir estas obligaciones probatorias utilizando herramientas comerciales de verificación formal. Demostramos la efectividad de nuestra técnica de verificación de seguridad RTL para siete implementaciones diferentes correctas y propensas a errores de la arquitectura SE».
Encuéntralo documento técnico aquí. Publicado en septiembre de 2023 (preimpresión).
Tan, Qinhan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean-Baptiste Jeannin, Sharad Malik y Todd Austin. «Verificación de seguridad de arquitecturas de baja confianza». Preimpresión de arXiv arXiv:2309.00181 (2023).
Lectura relacionada
Verificación y pruebas de seguridad y protección.
La verificación funcional está superando sus capacidades para garantizar sistemas seguros y protegidos. El nuevo soporte proviene del hardware y el software.
Nuevos conceptos necesarios para la verificación de seguridad.
¿Por qué es tan difícil garantizar que el hardware funcione correctamente y sea capaz de detectar vulnerabilidades que puedan aparecer en el campo?
