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

Abstract

This publication is based on our paper presented at the IEEE International Conference on Software Architecture 2019. Due to their close interconnection with the outside world, cyber-physical systems are vulnerable to information leaks. Accordingly, it is crucial for software engineers to regulate and analyze the flow of information through systems. The microservice architectural style requires engineers to refine the regulations into security policies for the constituent software components. These policies must be composable to secure the information flow from end to end. However, since security is hard to compose, a composition of secure components may lead to an insecure system. In our paper, we enable microservice architectures of cyber-physical systems to be composed securely. First, we provide engineers with a set of architectural well-formedness rules for the refinement of security policies, ensuring composability if the constituent components communicate by message passing. Second, we present a verification technique to analyze whether the real-time message passing of components adheres to their refined security policies. Since the analysis results are securely composable, we assure engineers that a composition of secure components will always lead to a secure system. We evaluated the accuracy of our contributions using an extension of the CoCoME case study.