Component-Based Refinement and Verification of Information-Flow Security Policies for Cyber-Physical Microservice Architectures
Title | Component-Based Refinement and Verification of Information-Flow Security Policies for Cyber-Physical Microservice Architectures |
Publication Type | Conference Paper |
Year of Publication | 2019 |
Authors | Gerking, Christopher, Schubert, David |
Conference Name | 2019 IEEE International Conference on Software Architecture (ICSA) |
Date Published | mar |
Publisher | IEEE |
ISBN Number | 978-1-7281-0528-4 |
Keywords | CoCoME case study, Collaboration, Computer architecture, cyber-physical microservice architectures, Cyber-physical systems, formal specification, individual microservices, information flow, information leaks, Information systems, information-flow security policies, macro-level policy, macro-level security policy, message passing, microservice architectural style, microservices, Perturbation methods, Policy Based Governance, policy-based governance, protocol verification, Protocols, pubcrawl, real-time behavior, resulting microlevel policies, security, security of data, security restrictions, Servers, service-oriented architecture, software architects |
Abstract | Since cyber-physical systems are inherently vulnerable to information leaks, software architects need to reason about security policies to define desired and undesired information flow through a system. The microservice architectural style requires the architects to refine a macro-level security policy into micro-level policies for individual microservices. However, when policies are refined in an ill-formed way, information leaks can emerge on composition of microservices. Related approaches to prevent such leaks do not take into account characteristics of cyber-physical systems like real-time behavior or message passing communication. In this paper, we enable the refinement and verification of information-flow security policies for cyber-physical microservice architectures. We provide architects with a set of well-formedness rules for refining a macro-level policy in a way that enforces its security restrictions. Based on the resulting micro-level policies, we present a verification technique to check if the real-time message passing of microservices is secure. In combination, our contributions prevent information leaks from emerging on composition. We evaluate the accuracy of our approach using an extension of the CoCoME case study. |
URL | https://ieeexplore.ieee.org/document/8703909 |
DOI | 10.1109/ICSA.2019.00015 |
Citation Key | gerking_component-based_2019 |
- microservices
- software architects
- service-oriented architecture
- Servers
- security restrictions
- security of data
- security
- resulting microlevel policies
- real-time behavior
- pubcrawl
- Protocols
- protocol verification
- policy-based governance
- Policy Based Governance
- Perturbation methods
- CoCoME case study
- microservice architectural style
- message passing
- macro-level security policy
- macro-level policy
- information-flow security policies
- Information systems
- information leaks
- Information Flow
- individual microservices
- Formal Specification
- cyber-physical systems
- cyber-physical microservice architectures
- computer architecture
- collaboration