A Rigorous Methodology for Security Architecture Modeling and Verification

This paper introduces a rigorous methodology for utilizing threat modeling in building secure software architectures using SAM (Software Architecture Modeling framework) and verifying them formally using Symbolic Model Checking. Security mitigations are expressed as constraints over a high-level SAM model and are used to refine it into a secure constrained model. We also, propose a translation from SAM Secure models into the SMV model checker where the threats and the elicited security properties from the threat modeling process are used as inputs to the verification phase as well. This method is developed with the aim of bridging the gap between informal security requirements and their formal representation and verification.