{"id":"fb36ae8a-020c-4190-8fd1-09c48d56fed3","arxiv_id":"2505.06842","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"Secure safety filters for sampled-data nonlinear systems under sensor spoofing are constructed from exact and relaxed observability maps, with safety guaranteed under sparse-observability and control barrier function assumptions.","lead":"A new secure safety filter uses observability maps to keep sampled-data nonlinear systems safe when up to s sensors are spoofed. It gives safety guarantees under sparse-observability conditions and demonstrates them on a unicycle with compromised sensors.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 2's induction assumes the CBF value at the estimator state h(hat x^Gamma_k) stays positive, but this is not established and can fail without a margin condition; the relaxed-case safety proof is incomplete.","rationale":"I read the paper in good faith. The exact-observability path (Section III) is a coherent extension of the authors' prior linear results: Theorem 1's guarantees follow from Proposition 1 and Corollary 1, and no gap surfaced there. The central contribution, however, is the relaxed-observability path, which is the one validated in simulation. The reader identified Lemma 2 as the weakest assumption. I agree that Lemma 2 is under-supported: the proof is omitted, and Definition 8 is ambiguous about whether the consistency witness z must lie in L_D^Gamma. But a closer reading shows Theorem 2 does not actually use Lemma 2; it uses Proposition 3 and the filter constraint (26). The most load-bearing flaw is in Theorem 2's own proof: the assertion that h(hat x^Gamma_k) remains positive by 'recursive reasoning' is not supported, because hat x^Gamma_k is an estimator output, not a propagated state, and no margin condition such as epsilon > L_1 delta' is assumed. This is a correctness risk in the core relaxed-case guarantee. The paper's numerical example is suggestive but does not test the boundary case where the estimate's CBF value is near zero while the actual state is safe; such a case is exactly where the induction could break. For these reasons I recommend conditional acceptance, contingent on a corrected and complete proof of Theorem 2 (with any needed margin assumption stated explicitly) and, secondarily, a full proof of Lemma 2 plus clarification of Definition 8.","tokens_in":13965,"tokens_out":15860,"duration_ms":163194,"concrete_test":"Formalize the induction in Theorem 2 with an explicit invariant. Either prove from the stated assumptions that for the Gamma selected in Proposition 3, h(hat x^Gamma_k) >= 0 for every k, or exhibit a system satisfying all assumptions with epsilon < L_1 delta' and an initial state on the boundary of C with h(x) < L_1 delta'. Then run filter (26) on the paper's unicycle example with T = 0.01, l = 25, the same Gaussian derivative estimator, and a safety constraint whose boundary is approached so that h(hat x^Gamma_k) becomes negative while the QP remains feasible. If the closed-loop h drops below 0, the recursive step in Theorem 2 is invalid. If it does not, identify the hidden margin condition that makes the invariant true and add it to the theorem statement and proof.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The relaxed-observability safety theorem (Theorem 2) contains a load-bearing proof gap that is independent of Lemma 2. In the proof, after deriving h(phi(T;x,u)) >= (1-gamma)h(hat x^Gamma_k) + epsilon, the text states: 'By recursive reasoning, we know h(hat x^Gamma_k) remains positive if it starts positive.' This step is unjustified. hat x^Gamma_k is the output of the observability map at time k for some consistent sensor set Gamma, not a state propagated from the previous estimate. The filter constraint (26) is enforced at hat x^Gamma_k and guarantees h(F(hat x^Gamma_k,u)) >= (1-gamma)h(hat x^Gamma_k)+epsilon+epsilon_1, but the next estimate hat x^Gamma_{k+1} is recomputed from new data and need not equal F(hat x^Gamma_k,u). No assumption on the observability map ensures the CBF value at the next estimate inherits positivity. At best, Lipschitz continuity gives h(hat x_{k+1}) >= h(x_{k+1}) - L_1 delta', and the derivation only yields h(x_{k+1}) >= (1-gamma)h(hat x_k)+epsilon. If h(hat x_k) is small and gamma is not the identity, this can be below epsilon, or even below L_1 delta', so the next estimate can have negative CBF value and the induction collapses. The theorem as stated assumes only that the initial state lies in C, not that h(x) >= L_1 delta' or any equivalent margin. This gap affects exactly the relaxed case that is exercised in the simulation. Separately, Lemma 2's omitted proof and the ambiguous consistency condition in Definition 8 remain genuine concerns, but they bear mainly on Corollary 2 rather than on Theorem 2 itself.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a secure safety filter for sampled-data nonlinear systems under sensor spoofing attacks, building on zero-order control barrier functions. It introduces exact and relaxed \"observability maps\" that abstract state estimators, defines sparse variants of differential observability, and uses consistency checks to compute an over-approximation of the set of plausible states. A safety filter is then formulated as a quadratic program enforcing the CBF condition over all plausible states; Theorem 1 covers the exact observability case and Theorem 2 the relaxed δ-bounded case. The claims are validated in simulation on a unicycle with two spoofed sensors.","tokens_in":14404,"tokens_out":9121,"duration_ms":89234,"significance":"The conceptual contribution is valuable: it extends secure safety filters from linear and differentially flat systems to general sampled-data nonlinear systems, and it cleanly separates secure state reconstruction from safety filtering by abstracting estimators as set-valued maps. The paper also provides reproducible code and a concrete simulation. However, the relaxed-case safety theorem is not yet proved: it relies on an omitted proof of Lemma 2 and on an unjustified recursive-positivity argument in the proof of Theorem 2. These are load-bearing for the relaxed case, which is the case exercised in the simulation, so the paper needs major revision.","major_comments":[{"comment":"The sentence \"By recursive reasoning, we know h(hat x_k) remains positive if it starts positive\" is not justified. The quantity hat x_k is produced from current input-output data by the observability map, and it need not equal the state propagated from the previous estimate F(hat x_{k-1}, u_{k-1}); the filter constraint (26) is enforced at the current estimate and does not control the next estimate. The proof needs an explicit margin condition on the estimator states, e.g., a lower bound on h(hat x_k)-gamma(h(hat x_k))+epsilon relative to the Lipschitz terms L1 delta' and L1 bar-w, or a direct argument that h(hat x_{k+1}) >= (1-gamma)h(hat x_k)+epsilon. Without such a condition the induction collapses. This gap affects exactly the relaxed case used in the simulation.","section":"Section IV, proof of Theorem 2 (after Eq. (27))"},{"comment":"Lemma 2 is the key step for Corollary 2 and Theorem 2, yet its proof is omitted with the statement \"neglected due to space limitations.\" This is not acceptable for a load-bearing lemma. In addition, Definition 8 only requires ||z - hat x_{k-l}^Gamma|| <= delta and does not require z to lie in L_D^Gamma(...), which makes the intersection claim (20) ambiguous: a point outside L_D^Gamma2 but inside its enclosing ball need not satisfy the consistency equations for the smaller sensor set. Please provide a full proof and clarify the exact role of L_D^Gamma in the consistency condition.","section":"Section IV, Lemma 2 and Definition 8"},{"comment":"The proof of Theorem 2 uses, without stating them as assumptions, that F(x,u) is Lipschitz in x uniformly in u (with constant L), that h is Lipschitz (with constant L1), and that these constants are known so that epsilon1 can be chosen. The theorem statement as written only assumes Assumption 1, zero-order CBF, and s-sparse delta-bounded observability. Please add the Lipschitz/global-constant assumptions to the theorem statement, or make clear that they are inherited from Proposition 3 and the choice of epsilon1 after Eq. (26).","section":"Section IV, Theorem 2 statement"}],"minor_comments":[{"comment":"There is a duplicated article in \"available to the the controller\" and again in \"with the the Department\" in the author footnote.","section":"Introduction"},{"comment":"Theorem 1 refers to \"system (7)\" for the sparse observability condition, but the system equation is (5) and (7) is the plausible-state equation; Theorem 2 refers to \"system (17)\", which should be (14).","section":"Theorems 1 and 2"},{"comment":"The notation (1-gamma)h(x) is not defined; since gamma is a function, it should be written as h(x)-gamma(h(x)) to avoid ambiguity.","section":"Definitions 1 and 3; proofs"},{"comment":"The quantity hat x_{k-l}^Gamma is used but not defined in the definition; it presumably denotes the center of the ball from Definition 6. Please state this explicitly.","section":"Definition 8"},{"comment":"In the proof of (23), the index Gamma is chosen after fixing an element z_{k-l}; the statement should clarify that the union is over Gamma and that for each Gamma the propagated bound uses the same Gamma throughout the l steps.","section":"Proposition 3"},{"comment":"The claim that the sampled-data unicycle is 2-sparse delta-bounded observable is asserted without a formal verification; given that Theorem 2 is the main relaxed-case result, a few details on how delta, delta', and epsilon1 are chosen would improve reproducibility.","section":"Section V, Simulation"}],"recommendation":"major_revision","confidential_remarks":"The paper is from a well-known group and the exact-case portion is sound, but the relaxed case is the advertised generalization and it is currently unproved. With a full proof of Lemma 2 and a repaired induction in Theorem 2, the paper would be a solid contribution; in its present form I cannot recommend publication."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nYou should know about arXiv:2505.06842 because it is one of the first attempts to push secure safety filters beyond linear systems, and the core abstraction is worth your time. The exact-observability half (Section III) is clean. Defining observability maps and consistency conditions for nonlinear systems, then showing the plausible-state set is the union over attack-free sensor subsets, is a nice generalization of their prior linear result. Theorem 1 and Corollary 1 are correctly argued as far as I can tell.\n\nThe trouble is in the relaxed-observability half, which is the one they actually simulate. Theorem 2's proof uses a step I do not think holds: after deriving h(phi(T;x,u)) >= (1-gamma)h(hat x^Gamma_k) + epsilon, it says \"by recursive reasoning, h(hat x^Gamma_k) remains positive.\" But hat x^Gamma_k is recomputed at each step from the observability map, not propagated from the previous estimate. The filter constraint is enforced at the current estimate for the current time, but nothing guarantees the next estimate has a positive CBF value. You would need either an assumption that h(hat x_k) >= something like L_1 delta' or a robustness margin in the filter, and the paper does not supply it. This is a load-bearing gap for the relaxed case, and it is separate from the omitted Lemma 2.\n\nLemma 2's proof is explicitly skipped \"due to space limitations\" and is used for Corollary 2's 4 delta bound rather than for Theorem 2. That is less critical, but it should still be supplied. The consistency condition in Definition 8 also does not explicitly require the candidate z to lie in L_D^Gamma, which makes the intersection claim in Lemma 2 ambiguous. These are fixable.\n\nThe unicycle simulation is useful and they provide code, which is more than many papers in this area do. The attack model is honest: omniscient attacker, at most s sensors. I would like to see the tuned consistency threshold specified, though.\n\nMy take: the exact case deserves publication, and the relaxed case is promising but not ready as stated. The induction gap is a genuine flaw that a referee would likely catch. I would still send this to peer review—it is novel, the framework is sound in the exact case, and the relaxed case could be repaired with a margin argument. But it should not be accepted without that fix.\n\nFor you: worth a reading group discussion because the gap is instructive. I would cite the exact-observability part if I write about secure CBFs. Recommendation: serious referee, conditional acceptance.","headline":"Novel extension of secure safety filters to nonlinear systems, but the relaxed-case Theorem 2 has a genuine induction gap that needs fixing before publication.","tokens_in":14862,"tokens_out":2488,"would_cite":true,"duration_ms":25163,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["93C57","93C10","93B07"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that secure safety filters, previously limited to linear or differentially flat systems, can be extended to general sampled-data nonlinear systems under sensor spoofing attacks, provided the system satisfies a sparse…","keywords":["secure safety filter","sensor spoofing attacks","nonlinear sampled-data systems","control barrier functions","sparse observability","secure state estimation","zero-order control barrier function","observability maps"],"falsifier":"Run a search over a nonlinear system that is $\\delta$-bounded observable, with nested sensor sets $\\Gamma_1\\subset\\Gamma_2$, for input-output data that is consistent for $\\Gamma_2$ under (19) but for which $L_D^{\\Gamma_1}\\cap L_D^{\\Gamma_2}=\\varnothing$; a single such instance would refute the $B_{4\\delta}$ bound of Corollary 2 and the relaxed $2s$-sparse guarantee. For the exact claim, simulate a $2s$-sparse observable sampled-data nonlinear system with an omniscient $s$-sensor spoofing attack and check whether the QP (13), feasible at every step, ever lets $h(x(t))<0$; any violation would refute Theorem 1.","tokens_in":13756,"feed_emoji":"🛡️","tokens_out":11428,"duration_ms":108568,"temperature":0.7,"pith_summary":"This paper tries to extend the secure safety filter—a device that keeps a system inside a safe set even when an attacker corrupts up to $s$ sensors—from linear and differentially flat systems to general sampled-data nonlinear systems. It does so by replacing concrete state estimators with observability maps: for every subset of $p-s$ sensors, the map converts a window of input-output data into a candidate past state, and a consistency check determines which candidates are plausible. The safety filter then solves a control-barrier-function optimization that enforces the safety condition for every plausible state at once. In the exact case, safety follows whenever that optimization is feasible, and with $2s$-sparse observability the true state is uniquely identified so feasibility is automatic; a relaxed version tolerates bounded process disturbance at the price of a slightly larger uncertainty set. A unicycle simulation with two spoofed sensors demonstrates the mechanism.","feed_headline":"Safety filters now guard nonlinear systems against sensor spoofing","feed_subtitle":"The filter checks every plausible state and keeps the true one safely inside.","key_machinery":"The load-bearing objects are exact and relaxed observability maps. An exact map $L^{\\Gamma}(\\cdot)$ reconstructs the state $l$ sampling steps in the past from a window of inputs and the measurements of sensor subset $\\Gamma$; its relaxed counterpart $L_D^{\\Gamma}$ is set-valued and returns a set inside a $\\delta$-ball around an estimate, accommodating bounded process disturbance. These maps abstract whichever state estimator a user has available, so the subsequent arguments hold for any concrete estimator satisfying the observability definition. The other half is the zero-order control barrier function, a function $h$ whose sampled-data decrease condition guarantees $h$ stays nonnegative throughout the sampling interval. The secure filter couples the two: it collects the union of consistent estimates over all $p-s$ sensor subsets, propagates them to the present, and demands the CBF constraint hold for every plausible state simultaneously, giving the quadratic programs (13) and (26). The consistency condition, together with the proved Lemma 1 in the exact case and the unproved Lemma 2 in the relaxed case, is what lets nested sensor sets be compared so that redundancy can identify the true state or bound it.","core_discovery":"The central claim is that a safety filter can be made attack-robust for general sampled-data nonlinear systems by basing it on observability maps rather than on any one estimator. For each subset $\\Gamma$ of $p-s$ sensors, an observability map $L^{\\Gamma}$ reconstructs the state $l$ steps in the past from input-output data, and a consistency condition labels those reconstructions that agree with the dynamics and with uncorrupted sensors. When the system is $s$-sparse observable, the set of all plausible states is exactly the union of consistent reconstructions (Proposition 1), so a zero-order CBF filter that keeps every plausible state inside $\\mathcal{C}$ keeps the true state inside $\\mathcal{C}$; when $2s$-sparse observability holds, the true state is the only consistent reconstruction (Corollary 1), making the filter feasible automatically. The relaxed case replaces points by set-valued maps $L_D^{\\Gamma}$ enclosed in $\\delta$-balls, over-approximates plausible states by a $B_{4\\delta}$ ball under $2s$-sparse $\\delta$-bounded observability (Corollary 2), and uses a robust CBF filter (26) to preserve safety despite bounded process disturbance. The paper therefore asserts provable safety guarantees for nonlinear sampled-data systems under arbitrary spoofing of at most $s$ sensors, contingent on an offline-checkable observability property and, in the weaker $s$-sparse cases, online feasibility.","pith_inferences":["Inference: if a proof of Lemma 2 is supplied, the $B_{4\\delta}$ bound can be used as a deterministic, computationally checkable safety certificate for approximate nonlinear models under spoofing.","Inference: the observability-map abstraction makes the filter modular—improving the underlying estimator directly tightens $\\delta$, and hence shrinks the safety margin, without redesigning the filter.","Inference: the $2s$ redundancy threshold mirrors error-correction bounds, which suggests that compressed-sensing or coding-theoretic attack models could be imported to reduce conservatism below the worst-case subset union.","Inference: a testable extension is to make the data window length $l$ adaptive, since longer windows improve observability depth but delay detection of attacks that begin mid-window; the trade-off is not analyzed in the paper."],"forward_implications":["Under $2s$-sparse observability, the exact secure filter (13) needs no online feasibility check: the true state is the unique consistent estimate, so the CBF constraint is always satisfiable.","With only $s$-sparse observability, the same filter is safe whenever its QP stays feasible, and the paper argues feasibility cannot be checked a priori because arbitrary $s$ sensors may be compromised.","For sampled-data implementations using approximate discrete-time models, the relaxed filter (26) preserves safety with an inflated margin; using fourth-order Runge-Kutta makes the margin shrink like $T^5$ as the sampling period goes to zero.","In the unicycle example, the filter leaves the nominal controller untouched away from the boundary and only corrects near the safety band, so the price of security is localized in time."],"supporting_citations":[{"why":"The linear-system secure safety filter that this paper generalizes; its feasibility and redundancy arguments are the template for Theorems 1 and 2.","marker":"[13]"},{"why":"The prior secure state reconstruction method for differentially flat nonlinear systems, which this paper goes beyond by using observability maps instead of flatness.","marker":"[14]"},{"why":"Defines the zero-order control barrier function with the $\\epsilon$ margin that both safety filters enforce.","marker":"[22]"},{"why":"Cited to justify $s$-sparse observability as a necessary condition for detecting attacks on $s$ sensors.","marker":"[24]"},{"why":"Provides the numerical derivative estimator used to construct observability maps for the unicycle simulation.","marker":"[29]"},{"why":"Supplies the robust control barrier function formulation the relaxed filter (26) is built on.","marker":"[30]"},{"why":"Gives the $T^5$ truncation bound for Runge-Kutta integration used to justify a small process-disturbance bound $\\bar{w}$.","marker":"[25]"}],"fun_headline_variants":["Observability maps shield nonlinear systems from sensor spoofing","Attack-robust safety filter for nonlinear systems under spoofing","Secure nonlinear safety filter defeats sensor spoofing attacks","Observability-based filter blocks spoofed sensors in nonlinear systems"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The relaxed-case guarantees stand on an unproved step: for nested sensor sets, consistency of data from the larger set must imply consistency of the smaller set and nonempty intersection of their two estimate sets ($L_D^{\\Gamma_1}\\cap L_D^{\\Gamma_2}\\neq\\varnothing$), a claim stated as Lemma 2 in Section IV with its proof omitted; if that step fails, the $B_{4\\delta}$ bound and the relaxed safety guarantee no longer follow.","fun_headline_variants_meta":{"raw":{"variants":["Observability maps shield nonlinear systems from sensor spoofing","Attack-robust safety filter for nonlinear systems under spoofing","Secure nonlinear safety filter defeats sensor spoofing attacks","Observability-based filter blocks spoofed sensors in nonlinear systems"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000796,"raw_usage":{"total_tokens":3517,"prompt_tokens":971,"completion_tokens":2546,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":587,"completion_tokens_details":{"reasoning_tokens":2477}},"tokens_in":587,"tokens_out":2546,"duration_ms":18772,"temperature":1.0,"reasoning_tokens":2477,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T22:31:56.775399+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run a search over a nonlinear system that is $\\delta$-bounded observable, with nested sensor sets $\\Gamma_1\\subset\\Gamma_2$, for input-output data that is consistent for $\\Gamma_2$ under (19) but for which $L_D^{\\Gamma_1}\\cap L_D^{\\Gamma_2}=\\varnothing$; a single such instance would refute the $B_{4\\delta}$ bound of Corollary 2 and the relaxed $2s$-sparse guarantee. For the exact claim, simulate a $2s$-sparse observable sampled-data nonlinear system with an omniscient $s$-sensor spoofing attack and check whether the QP (13), feasible at every step, ever lets $h(x(t))<0$; any violation would refute Theorem 1.","supporting_citations":[{"cited_title":"Safety of linear systems under severe sensor attacks,","cited_arxiv_id":null,"evidence_quote":"The linear-system secure safety filter that this paper generalizes; its feasibility and redundancy arguments are the template for Theorems 1 and 2."},{"cited_title":"Secure state reconstruction in differentially flat systems under sensor attacks using satisfiability modulo theory solving,","cited_arxiv_id":null,"evidence_quote":"The prior secure state reconstruction method for differentially flat nonlinear systems, which this paper goes beyond by using observability maps instead of flatness."},{"cited_title":"A coding theoretic view of secure state reconstruction,","cited_arxiv_id":null,"evidence_quote":"Cited to justify $s$-sparse observability as a necessary condition for detecting attacks on $s$ sensors."},{"cited_title":"Nonlinear observers with tighter online error bounds,","cited_arxiv_id":null,"evidence_quote":"Provides the numerical derivative estimator used to construct observability maps for the unicycle simulation."},{"cited_title":"Robust control barrier functions for constrained sta- bilization of nonlinear systems,","cited_arxiv_id":null,"evidence_quote":"Supplies the robust control barrier function formulation the relaxed filter (26) is built on."},{"cited_title":"Stuart and A","cited_arxiv_id":null,"evidence_quote":"Gives the $T^5$ truncation bound for Runge-Kutta integration used to justify a small process-disturbance bound $\\bar{w}$."}],"review_version":1}