Secure-by-Construction Synthesis for Control Systems

TL;DR

This work tackles safety and security in cyber-physical systems by formulating a secure-by-construction controller synthesis that enforces both safety and opacity. It introduces augmented control barrier functions (CBF/ACBF) on an augmented product system $\Sigma\times\Sigma$ and develops an iterative sum-of-squares (SOS) programming scheme to compute these barrier functions for polynomial dynamics. The approach accommodates user-defined costs, enabling the derivation of a single, optimal input at each step via a quadratic program, and it provides constructive conditions (Cond.1–6) guaranteeing invariance and opacity. Two case studies—a running car example and a chaser satellite—demonstrate practical efficacy, showing how the method preserves safety while concealing secret states from an intruder without relying on finite abstractions. Overall, this framework enables secure-by-construction synthesis for continuous-state CPS and highlights a pathway toward integrating broader security notions and temporal logic specifications into barrier-function-based control design.

Abstract

In this paper, we present the synthesis of secure-by-construction controllers that address safety and security properties simultaneously in cyber-physical systems. Our focus is on studying a specific security property called opacity, which characterizes the system's ability to maintain plausible deniability of its secret behavior in the presence of an intruder. These controllers are synthesized based on a concept of so-called (augmented) control barrier functions, which we introduce and discuss in detail. We propose conditions that facilitate the construction of the desired (augmented) control barrier functions and their corresponding secure-by-construction controllers. To compute these functions, we propose an iterative scheme that leverages iterative sum-of-square programming techniques. This approach enables efficient computation of these functions, particularly for polynomial systems. Moreover, we demonstrate the flexibility of our approach by incorporating user-defined cost functions into the construction of secure-by-construction controllers. Finally, we validate the effectiveness of our results through two case studies, illustrating the practical applicability and benefits of our proposed approach.

Figures (12)

• Figure 1: A malicious intruder observes the car's position to identify whether or not the car is executing a confidential task.
• Figure 2: Secure-by-construction controllers (yellow region) with a user-defined cost function, where $OP$ is an optimization problem appearing in Corollary \ref{['controller']}.
• Figure 3: A state run $\mathbf{x}_{x(0),\nu}$ of the car initiated from a secret location, and its ($\delta$-close output) equivalent trajectory $\mathbf{x}_{\hat{x}(0),\hat{\nu}}$ started from a non-secret region, i.e., $x(0)\in X_0\cap X^{\text{init}}_s$ and $\hat{x}(0)\in X_0\backslash X^{\text{init}}_s$. The shaded area in light blue is a $\delta$-band around $\mathbf{x}_{x(0),\nu}$. Additionally, $5.57$ and $-6.5$ are the boundaries of the secret state set $X^{\text{inf}}_s$ and the unsafe set $X_d$, respectively.
• Figure 4: Evolution of $x_2(k)$, input sequences $\nu(k)$ and $\hat{\nu}(k)$.
• Figure 5: A chaser satellite being observed by an intruder.

Theorems & Definitions (21)

• Definition 2.1
• Definition 2.2
• Definition 2.3
• Definition 2.4
• Definition 2.5
• Definition 2.6
• Example 1
• Definition 3.1
• Theorem 3.2
• Corollary 1