Visible to the public Component-Based Refinement and Verification of Information-Flow Security Policies for Cyber-Physical Microservice Architectures

TitleComponent-Based Refinement and Verification of Information-Flow Security Policies for Cyber-Physical Microservice Architectures
Publication TypeConference Paper
Year of Publication2019
AuthorsGerking, Christopher, Schubert, David
Conference Name2019 IEEE International Conference on Software Architecture (ICSA)
Date Publishedmar
PublisherIEEE
ISBN Number978-1-7281-0528-4
KeywordsCoCoME 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.

URLhttps://ieeexplore.ieee.org/document/8703909
DOI10.1109/ICSA.2019.00015
Citation Keygerking_component-based_2019