Karen Rudie

In this paper, we study a security problem of protecting secrets in distributed systems. Specifically, we employ discrete-event systems to describe the structure and behaviour of distributed systems, in which global secret information is separated into pieces and stored in local component agents. The goal is to prevent such secrets from being exposed to intruders by imposing appropriate protection measures. This problem is formulated as to ensure that at least one piece of every distributed global secret is secured by a required number of protections, while the overall cost to apply protections is minimum. We first characterize the solvability of this security problem by providing a necessary and sufficient condition, and then develop an algorithm to compute a solution based on the supervisory control theory of discrete-event systems. Finally, we illustrate the effectiveness of our solution with an example system comprising distributed databases.

Solutions to decentralized discrete-event systems problems are characterized by the way local decisions are fused to yield a global decision. A fusion rule is colloquially called an architecture. Current approaches do not provide a direct way to compare existing architectures. Determining whether an architecture is more permissive than another architecture had relied on producing examples ad hoc and on individual inspiration that puts the conditions for solvability in each architecture into some form that admits comparison. In response to these research efforts, a method based on morphisms between graphs has been extracted to yield a uniform approach to compare the permissiveness of the architectures.

An epistemic model for decentralized discrete-event systems with non-binary control is presented. This framework combines existing work on conditional control decisions with existing work on formal reasoning about knowledge in discrete-event systems. The novelty in the model presented is that the necessary and sufficient conditions for problem solvability encapsulate the actions that supervisors must take. This direct coupling between knowledge and action -- in a formalism that mimics natural language -- makes it easier, when the problem conditions fail, to determine how the problem requirements should be revised.

A syntactic model is presented for the specification of finite-state synchronous digital logic systems with complex input/output interfaces, which control the flow of data between opaque computational elements, and for the composition of compatible systems to form closed-loop systems with no inputs or outputs. This model improves upon similar existing models with a novel approach to specifying input and output ports in a way which is uniform and symmetric. An automaton model is also presented for encoding arbitrary computational processes, and an algorithm is presented to generate an automaton representation of a closed-loop system. Using the automaton model, the problem of timing-agnostic verification of closed-loop systems against a desired behavioural specification, encoded as the similarity of closed-loop systems in terms of the set of computations performed, is shown to be decidable. The relationship between the models and real-world implementations of systems is discussed.

In a truly decentralized system, agents must be able to make decisions based on their observations, without reliance on a centralized coordinator or fusion rule. A condition, called at least one can tell , is developed that characterizes when decentralized agents can determine whether behavior generated by a system is good (i.e., legal) or bad (i.e., illegal). It is shown that the at least one can tell condition is decidable and when the condition holds, finite-state decentralized observers can be constructed. Links between the at least one can tell condition and decentralized discrete-event systems are also made.