Model Checking para el código de arranque de los centros de datos de AWS(Amazon Web Services)
Este artículo describe nuestra experiencia con model checking simbólico en un entorno industrial. Hemos demostrado que el código de arranque inicial que se ejecuta en los centros de datos de Amazon Web Services es seguro para la memoria, un paso esencial para establecer la seguridad de cualquier centro de datos. Las herramientas estándar de análisis estático no se pueden usar fácilmente en el código de arranque sin modificaciones debido a problemas que no se encuentran comúnmente en el código de nivel superior, incluidas las interfaces de dispositivos mapeados en memoria, el acceso a la memoria de nivel de bytes y los scripts enlazados. Este documento describe soluciones automatizadas a estos problemas y su implementación en C Bounded Model Checker (CBMC). CBMC es ahora la primera herramienta de análisis estático de nivel de fuente para extraer el diseño de memoria descrito en un script enlazado para su uso en su análisis.
Este post es una traducción de Model Checking Boot Code from AWS Data Centers
- Título original: Model Checking Boot Code from AWS Data Centers
- Autores: Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle
- Año: 2018
