Herramientas automatizadas para aplicar métodos formales para verificar la política de seguridad en el software existente

1

Soy nuevo en el campo de los Métodos Formales, pero siento que tengo una comprensión educada de sus aplicaciones. Sin embargo, parece que solo encuentro métodos formales aplicados al proceso de desarrollo, a medida que se crea el software.

Me gustaría poder aplicar métodos formales en el software existente para comprobar si cumple con los controles de acceso basados en roles (RBAC) y la separación de información confidencial siguiendo el método de Bell-LaPadula (BLP).

¿Qué métodos y herramientas conoce que ofrecen una solución automatizada para la verificación similar a RBAC y BLP del software / código fuente existente?

    
pregunta Methmal Forods 14.06.2015 - 17:00
fuente

1 respuesta

0

Hace muchos años escribí sobre métodos y seguridad formales aquí - enlace : lo básico es cómo aplicar los estándares del antiguo Libro Naranja al software moderno.

Si tuviera que volver a escribir esa publicación de blog en 2015, algunas de las actualizaciones que agregaría son que los verificadores de modelos basados en SMT se han vuelto mucho más diversos, integrados y avanzados que los simples que describí (SPIN y JPF ). Estas páginas deben guiarlo hacia algunos de estos avances: enlace - enlace - enlace

DARPA está trabajando en un proyecto de Verificación formal de origen público (CSFV) aquí: enlace

Aunque estoy a favor de la automatización, sería interesante saber más sobre el dominio del problema para hacer recomendaciones secundarias sobre pruebas manuales. ¿Esto es para problemas de autorización basados en web y móvil de comercio electrónico? ¿Qué dominio (s) están involucrados?

    
respondido por el atdre 14.06.2015 - 18:01
fuente

Lea otras preguntas en las etiquetas