Bounded Synthesis of Resilient Supervisors

TL;DR

This paper presents a constraint-based method for synthesizing resilient supervisors in cyber-physical systems, capable of defending against combined actuator and sensor attacks by reducing the problem to QBF and SAT solving techniques.

Contribution

It introduces a novel bounded synthesis approach for resilient supervisors using QBF reduction and counterexample-guided inductive synthesis, addressing complex attack scenarios.

Findings

Effective synthesis of resilient supervisors against combined attacks

Reduction of the synthesis problem to QBF and SAT formulations

Use of counterexamples to guide the synthesis process

Abstract

In this paper, we investigate the problem of synthesizing resilient supervisors against combined actuator and sensor attacks, for the subclass of cyber-physical systems that can be modelled as discrete-event systems. We assume that the attackers can carry out actuator enablement and disablement attacks as well as sensor replacement attacks. We consider both risky attackers and covert attackers in the setup where the (partial-observation) attackers may or may not eavesdrop the control commands (issued by the supervisor). A constraint-based approach for the bounded synthesis of resilient supervisors is developed, by reducing the problem to the Quantified Boolean Formulas (QBF) problem. The bounded synthesis problem can then be solved either with a QBF solver or with repeated calls to a propositional satisfiability (SAT) solver, by employing maximally permissive attackers, which can be synthesized with the existing partial-observation supervisor synthesis procedures, as counter examples in the counter example guided inductive synthesis loop.