Carolyn Talcott

Benjamin Lion, Farhad Arbab, Carolyn Talcott

We propose a component-based semantic model for Cyber-Physical Systems (CPSs) wherein the notion of a component abstracts the internal details of both cyber and physical processes, to expose a uniform semantic model of their externally observable behaviors expressed as sets of sequences of observations. We introduce algebraic operations on such sequences to model different kinds of component composition. These composition operators yield the externally observable behavior of their resulting composite components through specifications of interactions of the behaviors of their constituent components, as they, e.g., synchronize with or mutually exclude each other's alternative behaviors. Our framework is expressive enough to allow articulation of properties that coordinate desired interactions among composed components within the framework, also as component behavior. We demonstrate the usefulness of our formalism through examples of coordination properties in a CPS consisting of two robots interacting through shared physical resources.

Deborah Shands, Carolyn Talcott

Many damaging cybersecurity attacks are enabled when an attacker can access residual sensitive information (e.g. cryptographic keys, personal identifiers) left behind from earlier computation. Attackers can sometimes use residual information to take control of a system, impersonate a user, or manipulate data. Current approaches to addressing access to residual sensitive information aim to patch individual software or hardware vulnerabilities. While such patching approaches are necessary to mitigate sometimes serious security vulnerabilities in the near term, they cannot address the underlying issue: explicit requirements for adequately eliminating residual information and explicit representations of the erasure capabilities of systems are necessary to ensure that sensitive information is handled as expected. This position paper introduces the concept of intentional forgetting and the capabilities that are needed to achieve it. Intentional forgetting enables software and hardware system designers at every level of abstraction to clearly specify and rigorously reason about the forgetting capabilities required of and provided by a system. We identify related work that may help to illuminate challenges or contribute to solutions and consider conceptual and engineering tradeoffs in implementations of forgetting capabilities. We discuss approaches to modeling intentional forgetting and then modeling the strength of a system's forgetting capability by its resistance to disclosing information to different types of detectors. Research is needed in a variety of domains to advance the theory, specification techniques, system foundations, implementation tools, and methodologies for effective, practical forgetting. We highlight research challenges in several domains and encourage cross-disciplinary collaboration to one day create a robust theory and practice of intentional forgetting.

Max Kanovich, Tajana Ban Kirigin, Vivek Nigam et al.

Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as Cyber-Physical. Time plays a key role in design and analysis of many of these protocols. This paper investigates the foundational differences and the impacts on the analysis when using models with discrete time and models with dense time. We show that there are attacks that can be found by models using dense time, but not when using discrete time. We illustrate this with a novel attack that can be carried out on most Distance Bounding Protocols. In this attack, one exploits the execution delay of instructions during one clock cycle to convince a verifier that he is in a location different from his actual position. We additionally present a probabilistic analysis of this novel attack. As a formal model for representing and analyzing Cyber-Physical properties, we propose a Multiset Rewriting model with dense time suitable for specifying cyber-physical security protocols. We introduce Circle-Configurations and show that they can be used to symbolically solve the reachability problem for our model, and show that for the important class of balanced theories the reachability problem is PSPACE-complete. We also show how our model can be implemented using the computational rewriting tool Maude, the machinery that automatically searches for such attacks.

Vivek Nigam, Carolyn Talcott, Abraão Aires Urquiza

Timed Intruder Models have been proposed for the verification of Cyber-Physical Security Protocols (CPSP) amending the traditional Dolev-Yao intruder to obey the physical restrictions of the environment. Since to learn a message, a Timed Intruder needs to wait for a message to arrive, mounting an attack may depend on where Timed Intruders are. It may well be the case that in the presence of a great number of intruders there is no attack, but there is an attack in the presence of a small number of well placed intruders. Therefore, a major challenge for the automated verification of CPSP is to determine how many Timed Intruders to use and where should they be placed. This paper answers this question by showing it is enough to use the same number of Timed Intruders as the number of participants. We also report on some preliminary experimental results in discovering attacks in CPSP.