The ability to exchange data while maintaining sovereignty is fundamental to emerging decentralized data-driven ecosystems. Data sovereignty refers to the entity's capability to be self-determined concerning data usage. As such, a data usage control system (UCON) is critical for sovereignty. UCON, a generalization of attribute-based access control, enforces continuous authorization, allowing attribute mutability after access is granted. In theory, UCON comprises a policy language to express constraints and obligations of data usage, and a technology to evaluate and enforce them. In practice, realizing the above is challenging and poses trust concerns. Partly, this is due to the complexity of UCON (continuous authorization, obligations) and the advanced usage constraints (stemming from, e.g., regulations or business contracts) combined with the decentralized nature of data ecosystems that allow different actors (e.g., data provider, security engineers) to author policies, and operate UCON. To that end, we propose to aid actors with automated policy analysis and verification methods. We present a new policy analysis method based on the combination of symbolic execution for policy evaluation and SMT solving to compute concrete scenarios answering queries on the policies. Our approach supports symbolic queries, where attribute values may be concrete values, a range of values, or symbolic variables. We also propose a monitoring approach using RTLola tool to verify the correctness of UCON's behavior in terms of decisions, obligations, and user-specified properties. To monitor obligations, we define their essential parameters and show how to monitor their fulfillment based on the configuration. We also present eight templates that allow users to generate the most important properties for monitoring UCON.

Automotive cyber-physical systems consist of multiple control subsystems working under resource limitations, and the trend is to run the corresponding control tasks on a shared platform. The resource requirements of the tasks are usually variable at runtime due to the uncertainties in the environment, necessitating some kinds of adaptation to deal with the resource limitations. Such adaptations may positively or negatively affect the control performance of several subsystems. Since there might be some thresholds on the control performances as quality constraints, this matter should be considered carefully to avoid any quality attribute constraint violation. This article proposes a scalable control performance constraint verification method for such a system that works based on a feedback scheduler. The scalability is the result of a control-aware pruning method. In case of a constraint violation, the designer may change the system configuration and perform re-verification. Our evaluations show that the proposed method scales well while preserving the verification soundness.

Modern system architectures require sophisticated access and usage control mechanisms. The need stems from demanding requirements for security, data sovereignty and privacy regulations, as well as the challenges presented by architectural approaches like zero trust networking. Usage control systems provide one approach to encapsulate and manage the complexities related to access and usage control. In order to trust a usage control system, it is essential to ensure that usage control policies express the intended properties and are enforced correctly. To achieve this, we need a precise specification of the intended behavior of a usage control system. For attribute-based access control, the XACML standard is a sufficient specification of the behavior of policies. Usage control models, such as UCON, extend access control with features for continuous authorization based on mutability of attribute values. This adds significant complexity to the problem of specifying the intended behavior. In this paper, we identify challenges with specifying a practical usage control system regarding continuous control, obligations, and concurrency aspects. We describe an approach to specifying the UCON+ model of Dimitrakos et al. and outline an implementation of the specification with Answer Set Programming.

Specification synthesis is the process of deriving a model from the input-output traces of a system. It is used extensively in test design, reverse engineering, and system identification. One type of the resulting artifact of this process for cyber-physical systems is hybrid automata. They are intuitive, precise, tool independent, and at a high level of abstraction, and can model systems with both discrete and continuous variables. In this article, we propose a new technique for synthesizing hybrid automaton from the input-output traces of a non-linear cyber-physical system. Similarity detection in non-linear behaviors is the main challenge for extracting such models. We address this problem by utilizing the Dynamic Time Warping technique. Our approach is passive, meaning that it does not need interaction with the system during automata synthesis from the logged traces; and online, which means that each input/output trace is used only once in the procedure. In other words, each new trace can be used to improve the already synthesized automaton. We evaluated our algorithm in one industrial and two simulated case studies. The accuracy of the derived automata shows promising results.

In this paper, we propose an automated technique for synthesizing fault-tolerant distributed protocols from their fault-intolerant version, where the number of processes is parameterized. A fault-tolerant protocol is one that ensures constant satisfaction of safety and liveness specifications even in the presence of faults. Although the parametrized synthesis problem is undecidable in general, we could propose a sound algorithm for this challenging problem. Our synthesis algorithm utilizes counter abstraction to construct a finite representation of the state space. Then, it performs fixpoint calculations to compute and exclude states that violate the safety/liveness specifications in the presence of faults. We demonstrate the effectiveness of our algorithm by synthesizing fault-tolerant distributed protocols for well-known problems, such as reliable broadcast and a simplified version of Byzantine agreement in a matter of seconds.

Self-stabilization in distributed systems is a technique to guarantee convergence to a set of legitimate states without external intervention when a transient fault or bad initialization occurs. Recently, there has been a surge of efforts in designing techniques for automated synthesis of self-stabilizing algorithms that are correct by construction. Most of these techniques, however, are not parameterized, meaning that they can only synthesize a solution for a fixed and predetermined number of processes. In this paper, we report a breakthrough in parameterized synthesis of self-stabilizing algorithms in symmetric rings. First, we develop tight cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimates states. We also develop a sufficient condition for convergence in silent self-stabilizing systems. Since some of our cutoffs grow with the size of local state space of processes, we also present an automated technique that significantly increases the scalability of synthesis in symmetric networks. Our technique is based on SMT-solving and incorporates a loop of synthesis and verification guided by counterexamples. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems.

In this article, we focus on efficient synthesis of fault-tolerant timed models from their fault-intolerant version. Although the complexity of the synthesis problem is known to be polynomial time in the size of the time-abstract bisimulation of the input model, the state of the art currently lacks synthesis algorithms that can be efficiently implemented. This is in part due to the fact that synthesis is in general a challenging problem and its complexity is significantly magnified in the context of timed systems. We propose an algorithm that takes as input a timed automaton, a set of fault actions, and a set of safety and bounded-time response properties, and utilizes a space-efficient symbolic representation of the timed automaton (called zone graph) to synthesize a fault-tolerant timed automaton as output. The output automaton satisfies strict phased recovery, where it is guaranteed that the output model behaves similarly to the input model in the absence of faults and in the presence of faults, fault recovery is achieved in two phases, each satisfying certain safety and timing constraints.

A self-stabilizing system is one that converges to a legitimate state from any arbitrary state. Such an arbitrary state may be reachable due to wrong initialization or the occurrence of transient faults. Average recovery time of self-stabilizing systems is a key factor in evaluating their performance, especially in the domain of network and robotic protocols. This paper introduces a groundbreaking result on automated repair and synthesis of self-stabilizing protocols whose average recovery time is required to satisfy certain constraints. We show that synthesizing and repairing weak-stabilizing protocols under average recovery time constraints is NP-complete. To cope with the exponential complexity (unless P = NP), we propose a polynomial-time heuristic.

A self-stabilizing system is one that guarantees reaching a set of legitimate states from any arbitrary initial state. Designing distributed self-stabilizing protocols is often a complex task and developing their proof of correctness is known to be significantly more tedious. In this article, we propose an SMT-based method that automatically synthesizes a self-stabilizing protocol, given the network topology of distributed processes and description of the set of legitimate states. Our method can synthesize synchronous, asynchronous, symmetric, and asymmetric protocols for two types of stabilization, namely weak and strong . We also report on successful automated synthesis of a set of well-known distributed stabilizing protocols such as Dijkstra’s token ring, distributed maximal matching, graph coloring, and mutual exclusion in anonymous networks.

Model Driven Engineering (MDE) is a progressive area that tries to fill the gap between problem definition and software development. There are many modeling languages proposed for use in MDE. A challenge is how to provide automatic analysis for these models without having to create new analyzers for each different language. In this research, we tackle this problem for a family of modeling languages using a semantically configurable model translation framework.