Security analysis methods can provide correct yet meaningless results if the assumptions underlying the model do not conform to reality. We present an approach to analyze the security of software-intensive system architectures that focusses on making these underlying assumptions explicit, so that they can be taken into account. Starting from an Alloy model of a software architecture, a set of constraints is elicited by leveraging model relaxation techniques. These constraints form a minimal but sufficient condition that the system must meet in order to realise its security requirements. As the approach starts from the minimal guarantees that the system environment offers, it does not depend on an explicit attacker model and can take arbitrary attacker behaviour into account. As it is iterative, it is possible to constructively integrate the approach in a secure software development life cycle. Our results are illustrated by means of a case study.
展开▼
