Source-linked AI summary
Secure State Estimation For Cyber Physical Systems Under Sensor Attacks: A Satisfiability Modulo Theory Approach
Yasser Shoukry, Pierluigi Nuzzo, Alberto Puggelli, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Paulo Tabuada
TL;DR
The paper addresses secure state estimation for linear dynamical systems when an attacker can corrupt sensor measurements. It develops IMHOTEP-SMT, an SMT-based detector that isolates attacked sensors and estimates the state, with formal soundness and completeness guarantees, runtime evaluation, and an unmanned ground vehicle demonstration.
Problem
Secure state estimation must handle arbitrary corruption of an unknown subset of sensors in multi-dimensional systems, making the problem combinatorial.
Method
The paper formulates estimation as Boolean and convex constraints and solves them with the IMHOTEP-SMT lazy SMT procedure.
Results
IMHOTEP-SMT is formally shown sound and complete under the stated conditions, and is evaluated through simulations and unmanned ground vehicle control.
Takeaways & Limitations
The approach provides attacked-sensor identification and state estimation while addressing the combinatorial structure of secure estimation.
Abstract
from arXiv · showhide
We address the problem of detecting and mitigating the effect of malicious attacks to the sensors of a linear dynamical system. We develop a novel, efficient algorithm that uses a Satisfiability-Modulo-Theory approach to isolate the compromised sensors and estimate the system state despite the presence of the attack, thus harnessing the intrinsic combinatorial complexity of the problem. By leveraging results from formal methods over real numbers, we provide guarantees on the soundness and completeness of our algorithm. We then report simulation results to compare its runtime performance with alternative techniques. Finally, we demonstrate its application to the problem of controlling an unmanned ground vehicle.
I. INTRODUCTION
The paper frames secure state estimation under arbitrary sensor attacks as a combinatorial problem and develops an SMT-based approach combining Boolean and convex constraints. Its contributions include formal correctness guarantees, runtime heuristics, and validation through simulations and an unmanned ground vehicle application.
- Motivation: Secure state estimation is challenging because multi-dimensional systems with multiple sensors face attacks whose time evolution is not assumed known.The problem becomes combinatorial when the system is multi-dimensional and the attacker may corrupt an unknown subset of sensors without restrictions on attack evolution.
- Related work: Prior brute-force methods can require a combinatorial number of monitors or outputs when only an upper bound on attacked sensors is known.These approaches search across possible attacked-sensor configurations, which may hinder scalability.
- Related work: Convex relaxation methods solve a polynomial-time approximation but can lose correctness guarantees, while alternative polynomial-time methods require restrictive system conditions.The paper reports experiments in which relaxed l_r/l_1 formulations produce incorrect results.
- Contributions: The paper formalizes secure state estimation as satisfiability over Boolean and convex real-valued constraints.Boolean variables represent whether sensors are attacked, while convex constraints encode properties of the system state.
- Contributions: IMHOTEP-SMT is presented as a sound and complete solver that returns attacked-sensor indices and the system-state estimate.The method uses formal methods and an SMT paradigm adapted to convex constraint solving.
- Contributions: The paper proposes geometry-aware heuristics and iteration upper bounds to improve execution time and provide real-time guarantees.The approach is evaluated through numerical comparisons and demonstrated in unmanned ground vehicle control.
D. Problem Statement
The paper formulates secure state estimation as finding the system state and sensor-attack indicators satisfying Boolean, cardinality, and convex measurement constraints. Minimal attack support provides a unique solution under 2s-sparse observability, while MIQP reformulation may lose completeness because of its big-M constant.
- Each sensor receives a binary indicator b_i, with b_i = 0 for attack-free and b_i = 1 for attacked sensors.
- Secure state estimation seeks an estimate (x, b) satisfying sensor residual bounds and a maximum of s attacked sensors.For attack-free sensors, the residual is constrained by the sensor’s noise bound; the cardinality constraint limits the number of attacked sensors.
- The minimal-support formulation selects the smallest attack set that explains the collected measurements, and binary search over the support size can recover this solution.
- In the noiseless case, Problem II.2 has a unique solution if and only if the system is 2s-sparse observable.
- Correct reconstruction is impossible when at least ⌈p/2⌉ sensors are attacked, because multiple states can then produce identical measurements.
- The MIQP reformulation depends on a sufficiently large big-M constant, so completeness cannot generally be guaranteed when attack magnitudes are not known a priori.
III. SMT-BASED DETECTOR
IMHOTEP-SMT combines SAT reasoning over attack assignments with convex theory checking over the state estimate. UNSAT certificates refine Boolean assignments, and under 2s-sparse observability the procedure has formal soundness and completeness properties, with tolerance-dependent limitations under noise.
- SMT architecture: IMHOTEP-SMT uses a SAT solver for Boolean and pseudo-Boolean constraints and a theory solver for convex constraints over real-valued states.
- SMT architecture: SAT-SOLVE proposes sensor assignments, while T-SOLVE.CHECK tests whether one state satisfies the convex constraints for the hypothesized attack-free sensors.
- SMT architecture: If the theory check is UNSAT, the solver generates Boolean constraints describing conflicting sensor measurements and repeats the SAT query.
- Soundness and completeness: With zero noise and zero solver tolerance, Algorithm 2 returns SAT exactly when the selected sensors are attack-free and its computed state equals the true state.
- Soundness and completeness: The proof uses 2s-sparse observability to show that at least p−2s selected sensors have an observability matrix with trivial kernel, forcing the estimated state to be unique.
- Noise and tolerance: With noise or nonzero numerical tolerance, checking only whether the objective falls below the threshold is insufficient for exact state recovery and may miss low-power attacks.
C. Generating UNSAT certificates
The certificate-generation procedure seeks small conflicting sensor sets rather than merely excluding one Boolean assignment. A residual-based heuristic starts with the lowest-residual hyperplanes and adds higher-residual sensors until a conflict appears.
- Trivial certificates: A trivial UNSAT certificate identifies that at least one sensor assumed attack-free is actually attacked, then forces a Boolean change in the next SAT assignment.
- Trivial certificates: The trivial certificate excludes only the current assignment and can therefore lead to exponential execution time.
- Geometric intuition: The geometric intuition represents attack-free measurements as hyperplanes sharing a unique intersection, while the attacked sensor’s hyperplane conflicts with that solution.
- Algorithm 3: Algorithm 3 begins with the p−2s sensors having the smallest normalized residuals, then adds sensors with larger residuals until their hyperplanes fail to intersect.
- Guarantees: Under the stated noiseless and zero-tolerance assumptions, the trivial-certificate algorithm is δ-complete with δ = 0, but its iteration bound is combinatorial.
D. Enhancing the Execution Time
The paper accelerates SMT-based secure state estimation by generating compact UNSAT certificates from geometric conflicts and sensor residuals. These certificates preserve formal guarantees while reducing the information the SAT solver must search through.
- Certificate design: Smaller UNSAT certificates accelerate SAT-solver convergence by encoding more information about conflicting sensor assignments.A certificate identifying one attacked sensor at each step improves substantially over the exponential worst-case complexity of the plain SAT problem.
- Geometric formulation: Proposition III.3 equates an UNSAT satisfiability check with an empty intersection of the corresponding sensor hyperplanes.Each sensor measurement defines a hyperplane, and the optimization problem minimizes residuals relative to these hyperplanes.
- Conflicting certificates: Any UNSAT sensor set larger than p−2s contains a conflicting subset of at most p−2s+1 sensors.This bound motivates searching for small conflict explanations rather than enumerating all sensors in a failed assignment.
- Conflicting certificates: The conflicting-certificate heuristic sorts normalized residuals, starts with the p−2s smallest, and tests higher-residual hyperplanes until a conflict appears.It then removes hyperplanes with the highest dimensions to further reduce the conflicting set.
- Guarantees: The conflicting-certificate algorithm remains δ-complete with δ = 0, while its worst-case iterations are bounded by exhaustive generation of conflicts of size p−2s+1.The bound follows because every generated conflicting certificate has at most p−2s+1 sensors.
- Agreeable certificates: The agreeable heuristic selects p−2s sensors with minimum residuals and checks whether their hyperplanes intersect at one point before certifying them as unattacked.This heuristic complements the conflicting certificate and is not always generated.
2) Agreeable Sensor Set:
The agreeable certificate exploits a set of low-residual sensors that agree on one state estimate, but its use requires stronger observability and is not universally applicable.
- Agreeable sensor set: The agreeable certificate marks the p−2s lowest-residual sensors as unattacked when their hyperplanes agree on a common state.The heuristic informs the SAT solver that these sensors are attack-free only when the satisfiability check succeeds.
- Agreeable sensor set: The agreeable heuristic is complementary because it is not always generated and attacks can make up to s compromised sensors agree on one state value.Its applicability therefore depends on an additional system condition.
- Guarantee: Under 3s-sparse observability, the agreeable certificate preserves δ-completeness with δ = 0 whenever it is generated.The certificate fixes p−2s sensors as unattacked, leaving 2s sensors for the solver to search.
E. Soundness and Completeness of Algorithm 1, Noiseless Case
The paper establishes exact correctness in the noiseless case and characterizes how noise and solver tolerance affect detection and estimation. The resulting guarantees depend on sparse observability, noise margins, and attack magnitude.
- Noiseless case: Theorem III.7 states that Algorithm 1 is δ-complete with δ = 0 under 2s-sparse observability, zero measurement noise, and zero solver tolerance.The implementation combines the certificate procedure with the agreeable heuristic when p > 3s.
- Technical quantities: The soundness and completeness analysis relies on properties of the Moore-Penrose pseudoinverse of the selected observation matrix.The paper defines auxiliary quantities based on this pseudoinverse and ∆s to state the noisy guarantees.
- Noisy case: In noisy settings, completeness depends on both numerical solver tolerance and the dynamical system’s intrinsic noise margin.The paper modifies the satisfiability condition to account for both quantities.
- Detection guarantee: For attacks satisfying the stated magnitude condition, the modified algorithm is δ-complete with δ = o∥Ψ∥2.The guarantee assumes 2s-sparse observability and positive solver tolerance.
- Detection guarantee: Only attacks below the stated detection threshold can remain undetected and affect the estimation error.The threshold depends on solver tolerance and the sparse-observability quantity ∆s.
- Estimation error: The resulting estimate satisfies the theorem’s error bound involving the noise norm, solver tolerance, and the factor 1−∆s.The bound characterizes estimation error under undetectable attacks rather than claiming exact recovery in that regime.
V. EXPERIMENTAL RESULTS
The experiments implement the theory solver in MATLAB with SAT4J and evaluate heuristic iteration counts, runtime against prior algorithms, and robotic-vehicle control.
- Experimental setup: The implementation uses MATLAB interfaced with the pseudo-Boolean SAT solver SAT4J on an Intel Core i7 3.4-GHz processor with 8 GB of memory.The evaluation compares the two heuristics, benchmarks runtime against prior algorithms, and demonstrates attack detection in robotic-vehicle control.
A. Runtime Performance
The experiments evaluate IMHOTEP-SMT’s heuristic efficiency and compare its runtime and estimation error with alternative secure state-estimation methods.
- Heuristic efficiency: Using the conflicting certificate reduced IMHOTEP-SMT iterations by an average factor of 50× versus the trivial certificate.Combining conflicting and agreement certificates increased the reduction factor to 75.
- Heuristic efficiency: The joint conflicting-and-agreement certificate decreased iterations by a factor of 75 compared with the trivial certificate.
- Comparative evaluation: IMHOTEP-SMT was compared with MIQP, ETPG, and the ℓr/ℓ1 decoder on execution time and estimation error.The implementations used GUROBI, MATLAB, and CVX, respectively.
- Comparative evaluation: IMHOTEP-SMT outperformed ETPG and the ℓr/ℓ1 approach and scaled with both the number of states and sensors in the reported tests.Increasing states had a small effect on its execution time, while increasing sensors increased constraints and execution time.
B. Attacking an Unmanned Ground Vehicle
The proposed SMT-based detector is applied to a UGV model with GPS and encoder sensors, where its state estimates support feedback control under several encoder attacks.
- Simulation context: Figure 2 reports iterations, execution time, and estimation error as the numbers of states and sensors vary.
- UGV model: The UGV model uses position and linear velocity as states, force as input, GPS for position, and two motor encoders for velocity.The model assumes straight-line motion and complete stops before rotation.
- Control application: The discretized SMT detector estimates the UGV state from the model and measurements for feedback control along a 5 m square path.The discretization time step is 0.1 s.
- Attack evaluation: The detector handles random-noise, step-and-ramp, and replay attacks while estimating the UGV state and attacked-sensor support.The attacker alternates between corrupting the left and right encoder measurements.
VI. CONCLUSIONS
The paper concludes that its sound and complete SMT algorithm addresses secure state estimation for linear systems under sensor attacks and is validated in simulations and UGV control.
- The proposed algorithm uses Satisfiability-Modulo-Theories to handle the combinatorial complexity of secure state estimation for linear dynamical systems under sensor attacks.Its detector exploits geometric structure to reason about inconsistent sensor measurements and improve runtime.
- The approach was validated through numerical simulations and demonstrated on an unmanned ground vehicle control problem.Future work includes extending and characterizing the algorithm for nonlinear and hybrid dynamical systems.
APPENDIX
The appendix develops matrix definiteness and eigenvalue facts used in its proof arguments.
- Products AB and BA have the same eigenvalues for square matrices A and B.
- If I − A is positive definite, every eigenvalue of A is strictly less than 1.
- For positive semidefinite A and positive definite B, the appendix states a matrix result involving (A + B)^−1.The proof uses positive definiteness, square-root transformations, and eigenvalue preservation.
- The transformed matrix 2(A + B)^−1/2 A(A + B)^−1/2 has eigenvalues strictly less than 1, implying the same for A(A + B)^−1.