Model-Driven Specification and Analysis of Confidentiality in Component-Based Systems

Many software systems have to be designed and developed in a way that guarantees that specific information remains confidential with respect to considered adversaries. Such guarantees depend on the internal information flow inside individual components and the system architecture, e.g., the deployment on hardware nodes and properties of their communication links. Therefore, we propose a novel architecture-driven approach for specifying and analyzing the confidentiality of information processed by component-based systems. It includes an architectural analysis that is able to infer leaks of confidential information from abstract architecture models, adversary models, and confidentiality specifications. Our approach supports re-usability of components and specification parts across systems as well as specifications with custom labels, e.g., accessibility of hardware and service interfaces. Additionally, our information flow specifications for components are compositional and supported by tools for non-interference verification on source code level. In two case studies, we show how our specification approach is applied and how the architectural analysis is able to detect information leaks of a system in an early design phase.