Security Architecture is one activity of the Trustworthy Systems project.
Aim: To model and analyse the software architectures of secure systems.
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 policies.
Context: Within the context of the Trustworthy Systems project, the security architecture provides the highest level representation of the system.
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 team).
- 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
|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
Building high assurance secure applications using security patterns for capability-based platforms
International Conference on Software Engineering, pp. 4, San Francisco, USA, May, 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