Security Architecture

Security Architecture was an activity of Trustworthy Systems.

• Aim: To model and analyse the software architectures of secure systems.

• Latest news:

  • 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 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 whole-system assurance, 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.

Research Activities

• 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.
• 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.

People

Publications

		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