Search

status: published

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. status: published

This document presents Smarmy, a formal modelling language intended to verify the security of software architectures. Smarmy is created with the practising software architect in mind. Its semantics are very close to how a software architecture would be modelled in UML, while its syntax is similar to Java. Smarmy is supported by Smarmelade, which is an integrated development environment built on top of the Eclipse framework. Smarmelade uses model finding to verify Smarmy models, and generate and visualise counterexamples to help the architect in debugging. The purpose of the Smarmy approach is to systematically uncover the context of an architecture, which consists of the assumptions that that architecture makes on its environment which are necessary to uphold its security requirements. The context represents the minimal but necessary preconditions on the deployment environment of the architecture. It can serve as an explicit target for a risk assessment, or as a checklist to ensure that the system-to-be is deployed securely. ispartof: CW Reports nrpages: 34 status: published

ispartof: Nordic Workshop on Secure IT Systems (NordSec) location:Copenhagen, Denmark date:Oct - Oct 2008 status: published

Reusing time-tested solutions rather than inventing ad-hoc quick fixes is a well-known security principle. Architectural and design patterns represent proven techniques to package knowledge from software engineering experts in a reusable format. More importantly, the solution proposed by a pattern is known to be sound because it is time-tested -- its strengths, weaknesses and possible drawbacks are known in advance. Therefore, in software security engineering, security patters have been considered to be a very promising means to increase the quality of secure design and make security more accessible to software engineers. However, their adoption does not live up to their potential. To understand why this is so, this paper analyzes the literature of security patterns published over the last ten years and outlines existing gaps. ispartof: CW Reports nrpages: 24 status: published

Security patterns, as domain-independent expert knowledge packaged in a reusable format, are able to offer significant guidance to the software engineer in developing secure systems. However, the overabundance of published security patterns complicates the process of finding the right pattern to solve the problem at hand. This is due to three reasons. First, not all security patterns are relevant to the software engineer. Second, the domain independence of patterns sometimes complicates finding a solution to a domain specific problem. Third, patterns exist on different levels of abstraction. Not all patterns can be applied to every step in the development process of a system. This report proposes a method to facilitate the selection of a suitable set of security patterns to realize a specific set of security requirements. It is comprised of two parts. First, additional structure is superimposed on this collection. Second, a methodology is proposed that, given this structured inventory of patterns, guides the software engineer from the security requirements to an appropriate solution using patterns, taking into account various trade-offs and relations between patterns. ispartof: CW Reports nrpages: 26 status: published

The security of Industrial Control Systems (ICS) has become an important topic. Attacks such as the Stuxnet worm have shown that inadequately protecting control systems could have disastrous consequences for society. Our research focuses on the creation of a tool that aims to enhance the security of Industrial Control Systems. It will be possible for system owners and operators to model their control systems in our tool. Using formal methodologies, the tool can extract a list of vulnerabilities in the system. Users can reason about the effects on system security of component changes or newly discovered vulnerabilities. ispartof: pages:45-48 ispartof: Proceedings of the 2014 ESSoS Doctoral Symposium co-located with the International Symposium on Engineering Secure Software and Systems (ESSoS 2014) vol:1298 pages:45-48 ispartof: ESSoS-DS 2014 location:Munich date:26 Feb - 26 Feb 2014 status: published