Context: 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. Objective: In this work, we propose an automated formal approach for security analysis of component-based systems with dynamic architectures. Methods: 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. Results: Compared to the state of the art, our results demonstrate an improvement both in the size of systems that can be analyzed and at the time required to complete the analysis. In particular, our incremental analysis is well suited for systems that alter their architectures at runtime. Conclusion: Therefore, this approach is suitable for analyzing the security dynamic component based both statically and at runtime.

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.

Given the increasing complexity of softwareintensive systems as well as the sophistication and high frequency of cyber-attacks, automated and sound approaches to select countermeasures are required to effectively protect software systems. In this paper, we propose a formal architecturecentered approach to analyze the security of a software-intensive component-based system to find cost-efficient countermeasures that 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.

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.

Abstract Correctness of the behavior of an adaptive system during dynamic adaptation is an important challenge to realize correct adaptive systems. Dynamic adaptation refers to changes to both the functionality of the computational entities that comprise a composite system, as well as the structure of their interconnections, in response to variations in the environment, e.g., the load of requests on a server system. In this research, we view the problem of correct structural adaptation as a supervisory control problem and synthesize a reconfiguration controller that guides the behavior of a system during adaptation. The reconfiguration controller observes the system behavior during an adaptation and controls the system behavior by allowing/disallowing actions in a way to ensure that a given property is satisfied and a deadlock is avoided. The system during adaptation is modeled using a graph transition system and properties to be enforced are specified using a graph automaton. We adapt a classical theory of supervisory control for synthesizing a controller for controlling the behavior of a system modeled using graph transition systems. This theory is used to synthesize a controller that can impose both behavioral and structural constraints on the system during an adaptation. We apply a tool that we have implemented to support our approach on a case study involving https servers.

We review and compare three notions of conformance testing for cyber-physical systems. We begin with a review of their underlying semantic models and present conformance-preserving translations between them. We identify the differences in the underlying semantic models and the various design decisions that lead to these substantially different notions of conformance testing. Learning from this exercise, we reflect upon the challenges in designing an "ideal" notion of conformance for cyber-physical systems and sketch a roadmap of future research in this domain.

A separation kernel simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. We present a formal verification of information flow security for a simple separation kernel for ARMv7. Previous work on information flow kernel security leaves communication to be handled by model-external means, and cannot be used to draw conclusions when there is explicit interaction between partitions. We propose a different approach where communication between partitions is made explicit and the information flow is analyzed in the presence of such a channel. Limiting the kernel functionality as much as meaningfully possible, we accomplish a detailed analysis and verification of the system, proving its correctness at the level of the ARMv7 assembly. As a sanity check we show how the security condition is reduced to noninterference in the special case where no communication takes place. The verification is done in HOL4 taking the Cambridge model of ARM as basis, transferring verification tasks on the actual assembly code to an adaptation of the BAP binary analysis tool developed at CMU.