This paper studies the synthesis of controllers for cyber-physical systems (CPSs) that are required to carry out complex time-sensitive tasks in the presence of an adversary. The time-sensitive task is specified as a formula in the metric interval temporal logic (MITL). CPSs that operate in adversarial environments have typically been abstracted as stochastic games (SGs); however, because traditional SG models do not incorporate a notion of time, they cannot be used in a setting where the objective is time-sensitive. To address this, we introduce durational stochastic games (DSGs). DSGs generalize SGs to incorporate a notion of time and model the adversary’s abilities to tamper with the control input (actuator attack) and manipulate the timing information that is perceived by the CPS (timing attack). We define notions of spatial, temporal, and spatio-temporal robustness to quantify the amounts by which system trajectories under the synthesized policy can be perturbed in space and time without affecting satisfaction of the MITL objective. In the case of an actuator attack, we design computational procedures to synthesize controllers that will satisfy the MITL task along with a guarantee of its robustness. In the presence of a timing attack, we relax the robustness constraint to develop a value iteration-based procedure to compute the CPS policy as a finite-state controller to maximize the probability of satisfying the MITL task. A numerical evaluation of our approach is presented on a signalized traffic network to illustrate our results.
Minimum Violation Control Synthesis on Cyber-Physical Systems under Attacks
Cyber-physical systems are conducting increasingly complex tasks, which are often modeled using formal
languages such as temporal logic. The system’s ability to
perform the required tasks can be curtailed by malicious
adversaries that mount intelligent attacks. At present, however,
synthesis in the presence of such attacks has received limited
research attention. In particular, the problem of synthesizing a
controller when the required specifications cannot be satisfied
completely due to adversarial attacks has not been studied.
In this paper, we focus on the minimum violation control
synthesis problem under linear temporal logic constraints of
a stochastic finite state discrete-time system with the presence
of an adversary. A minimum violation control strategy is one
that satisfies the most important tasks defined by the user while
violating the less important ones. We model the interaction
between the controller and adversary using a concurrent Stackelberg game and present a nonlinear programming problem to
formulate and solve for the optimal control policy. To reduce
the computation effort, we develop a heuristic algorithm that
solves the problem efficiently and demonstrate our proposed
approach using a numerical case study.
more »
« less
- Award ID(s):
- 1656981
- NSF-PAR ID:
- 10131732
- Date Published:
- Journal Name:
- IEEE Conference on Decision and Control (CDC)
- Page Range / eLocation ID:
- 262-269
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
more » « less
-
Prior work on automatic control synthesis for cyberphysical systems under logical constraints has primarily focused on environmental disturbances or modeling uncertainties, however, the impact of deliberate and malicious attacks has been less studied. In this paper, we consider a discrete-time dynamical system with a linear temporal logic (LTL) constraint in the presence of an adversary, which is modeled as a stochastic game. We assume that the adversary observes the control policy before choosing an attack strategy. We investigate two problems. In the first problem, we synthesize a robust control policy for the stochastic game that maximizes the probability of satisfying the LTL constraint. A value iteration based algorithm is proposed to compute the optimal control policy. In the second problem, we focus on a subclass of LTL constraints, which consist of an arbitrary LTL formula and an invariant constraint. We then investigate the problem of computing a control policy that minimizes the expected number of invariant constraint violations while maximizing the probability of satisfying the arbitrary LTL constraint. We characterize the optimality condition for the desired control policy. A policy iteration based algorithm is proposed to compute the control policy. We illustrate the proposed approaches using two numerical case studies.more » « less
-
The Unmanned aerial vehicles (UAVs) sector is fast-expanding. Protection of real-time UAV applications against malicious attacks has become an urgent problem that needs to be solved. Denial-of-service (DoS) attack aims to exhaust system resources and cause important tasks to miss deadlines. DoS attack may be one of the common problems of UAV systems, due to its simple implementation. In this paper, we present a software framework that offers DoS attack-resilient control for real-time UAV systems using containers: Container Drone. The framework provides defense mechanisms for three critical system resources: CPU, memory, and communication channel. We restrict the attacker's access to the CPU core set and utilization. Memory bandwidth throttling limits the attacker's memory usage. By simulating sensors and drivers in the container, a security monitor constantly checks DoS attacks over communication channels. Upon the detection of a security rule violation, the framework switches to the safety controller to mitigate the attack. We implemented a prototype quadcopter with commercially off-the-shelf (COTS) hardware and open-source software. Our experimental results demonstrated the effectiveness of the proposed framework defending against various DoS attacks.more » « less
-
This paper studies the synthesis of control policies for an agent that has to satisfy a temporal logic specification in a partially observable environment, in the presence of an adversary. The interaction of the agent (defender) with the adversary is modeled as a partially observable stochastic game. The search for policies is limited to over the space of finite state controllers, which leads to a tractable approach to determine policies. The goal is to generate a defender policy to maximize satisfaction of a given temporal logic specification under any adversary policy. We relate the satisfaction of the specification in terms of reaching (a subset of) recurrent states of a Markov chain. We then present a procedure to determine a set of defender and adversary finite state controllers of given sizes that will satisfy the temporal logic specification. We illustrate our approach with an example.more » « less
-
This paper studies the satisfaction of a class of temporal properties for cyber-physical systems (CPSs) over a finite-time horizon in the presence of an adversary, in an environment described by discretetime dynamics. The temporal logic specification is given in safe−LTLF , a fragment of linear temporal logic over traces of finite length. The interaction of the CPS with the adversary is modeled as a two-player zerosum discrete-time dynamic stochastic game with the CPS as defender. We formulate a dynamic programming based approach to determine a stationary defender policy that maximizes the probability of satisfaction of a safe − LTLF formula over a finite time-horizon under any stationary adversary policy. We introduce secure control barrier certificates (S-CBCs), a generalization of barrier certificates and control barrier certificates that accounts for the presence of an adversary, and use S-CBCs to provide a lower bound on the above satisfaction probability. When the dynamics of the evolution of the system state has a specific underlying structure, we present a way to determine an S-CBC as a polynomial in the state variables using sum-of-squares optimization. An illustrative example demonstrates our approach.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- The DOI is not currently available.
