Security Architecture is one activity of the Trustworthy Systems project.
Aim: To model and analyse the software architectures of secure systems.
- We have developed a case study: designing, analysing and developing a smart electricity meter based on CAmkES and seL4 using our approach and tools.
Overview: A security architecture provides a high-level design of the system,
describing the main software components and their interconnections,
together with security-related properties of these components and
connectors. Given such an architecture we can perform analysis of the
system's security, determining whether it adheres to required security
Context: Within the context of the Trustworthy Systems project, the
security architecture provides the highest level representation of the
This is the first step in the design of a trustworthy system and, most
importantly, it defines the trusted and untrusted components in the
system, and the isolation boundaries between them. Being able to
perform security analyses at this level allows us to analyse the
security of system designs before fully implementing and verifying the
system. Furthermore the architecture and its analysis feed into and
drive subsequent steps in the overall process. In particular it is a
key input into the whole-system assurance activity,
specifying the trusted and untrusted components in the system, as well
as their interconnections and expected security-related properties.
Specific links to other Trustworthy Systems activities are as follows:
- Trustworthy components: the
architecture model maps down to a componentised system with trusted component code, verified glue code and verified system initialisation.
- Information flow: the security
properties and policies are related to information flow.
- Whole-system assurance: the software architecture and security properties are one of the key inputs into the whole system proof.
- Proof Measurement and Estimation: developing and analysing the architecture is part of
the overall process that the project studies.
- Architecture Modelling: We have developed an architecture description language (ADL) called CapArch inspired by xADL. We have developed XML schemas for our language as well as tools to aid in editing and visualising the resulting architectures. We have also developed tools to translate from the architectural model to our analysis models.
- Architecture Analysis: We provide a
separate system analysis model and combine this with the architectural model
to analyse the architecture. We currently use two
approaches to analyse architectures: one based on graph analysis, and
the other based on model checking (for which we use Fitzroy from the Verification Tools and Automation
- Code Generation: The architecture description will drive the implementation of the system, and we expect that much of the framework-related code (e.g., providing isolation and performing communication) will be automatically generated. We target CAmkES and the tools developed in the trustworthy components activity to provide the code generation functionality. We have also developed tools to automatically translate from CapArch ADL to CAmkES ADL.
- Verification Integration: We expect that the system architecture and its analysis will also contribute to the whole-system assurance, both by providing verified framework-related code, verified system initialisation, and by specifying the required properties of the system, and which the whole system must be shown to provide.
- Security and Safety Patterns: We have gathered and catalogued existing security patterns and are analysing their applicability in capability-based systems. We have started formalising relevant patterns and analysing their security and safety properties.
Ihor Kuz, ihor.kuz<at>nicta.com.au
- Ihor Kuz
- Len Bass
- Mark Staples
- Matthew Fernandez
- Paul Rimba
- Sherry Xu
||Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz|
CAmkES glue code semantics
Technical Report, NICTA and UNSW, November, 2013
||Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick|
Towards a verified component platform
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, PA, USA, November, 2013
||Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray|
CAmkES formalisation of a component platform
Technical Report, NICTA and UNSW, November, 2013
||Andreas Bauer, Peter Baumgartner, Diller Martin and Michael Norrish|
Tableaux for verification of data-centric processes
Automated Reasoning with Analytic Tableaux and Related Methods, pp. 28–43, Nancy, France, September, 2013
||Ihor Kuz, Liming Zhu, Len Bass, Mark Staples and Sherry Xu|
An architectural approach for cost effective trustworthy systems
IEEE/IFIP Working Conference on Software Architecture (WICSA), pp. 325–328, Helsinki, Finland, August, 2012