Modelling and verifying software architectures

This page contains links to all source material on my research on modelling and verifying software architectures. This work is divided in six parts. First, we have defined a meta model to more easily model and verify software architectures. This is documented in modelling an architecture. Second, we have applied this approach to a pattern language of five security patterns for accountability, as documented in modelling security patterns. Third, based on this work, we have conducted a small observational study to verify the applicability of our modelling approach in the case of the online shop.

Future work includes showing how large, detailed architectural models can be decomposed into smaller, tractable models; and providing tool support to facilitate the whole modelling process.

We model software architectures in the Alloy language, which can subsequently be verified with the Alloy Analyzer, a freely available model finder. Our models are based on a meta model which defines generic architectural concepts such as Component, Connector, Node, etc. More details on our modelling technique are available in this COMPSAC 2010 paper.

As security patterns package reusable security solutions, they are an excellent target for improving the reusability of verification results. We have modelled a set of five patterns for accountability, i.e., the Secure Logger, Audit Interceptor, Authentication Enforcer, Authorization Enforcer and Secure Pipe. These patterns are modelled on two levels of abstraction. The abstract models allow the architect to easily compose these patterns into larger architectures, and verify that the composition is secure. The refined models allow the security expert to drill down and verify each pattern down to an arbitrary level of detail, in order to elicit trust assumptions on which the security of that pattern depends.

More details on these models, and how they are used, can be found in this ECSA/WICSA 2012 paper.

The Alloy code of the patterns can be found here. For every pattern, the abstract model, refined model and the correspondence check to verify that one is a refinement of the other is provided. The abstract models:

• Secure Logger
• Audit Interceptor
• Authorization Enforcer
• Authentication Enforcer
• Secure Pipe

The refined security pattern models:

• Secure Logger
• Audit Interceptor
• Authorization Enforcer
• Authentication Enforcer
• Secure Pipe

...and the correspondence checks:

• Secure Logger check
• Audit Interceptor check
• Authorization Enforcer check
• Authentication Enforcer check
• Secure Pipe check

To investigate the usability of the approach and the pattern library, a small observational study was performed in which two architects were tasked to compose two patterns in a simple model of the architecture of an online shop, and verify two corresponding security requirements on that shop. The details of the experiment can be found in the previous ECSA/WICSA 2012 paper. The source files of the experiment can be found here (zip) for reproducibility.

In order to support scalable modelling of large architectures, we have created a formal model theoretical framework that allows decomposing a large model in smaller models, based on refinement. The approach guarantees both security of the approach (i.e., if all parts are secure, the composition will be) and compatibility (i.e., if all parts have instances, the composition will have instances).

(Awaiting publication. Contact me if you are interested.)

We are actively working on an Eclipse plug-in to allow architects to specify architectural models in a higher level DSL. This tool will also support various heuristics to make the modelling and subsequent verification process as painless as humanly possible.

(Ongoing research. Contact me if you are interested.)