Author:

Abstract:

Security is no sugar coating that can be added to a software system as an afterthought; a software system should be designed securely from the start. Over the years, many approaches have been conceived that analyse the security of a software system throughout the various phases of the software development process. One phase in particular, software architecture design, has proven to be crucial in this process.Analysis methods for software architecture security can be subdivided into two categories: engineering methods and formal methods. While engineering methods excel in achieving reasonable security with reasonable effort, formal methods can provide stronger security guarantees in return for an often much larger investment. However, formal methods do not always take the intricacies of software architecture design into account. This includes providing support for the decomposition of large models, information hiding through abstraction, reuse of verification results, creating partial models with incomplete information early in the design phase, catering to the various stakeholders involved in software development, and integration of the modelling process itself in a larger enterprise risk management process. This last feature is critical---if the residual risk inherent in a security analysis is not made explicit, then the results of a formal analysis can be correct in theory but worthless in practise.The central thesis of this dissertation is that it is possible to bring both categories of secure software architecture analysis methods closer together. We propose a novel formal modelling and verification technique for software architectures that is based on model finding. By systematically eliciting assumptions, we enable integration of the verification results in a risk management process, and facilitate the involvement of various stakeholders such as the security expert, application deployer and requirements engineer. Furthermore, we prove that the verification results are composable, which in turn supports information hiding through abstraction, reusing (partial) verification results, and makes the verification of large models tractable.The modelling technique is verified by creating a reusable library of a security pattern language for accountability, in which a number of relevant undocumented assumptions are uncovered that were left implicit in the original documentation. The usability of this library is demonstrated through a small but rigorous observational case study, which shows that non experts can use this library to create secure architectural compositions. We verify that the approach supports mainstream architectural modelling practises, and that the verification supports mainstream security properties. We also illustrate how extra language concepts can be leveraged to improve upon the proposed modelling technique. We conclude that it is possible to bring both the secure software architecture engineering community and formal community closer together, a longer term process in which this work is a first step.