Secure-by-Construction Synthesis for Control Systems
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.
Code (0)
등록된 구현이 없습니다.
Methods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Encrypted Price-based Market Mechanism for Optimal Load Frequency Control
The global trend of energy deregulation has led to the market mechanism replacing some functionality of load frequency control (LFC). Accordingly, information exchange among participating generators and the market operat…
Reset Controller Synthesis by Reach-avoid Analysis for Delay Hybrid Systems
A reset controller plays a crucial role in designing hybrid systems. It restricts the initial set and redefines the reset map associated with discrete transitions, in order to guarantee the system to achieve its objectiv…
Discrete-Event Controller Synthesis for Autonomous Systems with Deep-Learning Perception Components
We present DeepDECS, a new method for the synthesis of correct-by-construction discrete-event controllers for autonomous systems that use deep neural network (DNN) classifiers for the perception step of their decision-ma…
Autonomous DrivingDecision MakingClawed and Dangerous: Can We Trust Open Agentic Systems?
Open agentic systems combine LLM-based planning with external capabilities, persistent memory, and privileged execution. They are used in coding assistants, browser copilots, and enterprise automation. OpenClaw is a visi…
Synthesis of Lyapunov Functions using Formal Verification
Recent employments of SMT solvers within the Lyapunov function synthesis provided effective tools for automated construction of Lyapunov functions alongside with sound computer-assisted certificates. The main benefit of …