To reason about and enforce security in dynamic software systems, automated analysis and verification approaches are required. However, such approaches often encounter scalability issues, particularly when employed for runtime analysis, which is necessary in software systems with dynamically changing architectures, such as self-adaptive systems. In this work, we propose an automated formal approach for security analysis of component-based systems with dynamic architectures. This approach leverages formal abstraction and incremental analysis techniques to reduce the complexity of runtime analysis. We have implemented and evaluated our approach against ZNN, a widely known self-adaptive system exemplar. Our experimental results demonstrate the effectiveness of our approach in addressing scalability issues.

In the realm of sound object-oriented program analyses for information-flow control, very few approaches adopt flow-sensitive abstractions of the heap that enable a precise modeling of implicit flows. To tackle this challenge, we advance a new symbolic abstraction approach for modeling the heap in Java-like programs. We use a store-less representation that is parameterized with a family of relations among references to offer various levels of precision based on user preferences. This enables us to automatically infer polymorphic information-flow guards for methods via a co-reachability analysis of a symbolic finite-state system. We instantiate the heap abstraction with three different families of relations. We prove the soundness of our approach and compare the precision and scalability obtained with each instantiated heap domain by using the IFSpec benchmarks and real-life applications.

Given the increasing complexity of software-intensive systems as well as the sophistication and high frequencyof cyber-attacks, automated and sound approaches to select countermeasures are required to effectively protect softwaresystems. In this paper, we propose a formal architecture-centered approach to analyze the security of a software-intensive component-based system to find cost-efficient countermeasuresthat consider both the system architecture and its behavior. We evaluate our approach by applying it on a case study.

In this paper, we propose a sound method to synthesize a permissive monitor using boolean supervisory controller synthesis that observes a Java program at certain checkpoints, predicts information flow violations and applies suitable countermeasures to prevent violations. We introduce an approach for modeling heap and information flow via heap. To improve permissiveness, we train the monitor and remove false positives by executing the program along with its executable model. If a security violation is detected, the user can define sound countermeasures, including declassification to apply in checkpoints. We prove that the monitored program ensures localized delimited release in case of declassifying information and termination-insensitive noninterference in case of no declassification. We implement a tool to automate the whole process and generate a monitor. Our method is evaluated by applying it on the Droidbench benchmark and one real-life Android application.

This chapter targets a better understanding of the compositionality of analyses, including different forms of compositionality and specific conditions of composition. Analysis involves models, contexts, and properties. These are all expressed in languages with their own semantics. For a successful composition of analyses, it is therefore important to compose models as well as the underlying languages. We aim to develop a better understanding of what is needed to answer questions such as “When I want to compose two or more analyses, what do I need to take into account?” We describe the elements impacting analysis compositionality, the relation of these elements to analysis, and how composition of analysis relates to compositionality of these elements.

This core chapter addresses Challenge 1 introduced in Chap. 3 of this book (the theoretical foundations—how to compose the underlying languages, models, and analyses).

As threats to computer security become more common, complex and frequent, systems that canautomatically protect themselves from attacks are imminently needed. In this paper, we proposea formal approach to achieve self-protection by performing security analysis on self-adaptive systems, taking the adaptation process into account. We use probabilistic model checking to quantitatively analyze adaptation security, rank the strategies available and select the most secure one to apply in the system. We have incorporated our approach in Rainbow which is a framework to develop architecture-based self-adaptive systems.To evaluate our approach's effectiveness, we applied it on two  case studies: a simple document storage system and ZNN, a well known self-adaptive exemplar. The results show that applying our approachcan guarantee a reasonable degree of security, both during and after adaptation.

This chapter gives an introduction to the key concepts and terminology relevant for model-based analysis tools and their composition. In the first half of the chapter, we introduce concepts relevant for modelling and composition of models and modelling languages. The second half of the chapter then focuses on concepts relevant to analysis and analysis composition. This chapter, thus, lays the foundations for the remainder of the book, ensuring that readers can go through the book as a coherent piece.

In recent years, it has become more challenging for organizations to assess the security risks of their assets properly, as more vulnerabilities are discovered, exploited, and weaponized. Further, attackers usually use complex multi-stage attack strategies to compromise a system and achieve their goals by exploiting several vulnerabilities.The number of affected assets and the strategy used to create the compromises by the threat actor will often dictate the costs and damages to the organization.When performing risk analysis, in addition to existing vulnerabilities, it is important, but often neglected, to consider the criticality of the data residing in the vulnerable asset. However, graphical threat modeling techniques often do not offer suitable toolsfor this type of analysis.In this paper, we propose a class of security risk metrics to estimate the cost of an attack that considers the criticality of data in addition to the dependencies among vulnerabilities. Our metrics are based on graphical modeling techniques in which we incorporate data criticality. We applied our approach to a real-life case study and obtained promising results.

Modern software systems are decentralized, distributed, and dynamic, and consequently, require decentralized mechanisms to enforce security. In this paper, we propose an adaptive approach using a combination of decentralized information flow control (DIFC) mechanisms, trust-based methods and decentralized control architectures to enforce security in open distributed systems. In our approach, adaptivity mitigates two aspects of the system dynamics that cause uncertainty: the ever-changing nature of trust and system openness. We formalize our trust-aware DIFC model and instantiate two decentralized control architectures to implement and evaluate it. We evaluate the effectiveness and performance of our method and decentralized control architectures on two case studies.

Modern software systems and their corresponding architectures are increasingly decentralized, distributed, and dynamic. As a consequence, decentralized mechanisms are required to ensure security in such architectures. Decentralized Information Flow Control (DIFC) is a mechanism to control information flow in distributed systems. This article presents and discusses several improvements to an adaptive decentralized information flow approach that incorporates trust for decentralized systems to provide security. Adaptive Trust-Aware Decentralized Information Flow (AT-DIFC+) combines decentralized information flow control mechanisms, trust-based methods, and decentralized control architectures to control and enforce information flow in an open, decentralized system. We strengthen our approach against newly discovered attacks and provide additional information about its reconfiguration, decentralized control architectures, and reference implementation. We evaluate the effectiveness and performance of AT-DIFC+ on two case studies and perform additional experiments and to gauge the mitigations’ effectiveness against the identified attacks.