Generación Automatizada de Pruebas de Seguridad con Modelos de Amenaza Formales

Los ataques de seguridad típicamente resultan de comportamientos no intencionados o entradas inválidas. La prueba de seguridad es intensiva en mano de obra porque un programa del mundo real generalmente tiene demasiadas entradas inválidas. Es altamente deseable automatizar o parcialmente automatizar el proceso de prueba de seguridad. Este documento presenta un enfoque para la generación automatizada de pruebas de seguridad utilizando modelos de amenaza formales representados como redes de Predicado/Transición. Genera todos los caminos de ataque, es decir, pruebas de seguridad, a partir de un modelo de amenaza y los convierte en código de prueba ejecutable de acuerdo con la especificación dada de Mapeo Modelo-Implementación (MIM). Hemos aplicado este enfoque a dos sistemas del mundo real, Magento (un sistema de compras en línea utilizado por muchas tiendas en línea) y FileZilla Server (una popular implementación de servidor FTP en C++). Los modelos de amenaza se construyen sistemáticamente examinando todas las amenazas potenciales de STRIDE (suplantación de identidad, manipulación de datos, repudio, divulgación de información, denegación de servicio y elevación de privilegios) a las funciones del sistema. Las pruebas de seguridad generadas a partir de estos modelos han encontrado múltiples riesgos de seguridad en cada sistema. El código de prueba para la mayoría de las pruebas de seguridad puede ser generado y ejecutado automáticamente. Para evaluar aún más la capacidad de detección de vulnerabilidades del enfoque de prueba, se han aplicado las pruebas de seguridad a un número de mutantes de seguridad donde se inyectan deliberadamente vulnerabilidades. Los mutantes se crean de acuerdo con las vulnerabilidades comunes en C++ y aplicaciones web. Nuestros experimentos muestran que las pruebas de seguridad han eliminado la mayoría de los mutantes.