-
Dialects for CoAP-like Messaging Protocols
Authors:
Carolyn Talcott
Abstract:
Messaging protocols for resource limited systems such as distributed IoT systems are often vulnerable to attacks due to security choices made to conserve resources such as time, memory, or bandwidth. For example, use of secure layers such as DTLS are resource expensive and can sometimes cause service disruption. Protocol dialects are intended as a light weight, modular mechanism to provide selecte…
▽ More
Messaging protocols for resource limited systems such as distributed IoT systems are often vulnerable to attacks due to security choices made to conserve resources such as time, memory, or bandwidth. For example, use of secure layers such as DTLS are resource expensive and can sometimes cause service disruption. Protocol dialects are intended as a light weight, modular mechanism to provide selected security guarantees, such as authentication. In this report we study the CoAP messaging protocol and define two attack models formalizing different vulnerabilities. We propose a generic dialect for CoAP messaging. The CoAP protocol, dialect, and attack models are formalized in the rewriting logic system Maude. A number of case studies are reported illustrating vulnerabilities and effects of applying the dialect. We also prove (stuttering) bisimulations between CoAP messaging applications and dialected versions, thus ensuring that dialecting preserves LTL properties (without Next) of CoAP applications.
△ Less
Submitted 21 May, 2024;
originally announced May 2024.
-
Technical Report: Time-Bounded Resilience
Authors:
Tajana Ban Kirigin,
Jesse Comer,
Max Kanovich,
Andre Scedrov,
Carolyn Talcott
Abstract:
Most research on formal system design has focused on optimizing various measures of efficiency. However, insufficient attention has been given to the design of systems optimizing resilience, the ability of systems to adapt to unexpected changes or adversarial disruptions. In our prior work, we formalized the intuitive notion of resilience as a property of cyber-physical systems by using a multiset…
▽ More
Most research on formal system design has focused on optimizing various measures of efficiency. However, insufficient attention has been given to the design of systems optimizing resilience, the ability of systems to adapt to unexpected changes or adversarial disruptions. In our prior work, we formalized the intuitive notion of resilience as a property of cyber-physical systems by using a multiset rewriting language with explicit time. In the present paper, we study the computational complexity of a formalization of time-bounded resilience problems for the class of $η$-simple progressing planning scenarios, where, intuitively, it is simple to check that a system configuration is critical, and only a finite number of actions can be carried out in a bounded time period. We show that, in the time-bounded model with $n$ (potentially adversarially chosen) updates, the corresponding time-bounded resilience problem for this class of systems is complete for the $Σ^P_{2n+1}$ class of the polynomial hierarchy, PH. To support the formal models and complexity results, we perform automated experiments for time-bounded verification using the rewriting logic tool Maude.
△ Less
Submitted 2 June, 2024; v1 submitted 10 January, 2024;
originally announced January 2024.
-
Technical-Report: Automating Recoverability Proofs for Cyber-Physical Systems with Runtime Assurance Architectures
Authors:
Vivek Nigam,
Carolyn Talcott
Abstract:
Cyber-physical systems (CPSes), such as autonomous vehicles, use sophisticated components like ML-based controllers. It is difficult to provide evidence about the safe functioning of such components. To overcome this problem, Runtime Assurance Architecture (RTA) solutions have been proposed. The \RAP's decision component evaluates the system's safety risk and whenever the risk is higher than accep…
▽ More
Cyber-physical systems (CPSes), such as autonomous vehicles, use sophisticated components like ML-based controllers. It is difficult to provide evidence about the safe functioning of such components. To overcome this problem, Runtime Assurance Architecture (RTA) solutions have been proposed. The \RAP's decision component evaluates the system's safety risk and whenever the risk is higher than acceptable the RTA switches to a safety mode that, for example, activates a controller with strong evidence for its safe functioning. In this way, RTAs increase CPS runtime safety and resilience by recovering the system from higher to lower risk levels. The goal of this paper is to automate recovery proofs of CPSes using RTAs. We first formalize the key verification problems, namely, the decision sampling-time adequacy problem and the time-bounded recoverability problem. We then demonstrate how to automatically generate proofs for the proposed verification problems using symbolic rewriting modulo SMT. Automation is enabled by integrating the rewriting logic tool (Maude), which generates sets of non-linear constraints, with an SMT-solver (Z3) to produce proofs
△ Less
Submitted 23 April, 2023;
originally announced April 2023.
-
A Formal Framework for Distributed Cyber-Physical Systems
Authors:
Benjamin Lion,
Farhad Arbab,
Carolyn Talcott
Abstract:
Composition is an important feature of a specification language, as it enables the design of a complex system in terms of a product of its parts. Decomposition is equally important in order to reason about structural properties of a system. Usually, however, a system can be decomposed in more than one way, each optimizing for a different set of criteria. We extend an algebraic component-based mode…
▽ More
Composition is an important feature of a specification language, as it enables the design of a complex system in terms of a product of its parts. Decomposition is equally important in order to reason about structural properties of a system. Usually, however, a system can be decomposed in more than one way, each optimizing for a different set of criteria. We extend an algebraic component-based model for cyber-physical systems to reason about decomposition. In this model, components compose using a family of algebraic products, and decompose, under some conditions, given a corresponding family of division operators. We use division to specify invariant of a system of components, and to model desirable updates. We apply our framework to design a cyber-physical system consisting of robots moving on a shared field, and identify desirable updates using our division operator.
△ Less
Submitted 3 July, 2022;
originally announced July 2022.
-
A Rewriting Framework for Interacting Cyber-Physical Agents
Authors:
Benjamin Lion,
Farhad Arbab,
Carolyn Talcott
Abstract:
The analysis of cyber-physical systems (CPS) is challenging due to the large state space and the continuous changes occurring in their constituent parts. Design practices favor modularity to help reducing this complexity. In a previous work, we proposed a discrete semantic model for CPS that captures both cyber and physical aspects as streams of discrete observations, which ultimately form the beh…
▽ More
The analysis of cyber-physical systems (CPS) is challenging due to the large state space and the continuous changes occurring in their constituent parts. Design practices favor modularity to help reducing this complexity. In a previous work, we proposed a discrete semantic model for CPS that captures both cyber and physical aspects as streams of discrete observations, which ultimately form the behavior of a component. This semantic model is denotational and compositional, where each composition operator algebraically models an interaction between a pair of components. In this paper, we propose a specification of components as rewrite systems. The specification is operational and executable, and we study conditions for its semantics as components to be compositional. We demonstrate our framework by modeling a coordination of robots moving on a shared field. We show that our system of robots can be coordinated by a protocol in order to exhibit a desired emerging behavior. We use an implementation of our framework in Maude to give practical results.
△ Less
Submitted 2 August, 2022; v1 submitted 8 June, 2022;
originally announced June 2022.
-
Runtime Composition Of Systems of Interacting Cyber-Physical Components
Authors:
Benjamin Lion,
Farhad Arbab,
Carolyn Talcott
Abstract:
We introduce a transition system based specification of cyber-physical systems whose semantics is compositional with respect to a family of algebraic products. We give sufficient conditions for execution of a product to be correctly implemented by a lazy expansion of the product construction. The transition system algebra is implemented in the Maude rewriting logic system, and we report a simple c…
▽ More
We introduce a transition system based specification of cyber-physical systems whose semantics is compositional with respect to a family of algebraic products. We give sufficient conditions for execution of a product to be correctly implemented by a lazy expansion of the product construction. The transition system algebra is implemented in the Maude rewriting logic system, and we report a simple case study illustrating compositional specification.
△ Less
Submitted 25 May, 2022;
originally announced May 2022.
-
A Semantic Model for Interacting Cyber-Physical Systems
Authors:
Benjamin Lion,
Farhad Arbab,
Carolyn Talcott
Abstract:
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 compo…
▽ More
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.
△ Less
Submitted 1 October, 2021;
originally announced October 2021.
-
Intentional Forgetting
Authors:
Deborah Shands,
Carolyn Talcott
Abstract:
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 in…
▽ More
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.
△ Less
Submitted 17 June, 2021;
originally announced June 2021.
-
On the Complexity of Verification of Time-Sensitive Distributed Systems: Technical Report
Authors:
Max Kanovich,
Tajana Ban Kirigin,
Vivek Nigam,
Andre Scedrov,
Carolyn Talcott
Abstract:
This paper develops a Multiset Rewriting language with explicit time for the specification and analysis of Time-Sensitive Distributed Systems (TSDS). Goals are often specified using explicit time constraints. A good trace is an infinite trace in which the goals are satisfied perpetually despite possible interference from the environment. In our previous work (FORMATS 2016), we discussed two desira…
▽ More
This paper develops a Multiset Rewriting language with explicit time for the specification and analysis of Time-Sensitive Distributed Systems (TSDS). Goals are often specified using explicit time constraints. A good trace is an infinite trace in which the goals are satisfied perpetually despite possible interference from the environment. In our previous work (FORMATS 2016), we discussed two desirable properties of TSDSes, realizability (there exists a good trace) and survivability (where, in addition, all admissible traces are good). Here we consider two additional properties, recoverability (all compliant traces do not reach points-of-no-return) and reliability (the system can always continue functioning using a good trace). Following (FORMATS 2016), we focus on a class of systems called Progressing Timed Systems (PTS), where intuitively only a finite number of actions can be carried out in a bounded time period. We prove that for this class of systems the properties of recoverability and reliability coincide and are PSPACE-complete. Moreover, if we impose a bound on time (as in bounded model-checking), we show that for PTS the reliability property is in the $Π_2^p$ class of the polynomial hierarchy, a subclass of PSPACE. We also show that the bounded survivability is both NP-hard and coNP-hard.
△ Less
Submitted 14 September, 2021; v1 submitted 7 May, 2021;
originally announced May 2021.
-
Programming and Symbolic Computation in Maude
Authors:
Francisco Durán,
Steven Eker,
Santiago Escobar,
Narciso Martí-Oliet,
José Meseguer,
Rubén Rubio,
Carolyn Talcott
Abstract:
Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories. Maude has also a formal environment of verification tools. Symbolic computation is a powerful technique for reasoning about the correctness of concurr…
▽ More
Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories. Maude has also a formal environment of verification tools. Symbolic computation is a powerful technique for reasoning about the correctness of concurrent systems and for increasing the power of formal tools. We present several new symbolic features of Maude that enhance formal reasoning about Maude programs and the effectiveness of formal tools. They include: (i) very general unification modulo user-definable equational theories, and (ii) symbolic reachability analysis of concurrent systems using narrowing. The paper does not focus just on symbolic features: it also describes several other new Maude features, including: (iii) Maude's strategy language for controlling rewriting, and (iv) external objects that allow flexible interaction of Maude object-based concurrent systems with the external world. In particular, meta-interpreters are external objects encapsulating Maude interpreters that can interact with many other objects. To make the paper self-contained and give a reasonably complete language overview, we also review the basic Maude features for equational rewriting and rewriting with rules, Maude programming of concurrent object systems, and reflection. Furthermore, we include many examples illustrating all the Maude notions and features described in the paper.
△ Less
Submitted 18 October, 2019;
originally announced October 2019.
-
Transcriptional Response of SK-N-AS Cells to Methamidophos
Authors:
Akos Vertes,
Albert-Baskar Arul,
Peter Avar,
Andrew R. Korte,
Lida Parvin,
Ziad J. Sahab,
Deborah I. Bunin,
Merrill Knapp,
Denise Nishita,
Andrew Poggio,
Mark-Oliver Stehr,
Carolyn L. Talcott,
Brian M. Davis,
Christine A. Morton,
Christopher J. Sevinsky,
Maria I. Zavodszky
Abstract:
Transcriptomics response of SK-N-AS cells to methamidophos (an acetylcholine esterase inhibitor) exposure was measured at 10 time points between 0.5 and 48 h. The data was analyzed using a combination of traditional statistical methods and novel machine learning algorithms for detecting anomalous behavior and infer causal relations between time profiles. We identified several processes that appear…
▽ More
Transcriptomics response of SK-N-AS cells to methamidophos (an acetylcholine esterase inhibitor) exposure was measured at 10 time points between 0.5 and 48 h. The data was analyzed using a combination of traditional statistical methods and novel machine learning algorithms for detecting anomalous behavior and infer causal relations between time profiles. We identified several processes that appeared to be upregulated in cells treated with methamidophos including: unfolded protein response, response to cAMP, calcium ion response, and cell-cell signaling. The data confirmed the expected consequence of acetylcholine buildup. In addition, transcripts with potentially key roles were identified and causal networks relating these transcripts were inferred using two different computational methods: Siamese convolutional networks and time warp causal inference. Two types of anomaly detection algorithms, one based on Autoencoders and the other one based on Generative Adversarial Networks (GANs), were applied to narrow down the set of relevant transcripts.
△ Less
Submitted 10 August, 2019;
originally announced August 2019.
-
Probabilistic Approximate Logic and its Implementation in the Logical Imagination Engine
Authors:
Mark-Oliver Stehr,
Minyoung Kim,
Carolyn L. Talcott,
Merrill Knapp,
Akos Vertes
Abstract:
In spite of the rapidly increasing number of applications of machine learning in various domains, a principled and systematic approach to the incorporation of domain knowledge in the engineering process is still lacking and ad hoc solutions that are difficult to validate are still the norm in practice, which is of growing concern not only in mission-critical applications.
In this note, we introd…
▽ More
In spite of the rapidly increasing number of applications of machine learning in various domains, a principled and systematic approach to the incorporation of domain knowledge in the engineering process is still lacking and ad hoc solutions that are difficult to validate are still the norm in practice, which is of growing concern not only in mission-critical applications.
In this note, we introduce Probabilistic Approximate Logic (PALO) as a logic based on the notion of mean approximate probability to overcome conceptual and computational difficulties inherent to strictly probabilistic logics. The logic is approximate in several dimensions. Logical independence assumptions are used to obtain approximate probabilities, but by averaging over many instances of formulas a useful estimate of mean probability with known confidence can usually be obtained. To enable efficient computational inference, the logic has a continuous semantics that reflects only a subset of the structural properties of classical logic, but this imprecision can be partly compensated by richer theories obtained by classical inference or other means. Computational inference, which refers to the construction of models and validation of logical properties, is based on Stochastic Gradient Descent (SGD) and Markov Chain Monte Carlo (MCMC) techniques and hence another dimension where approximations are involved.
We also present the Logical Imagination Engine (LIME), a prototypical implementation of PALO based on TensorFlow. Albeit not limited to the biological domain, we illustrate its operation in a quite substantial bioinformatics machine learning application concerned with network synthesis and analysis in a recent DARPA project.
△ Less
Submitted 25 July, 2019;
originally announced July 2019.
-
Learning Causality: Synthesis of Large-Scale Causal Networks from High-Dimensional Time Series Data
Authors:
Mark-Oliver Stehr,
Peter Avar,
Andrew R. Korte,
Lida Parvin,
Ziad J. Sahab,
Deborah I. Bunin,
Merrill Knapp,
Denise Nishita,
Andrew Poggio,
Carolyn L. Talcott,
Brian M. Davis,
Christine A. Morton,
Christopher J. Sevinsky,
Maria I. Zavodszky,
Akos Vertes
Abstract:
There is an abundance of complex dynamic systems that are critical to our daily lives and our society but that are hardly understood, and even with today's possibilities to sense and collect large amounts of experimental data, they are so complex and continuously evolving that it is unlikely that their dynamics will ever be understood in full detail. Nevertheless, through computational tools we ca…
▽ More
There is an abundance of complex dynamic systems that are critical to our daily lives and our society but that are hardly understood, and even with today's possibilities to sense and collect large amounts of experimental data, they are so complex and continuously evolving that it is unlikely that their dynamics will ever be understood in full detail. Nevertheless, through computational tools we can try to make the best possible use of the current technologies and available data. We believe that the most useful models will have to take into account the imbalance between system complexity and available data in the context of limited knowledge or multiple hypotheses. The complex system of biological cells is a prime example of such a system that is studied in systems biology and has motivated the methods presented in this paper. They were developed as part of the DARPA Rapid Threat Assessment (RTA) program, which is concerned with understanding of the mechanism of action (MoA) of toxins or drugs affecting human cells. Using a combination of Gaussian processes and abstract network modeling, we present three fundamentally different machine-learning-based approaches to learn causal relations and synthesize causal networks from high-dimensional time series data. While other types of data are available and have been analyzed and integrated in our RTA work, we focus on transcriptomics (that is gene expression) data obtained from high-throughput microarray experiments in this paper to illustrate capabilities and limitations of our algorithms. Our algorithms make different but overall relatively few biological assumptions, so that they are applicable to other types of biological data and potentially even to other complex systems that exhibit high dimensionality but are not of biological nature.
△ Less
Submitted 6 May, 2019;
originally announced May 2019.
-
Compliance in Real Time Multiset Rewriting Models
Authors:
Max Kanovich,
Tajana Ban Kirigin,
Vivek Nigam,
Andre Scedrov,
Carolyn Talcott
Abstract:
The notion of compliance in Multiset Rewriting Models (MSR) has been introduced for untimed models and for models with discrete time. In this paper we revisit the notion of compliance and adapt it to fit with additional nondeterminism specific for dense time domains. Existing MSR with dense time are extended with critical configurations and non-critical traces, that is, traces involving no critica…
▽ More
The notion of compliance in Multiset Rewriting Models (MSR) has been introduced for untimed models and for models with discrete time. In this paper we revisit the notion of compliance and adapt it to fit with additional nondeterminism specific for dense time domains. Existing MSR with dense time are extended with critical configurations and non-critical traces, that is, traces involving no critical configurations. Complexity of related {\em non-critical reachability problem} is investigated. Although this problem is undecidable in general, we prove that for balanced MSR with dense time the non-critical reachability problem is PSPACE-complete.
△ Less
Submitted 12 November, 2018;
originally announced November 2018.
-
Reasoning about effects: from lists to cyber-physical agents
Authors:
Ian A. Mason,
Carolyn L. Talcott
Abstract:
Theories for reasoning about programs with effects initially focused on basic manipulation of lists and other mutable data. The next challenge was to consider higher-order programming, adding functions as first class objects to mutable data. Reasoning about actors added the challenge of dealing with distributed open systems of entities interacting asynchronously. The advent of cyber-physical agent…
▽ More
Theories for reasoning about programs with effects initially focused on basic manipulation of lists and other mutable data. The next challenge was to consider higher-order programming, adding functions as first class objects to mutable data. Reasoning about actors added the challenge of dealing with distributed open systems of entities interacting asynchronously. The advent of cyber-physical agents introduces the need to consider uncertainty, faults, physical as well as logical effects. In addition cyber-physical agents have sensors and actuators giving rise to a much richer class of effects with broader scope: think of self-driving cars, autonomous drones, or smart medical devices.
This paper gives a retrospective on reasoning about effects highlighting key principles and techniques and closing with challenges for future work.
△ Less
Submitted 29 April, 2019; v1 submitted 24 January, 2018;
originally announced January 2018.
-
Symbolic Timed Observational Equivalence
Authors:
Vivek Nigam,
Carolyn Talcott,
Abrãao Aires Urquiza
Abstract:
Intruders can infer properties of a system by measuring the time it takes for the system to respond to some request of a given protocol, that is, by exploiting time side channels. These properties may help intruders distinguish whether a system is a honeypot or concrete system hel** him avoid defense mechanisms, or track a user among others violating his privacy. Observational equivalence is the…
▽ More
Intruders can infer properties of a system by measuring the time it takes for the system to respond to some request of a given protocol, that is, by exploiting time side channels. These properties may help intruders distinguish whether a system is a honeypot or concrete system hel** him avoid defense mechanisms, or track a user among others violating his privacy. Observational equivalence is the technical machinery used for verifying whether two systems are distinguishable. Moreover, efficient symbolic methods have been developed for automating the check of observational equivalence of systems. This paper introduces a novel definition of timed observational equivalence which also distinguishes systems according to their time side channels. Moreover, as our definition uses symbolic time constraints, it can be automated by using SMT-solvers.
△ Less
Submitted 17 December, 2018; v1 submitted 12 January, 2018;
originally announced January 2018.
-
A Component-oriented Framework for Autonomous Agents
Authors:
Tobias Kappé,
Farhad Arbab,
Carolyn Talcott
Abstract:
The design of a complex system warrants a compositional methodology, i.e., composing simple components to obtain a larger system that exhibits their collective behavior in a meaningful way. We propose an automaton-based paradigm for compositional design of such systems where an action is accompanied by one or more preferences. At run-time, these preferences provide a natural fallback mechanism for…
▽ More
The design of a complex system warrants a compositional methodology, i.e., composing simple components to obtain a larger system that exhibits their collective behavior in a meaningful way. We propose an automaton-based paradigm for compositional design of such systems where an action is accompanied by one or more preferences. At run-time, these preferences provide a natural fallback mechanism for the component, while at design-time they can be used to reason about the behavior of the component in an uncertain physical world. Using structures that tell us how to compose preferences and actions, we can compose formal representations of individual components or agents to obtain a representation of the composed system. We extend Linear Temporal Logic with two unary connectives that reflect the compositional structure of the actions, and show how it can be used to diagnose undesired behavior by tracing the falsification of a specification back to one or more culpable components.
△ Less
Submitted 31 July, 2017;
originally announced August 2017.
-
Time, Computational Complexity, and Probability in the Analysis of Distance-Bounding Protocols
Authors:
Max Kanovich,
Tajana Ban Kirigin,
Vivek Nigam,
Andre Scedrov,
Carolyn Talcott
Abstract:
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…
▽ More
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.
△ Less
Submitted 4 October, 2017; v1 submitted 12 February, 2017;
originally announced February 2017.
-
A Compositional Framework for Preference-Aware Agents
Authors:
Tobias Kappé,
Farhad Arbab,
Carolyn Talcott
Abstract:
A formal description of a Cyber-Physical system should include a rigorous specification of the computational and physical components involved, as well as their interaction. Such a description, thus, lends itself to a compositional model where every module in the model specifies the behavior of a (computational or physical) component or the interaction between different components. We propose a fra…
▽ More
A formal description of a Cyber-Physical system should include a rigorous specification of the computational and physical components involved, as well as their interaction. Such a description, thus, lends itself to a compositional model where every module in the model specifies the behavior of a (computational or physical) component or the interaction between different components. We propose a framework based on Soft Constraint Automata that facilitates the component-wise description of such systems and includes the tools necessary to compose subsystems in a meaningful way, to yield a description of the entire system. Most importantly, Soft Constraint Automata allow the description and composition of components' preferences as well as environmental constraints in a uniform fashion. We illustrate the utility of our framework using a detailed description of a patrolling robot, while highlighting methods of composition as well as possible techniques to employ them.
△ Less
Submitted 15 December, 2016;
originally announced December 2016.
-
Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems
Authors:
Max Kanovich,
Tajana Ban Kirigin,
Vivek Nigam,
Andre Scedrov,
Carolyn Talcott
Abstract:
Time-Sensitive Distributed Systems (TSDS), such as applications using autonomous drones, achieve goals under possible environment interference (\eg, winds). Moreover, goals are often specified using explicit time constraints which must be satisfied by the system \emph{perpetually}. For example, drones carrying out the surveillance of some area must always have \emph{recent pictures}, \ie, at most…
▽ More
Time-Sensitive Distributed Systems (TSDS), such as applications using autonomous drones, achieve goals under possible environment interference (\eg, winds). Moreover, goals are often specified using explicit time constraints which must be satisfied by the system \emph{perpetually}. For example, drones carrying out the surveillance of some area must always have \emph{recent pictures}, \ie, at most $M$ time units old, of some strategic locations. This paper proposes a Multiset Rewriting language with explicit time for specifying and analysing TSDSes. We introduce two properties, \emph{realizability} (some trace is good) and \emph{survivability} (where, in addition, all admissible traces are good). A good trace is an infinite trace in which goals are perpetually satisfied. We propose a class of systems called \emph{progressive timed systems} (PTS), where intuitively only a finite number of actions can be carried out in a bounded time period. We prove that for this class of systems both the realizability and the survivability problems are PSPACE-complete. Furthermore, if we impose a bound on time (as in bounded model-checking), we show that for PTS, realizability becomes NP-complete, while survivability is in the $Δ_2^p$ class of the polynomial hierarchy. Finally, we demonstrate that the rewriting logic system Maude can be used to automate time bounded verification of PTS.
△ Less
Submitted 2 July, 2024; v1 submitted 25 June, 2016;
originally announced June 2016.
-
Towards the Automated Verification of Cyber-Physical Security Protocols: Bounding the Number of Timed Intruders
Authors:
Vivek Nigam,
Carolyn Talcott,
Abraão Aires Urquiza
Abstract:
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 grea…
▽ More
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.
△ Less
Submitted 27 May, 2016;
originally announced May 2016.
-
The Immune System: the ultimate fractionated cyber-physical system
Authors:
Carolyn Talcott
Abstract:
In this little vision paper we analyze the human immune system from a computer science point of view with the aim of understanding the architecture and features that allow robust, effective behavior to emerge from local sensing and actions. We then recall the notion of fractionated cyber-physical systems, and compare and contrast this to the immune system. We conclude with some challenges.
In this little vision paper we analyze the human immune system from a computer science point of view with the aim of understanding the architecture and features that allow robust, effective behavior to emerge from local sensing and actions. We then recall the notion of fractionated cyber-physical systems, and compare and contrast this to the immune system. We conclude with some challenges.
△ Less
Submitted 19 September, 2013;
originally announced September 2013.
