Towards continuous verification of security patterns

Abstract

Security patterns are widely recognized as an effective solution for mitigating vulnerabilities in software design and development. However, ensuring that integrated patterns remain correct across evolving system specifications is a challenging problem in practice. This is more so when the evolution occurs at runtime. In order to solve this problem, we propose a solution for the synchronization of a pragmatic security pattern framework for Java source code (which includes runtime monitoring of security properties) with a formal specification in Alloy, so that changes to the pattern introduced by evolution events trigger a correctness verification. Our solution leverages model federation, a model-management paradigm that promotes the reification of dependencies between heterogeneous models while keeping them in their original technological spaces.