Pith. sign in

REVIEW 3 major objections 4 minor 33 references

A new system called Knox can statically verify safety rules for smart-home routines, guaranteeing that no possible concurrent interleaving that violates a rule is ever missed.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-03 11:50 UTC pith:C7DT3RTT

load-bearing objection The stress-test is correct: Knox's no-false-negative guarantee fails because false-positive routines are filtered out of concurrent checks. the 3 major comments →

arxiv 2607.29198 v1 pith:C7DT3RTT submitted 2026-07-31 cs.DC

Knox: Fortifying Smart Spaces With Safety Guarantees

Rishabh Menezes , Jadon T. Schuler , Kaimeng Zhu , Oliver Rogalski , Indranil Gupta This is my paper
classification cs.DC
keywords IoT safetysmart home routinesstatic verificationsafety clausesconcurrent routine safetycut-based checkingfalse negativesSafron grammar
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Knox aims to prove that safety in smart spaces can be checked statically — at submission time, before any routine executes — even though the underlying problem is computationally hard. The paper introduces Safron, a grammar for writing safety clauses such as "if the camera is on, some light must be on," and two cut-based algorithms that check a single routine and arbitrary groups of concurrent routines against all clauses. Its central guarantee is that Knox never misses a real safety violation, at the price of occasionally flagging a harmless situation; the authors report false-positive rates below 4% in their experiments. If the guarantee holds, hub controllers could reject unsafe automations as soon as they are submitted and explain exactly which commands could cause a violation.

Core claim

The paper's core claim is that for any set of branch-free routines and any Safron safety rule, Knox's cut-based checker reports every location vector from which some interleaving and some initial state can violate the rule, with per-rule explanations, and does this without enumerating interleavings. The mechanism is to represent each rule as a stateful tree, record for each leaf at a cut whether a routine has set it true, false, unset, or in conflict, and then assign every unset or conflicting leaf its "attack state" — the value that brings the rule closer to violation. The paper proves that no real violation can be hidden by this worst-case filling for single routines and, under stated cond

What carries the argument

The central object is the multi-routine cut: a location vector recording how many commands each routine has completed, paired with a merged cut-state list recording, for every leaf of a rule's parse tree, whether the most recent writes make that leaf true, false, unset, or in conflict. The Cut Contextualizer turns a cut into a stateful tree by replacing unset and conflict leaves with their attack state; because merge operations are commutative and associative, cuts can be combined cheaply. The Attack/Defense optimization classifies commands as attack, defense, or ambiguous to skip provably safe or provably unsafe regions of the lattice, and Wall/Siege maintains only the shrinking set of leav

Load-bearing premise

The no-false-negatives guarantee rests on the assumption that replacing every unknown or conflicting device state with its worst-case value can only push the rule toward violation, and that these per-leaf worst-case choices remain consistent even when one device appears in several leaves of the same rule.

What would settle it

Run Knox side-by-side with exhaustive enumeration of all interleavings and all initial states on a small smart space, targeting rules that mention the same device in more than one leaf and routines that leave that device unset; any violation brute force finds that Knox does not report would refute the central claim. A focused version of the paper's own brute-force comparison on such duplicate-device rules is enough to test the guarantee.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • Every safety rule can be checked against every newly submitted routine at the hub before the routine is allowed to run, so violations are caught without waiting for runtime.
  • Because checking covers full location vectors rather than pairwise routine comparisons, violations that require three or more routines acting together are detected.
  • Each reported violation is accompanied by the rule that was violated and the specific commands whose most recent writes set the relevant leaves, giving users actionable feedback.
  • The no-false-negatives property holds regardless of the initial state of the smart space, so users do not need to know or control device states when submitting routines.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: If the same cut-based worst-case reasoning transfers to security invariants, static checking could be extended from safety clauses to general policy enforcement, letting hubs reject routines that violate privacy or access rules.
  • Editorial inference: A natural next step is to make the proof cover rules that mention the same device in multiple leaves; the paper currently treats duplicate-device leaves only as a source of false positives, so a consistent worst-case assignment for those leaves would close the main gap in the guarantee.
  • Editorial inference: The authors leave dynamic checking to future work, but the same cut lattice could be reused as runtime checkpoints, giving continuous safety verification as routines execute rather than only at submission time.
  • Editorial inference: The Wall/Siege short-circuit — once no leaf remains that can satisfy a rule, further cuts are trivially unsafe — is a general monotone-pruning idea that could apply to other concurrency analyses beyond IoT routines.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper presents Safron, a grammar for specifying safety rules in IoT-enabled smart spaces, and Knox, a static checker that analyzes single-routine and concurrent-routine safety using cut-based worst-case evaluation. The authors claim that Knox is complete (zero false negatives), provide formal theorems to that effect, introduce two optimizations (Attack/Defense and Wall/Siege), and report experiments showing large speedups over brute force and TapChecker, with low false-positive rates.

Significance. If the central correctness claim were valid, this would be a valuable contribution: the grammar is expressive, the cut-based approach is intuitively appealing and explainable, the appendices contain formal proofs of the main theorems, and the experimental evaluation is extensive. However, the no-false-negatives guarantee is not merely unproven for the full grammar; it is false for the pipeline as described. The concrete counterexample below shows that Knox can miss a real concurrent safety violation because of false positives from duplicate-device leaves combined with the filtering of UnsafeRoutines. This directly contradicts the headline claim and substantially weakens the practical and theoretical contributions.

major comments (3)
  1. [Section V-I (Algorithm 3), Section V-F] The core pipeline runs ConcurrentSafety only on SafeRoutines (Algorithm 3, line 6). A false positive in Single Routine Safety therefore removes a routine from all concurrent checks. False positives are explicitly possible when a rule has multiple leaves for the same device, as acknowledged in Section V-F. This creates a false-negative path. Concretely, let S0 be satisfiable and such that routines R1,R2,R3 have a triple concurrent violation (as in Fig. 1) while each routine is individually safe. Add fresh binary devices A,B not touched by any routine, and set S = S0 AND ((A==ON AND B==ON) OR (A==OFF AND B==OFF)). This rule is satisfiable and non-degenerate. At location 0 of any routine, all four A/B leaves are unset, so the Cut Contextualizer sets each to its attack state (false); the XNOR conjunct evaluates false, making the whole tree false. Algorithm 4 therefore places every routine in
  2. [Theorem V.16 and Appendix proof] The theorem states completeness for arbitrary routine groups, but the proof's key step—changing leaves from their assumed attack states to the actual defense states preserves rule satisfaction—requires that attack/defense assignments be globally consistent. The paper explicitly permits multiple leaves per device (Section V-F), and in that case the assignments can be contradictory. In the rule above, leaves A==ON and A==OFF are both set to false under the attack-state assignment, yet a real state can make exactly one of them true. The monotonicity argument fails, so the theorem as stated is not established for the full grammar. The paper's own Section V-F treats the duplicate-leaf contradiction only as a source of false positives, not as a threat to completeness.
  3. [Section VI-B, Theorem VI.8] The stated runtime O(V·L_S + (|R| choose L_S)·|Rmax|^{L_S}·N_S) is asserted with a one-sentence proof sketch. It is not shown that the second term bounds the number of safety evaluations under the wall/siege scheme, nor that it is asymptotically smaller than the baseline V·N_S. For L_S close to |R|, the binomial term can be exponential in |R| at a rate comparable to V. The claimed theoretical advantage of Wall/Siege over Baseline is therefore not established independently of the experimental results.
minor comments (4)
  1. [Section I] Typo: 'static verificati on' should be 'static verification'.
  2. [Section V-F] The discussion of the degenerate rule 'AC == ON OR AC == OFF' says it 'would not be admitted to the system,' but nothing in the grammar or the feasibility check rejects such a rule. If the admission policy is meant to exclude such rules, it should be stated explicitly.
  3. [Definition V.9] The notation l'_i is used in the definition of predecessor cuts but is not explicitly defined as the i-th component of I'. Please clarify.
  4. [Section VII-A] For complex workloads, the paper reports that brute force 'took too long to measure' without giving a timeout or a lower bound on the runtime. A concrete cutoff would make the comparison more informative.

Circularity Check

0 steps flagged

No load-bearing circularity; the safety claim is defined independently of the checker and anchored to external brute-force/TapChecker baselines. The only self-citations are non-load-bearing related work.

full rationale

Knox's headline safety guarantee is anchored to an independent semantic object: an actual violation is an interleaving and initial state that make a Safron rule false (Sections I, V-D), not merely a cut that Knox's own attack/defense heuristic flags. The cut contextualizer is a pessimistic oracle whose completeness is separately argued (Theorems V.15-V.20) and empirically checked against brute-force simulation and TapChecker (Tables VIII-X). I found no curve where a fitted parameter is renamed as a prediction, and no theorem whose conclusion is imported by definition. The only self-citations [2,3] are SafeHome papers used as orthogonal related work ('SafeHome can use Knox orthogonally'); they do not supply a premise for Knox's algorithms, complexity results, or claims of zero false negatives. The skeptical UnsafeRoutines-filtering example is a genuine completeness concern about Algorithm 3 restricting ConcurrentSafety to SafeRoutines while false positives are admitted, but that is a soundness/correctness gap in the proof chain, not a circular reduction. The low non-zero score reflects only the presence of non-load-bearing self-citation.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 0 invented entities

The central result rests on a small IoT system model (branch-free routines, atomic commands, no failures, time-free rules) plus Knox's own conservative abstraction: unknown/conflicting leaves are set to their attack state. There are no fitted parameters. The most fragile entry is the monotonicity of attack/defense semantics in the presence of multiple leaves for the same device; the paper treats contradictory worst-case assignments only as a false-positive source. This ledger is why correctness risk is medium rather than low.

axioms (5)
  • domain assumption Routines are finite sequences of commands with no conditionals or branches; each command atomically changes a device state.
    Section II states this is consistent with Alexa/Google Home routines; it is what lets routines be represented as ordered commands and cuts as location vectors.
  • domain assumption Device state may be modified only by commands; hub and devices do not fail during checking.
    Section II explicitly declares the no-failure assumption and leaves dynamic failures to future work; without it the static 'no interleaving violates' claim would need fault modeling.
  • domain assumption Initial device states are arbitrary and unknown; safety must be guaranteed from any starting state.
    Section V.A and Theorem V.18 construct initial states from attack states; the arbitrary-initial-state assumption makes the worst-case cut semantics necessary.
  • domain assumption Safety rules are quantifier-free and time-free Boolean predicates over device states and hold at all times.
    Section IV: the Safron grammar has no temporal operators, so the checker can evaluate rule satisfaction on cuts rather than on traces.
  • ad hoc to paper Replacing every unset/conflict leaf by its attack state is a sound over-approximation of all completions, and the attack-to-defense transition is monotone with respect to rule satisfaction.
    This is Knox's core design heuristic (Definition V.6, Algorithm 2). It is proved for trees with one leaf per device but only partially discussed for duplicate-device leaves; if false, the no-false-negatives claim fails. It is not an assumption forced by the problem, so it is ad hoc to this paper.

pith-pipeline@v1.3.0-daily-deepseek · 18921 in / 27056 out tokens · 304018 ms · 2026-08-03T11:50:35.530047+00:00 · methodology

0 comments
read the original abstract

Internet of Things (IoT) devices in smart spaces and buildings are an emerging class of distributed systems with critical safety requirements. This paper presents Knox, the first system to enable safety checking in IoT-enabled smart spaces. Knox's contributions include (i) safety specifications: a new language for safety clauses in such smart spaces, and (ii) static safety checking: two new algorithms for static verification of multiple safety properties across multiple routines running inside a smart space. Since the latter problem is NP-hard, we present and analyze novel and explainable algorithms for the static version of the problem. We also present optimizations that further reduce runtime. Our analysis and experimental results with real datasets show that Knox reduces checking time significantly compared to baselines, while providing high accuracy in catching safety violations.

Figures

Figures reproduced from arXiv: 2607.29198 by Indranil Gupta, Jadon T. Schuler, Kaimeng Zhu, Oliver Rogalski, Rishabh Menezes.

Figure 1
Figure 1. Figure 1: Incompleteness of pairwise concurrent routine verification in TapChecker [8]: Based on a given safety rule’s semantics, some violations between 3 or more routines may never be caught. In the example, pairwise comparisons between R1, R2, and R3 will consider the overall rule satisfied, but will miss the conflict when all three run concurrently. APEX [31] targets safety in a smart space, accepting user￾submi… view at source ↗
Figure 2
Figure 2. Figure 2: Safron: Grammar for Safety Among Routines safety. SafeHome can use Knox orthogonally. Formal verification for distributed systems has flour￾ished [16], [17]. However, smart space users are lay users and cannot be expected to learn formal verification tools. IV. THE SAFRON GRAMMAR Knox allows safety clauses to be written using our Safron (Safety Among Routines) grammar, defined in [PITH_FULL_IMAGE:figures/… view at source ↗
Figure 3
Figure 3. Figure 3: Parse Tree Example For Rule 4 of Table II Original Clause Translation IF A THEN B !A OR B IF A THEN B ELSE C (!A OR B) AND (A OR C) EXACTLY k (...) AT MOST k (...) AND AT LEAST k (...) TABLE III Parsing Modifications Term Definition S Set of feasible safety rules D Set of all smart devices in the smart space Ds Set of all possible device states R Set of all routines in the smart space h Space state, a mapp… view at source ↗
Figure 4
Figure 4. Figure 4: Cuts and Cut Comparisons: Each routine can execute commands independently of others. Cuts can be compared if they share the same routine set — C1 and C2 cover R1 and R2 so they are comparable, but C3 includes state from R3, so it cannot be compared to either. < 80) to true, so the merged state is also true. Had Routine 2 instead been thermostat = 90 (violating the rule), the merged state would be a conflic… view at source ↗
Figure 5
Figure 5. Figure 5: Average runtime comparison for routines with different complex￾ity and distribution. not inside W are set to their attack state. Let L2 be a set of truth values generated by applying the Cut Contextualizer to C. Then L1 = L2. (Proof in Appendix) If a cut C does not remove any leaves from a wall after a siege, then it will similarly be ineffective on sieging a smaller wall (one with a subset of the original… view at source ↗
Figure 6
Figure 6. Figure 6: Device Scalability: Average runtime vs. number of devices. We observe that Baseline Knox (1) significantly reduces runtime over the default brute-force approach, and (2) achieves significant speedup, up to 3102× on simple routines (for com￾plex routines, Brute Force took too long to measure). Further, (3) our two optimizations—Attack/Defense & Wall/Siege— reduce runtime over Baseline Knox on complex routin… view at source ↗
Figure 7
Figure 7. Figure 7: Home Assistant Experiments: Average runtime comparison for realistic routines in a room simulation. (i) Attack/Defense and Wall/Siege both outperform Baseline by around 2.2×, and (ii) Wall/Siege is slightly faster than Attack/Defense. (Brute Force was prohibitively slow to test.) 50 Routines 500 Routines LR BR LR BR TapChecker .66 s .65 s 69.365 s 69.372 s Knox .029 s .027 s .238 s .239 s Speedup 22.76× 24… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

33 extracted references

  1. [1]

    @internetofshit,Internet of Shit, Feb. 2024. [Online]. Available: https://x.com/internetofshit

    2024

  2. [2]

    Home, SafeHome: Smart home reliability with vis- ibility and atomicity,

    S. B. Ahsan, R. Yang, S. A. Noghabi, and I. Gupta, “Home, SafeHome: Smart home reliability with vis- ibility and atomicity,” inProc. EuroSys ’21, Online Event, United Kingdom, 2021, pp. 590–605,ISBN: 9781450383349.DOI: 10.1145/3447786.3456261

    arXiv 2021

  3. [3]

    Home, SafeHome: Ensuring a safe and reliable home using the edge,

    S. B. Ahsan, R. Yang, S. A. Noghabi, and I. Gupta, “Home, SafeHome: Ensuring a safe and reliable home using the edge,” inHotEdge 19, 2019

    2019

  4. [4]

    Amazon,Amazon Alexa, Jan. 2024. [Online]. Available: https://developer.amazon.com/en-US/alexa

    2024

  5. [5]

    Apple,Apple Home, Jan. 2024. [Online]. Available: https://www.apple.com/home-app/

    2024

  6. [6]

    cvc5: A versatile and industrial-strength SMT solver,

    H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. N ¨otzli, A. Ozdemir, M. Preiner, A. Reynolds, Y . Sheng, C. Tinelli, and Y . Zohar, “cvc5: A versatile and industrial-strength SMT solver,” in TACAS ’22, ser. Lecture Notes in Computer Science, vol. 13243, 2022, pp. 415–442.DOI: 10.1007/978-3- 030...

    doi:10.1007/978-3- 2022

  7. [7]

    How users interpret bugs in trigger-action programming,

    W. Brackenbury, A. Deora, J. Ritchey, J. Vallee, W. He, G. Wang, M. L. Littman, and B. Ur, “How users interpret bugs in trigger-action programming,” inProc. CHI ’19, 2019, pp. 1–12,ISBN: 9781450359702.DOI: 10.1145/3290605.3300782

    arXiv 2019

  8. [8]

    TapChecker: A lightweight SMT-based conflict analysis for trigger-action programming,

    L. Chen, C. Wang, C. Chen, C. Huang, X. Chen, and M. Zhang, “TapChecker: A lightweight SMT-based conflict analysis for trigger-action programming,”IEEE IoT Journal, vol. 11, no. 12, pp. 21 411–21 426, 2024. DOI: 10.1109/JIOT.2024.3374556

    arXiv 2024

  9. [9]

    Em- powering end users in debugging trigger-action rules,

    F. Corno, L. De Russis, and A. Monge Roffarello, “Em- powering end users in debugging trigger-action rules,” inProc. CHI, 2019, pp. 1–13,ISBN: 9781450359702

    2019

  10. [10]

    Principles of smart home control,

    S. Davidoff, M. K. Lee, C. Yiu, J. Zimmerman, and A. K. Dey, “Principles of smart home control,” inProc. Ubicomp, 2006, pp. 19–34,ISBN: 9783540396345

    2006

  11. [11]

    Programming and symbolic computation in Maude,

    F. Dur ´an, S. Eker, S. Escobar, N. Mart ´ı-Oliet, J. Meseguer, R. Rubio, and C. Talcott, “Programming and symbolic computation in Maude,”Journal of Logical and Algebraic Methods in Programming, vol. 110, p. 100 497, 2020,ISSN: 2352-2208.DOI: 10 . 1016 / j . jlamp . 2019 . 100497 [Online]. Available: https : / / www . sciencedirect . com / science / artic...

    2020

  12. [12]

    fabiom91,HomeKit unreliable: Unresponsive acces- sories, Mar. 2022. [Online]. Available: https : / / discussions.apple.com/thread/253711255

    arXiv 2022

  13. [13]

    Google,Create and manage routines for Google Home automations, Jan. 2024. [Online]. Available: https : / / support.google.com/googlenest/answer/7029585

    arXiv 2024

  14. [14]

    Google,Google Home, Jan. 2024. [Online]. Available: https://home.google.com/welcome/

    2024

  15. [15]

    [On- line]

    Grand-View-Research,Smart home market, 2026. [On- line]. Available: https://www.grandviewresearch.com/ industry-analysis/smart-homes-industry

    2026

  16. [16]

    Finding invariants of distributed systems: It’s a small (enough) world after all,

    T. Hance, M. Heule, R. Martins, and B. Parno, “Finding invariants of distributed systems: It’s a small (enough) world after all,” inNSDI ’21, Apr. 2021, pp. 115–131, ISBN: 978-1-939133-21-2

    2021

  17. [17]

    IronFleet: Proving safety and liveness of practical distributed systems,

    C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. Setty, and B. Zill, “IronFleet: Proving safety and liveness of practical distributed systems,”CACM, vol. 60, no. 7, pp. 83–92, 2017,ISSN: 0001-0782.DOI: 10.1145/3068608

    doi:10.1145/3068608 2017

  18. [18]

    When smart devices are stupid: Negative experi- ences using home smart devices,

    W. He, J. Martinez, R. Padhi, L. Zhang, and B. Ur, “When smart devices are stupid: Negative experi- ences using home smart devices,” inIEEE SPW, 2019, pp. 150–155.DOI: 10.1109/SPW.2019.00036

    arXiv 2019

  19. [19]

    HomeAssistant,Home Assistant developer docs, Oct

  20. [20]

    IFTTT,IFTTT, Jan. 2024. [Online]. Available: https : //ifttt.com/

    2024

  21. [21]

    IoT-Analytics,IoT Startup Landscape 2024: 7 notable insights, Jul. 2024. [Online]. Available: https : / / iot - analytics.com/iot-startup-landscape/

    2024

  22. [22]

    IoT-Analytics,State of IoT 2025: Number of connected IoT devices growing 14% to 21.1 billion globally, Oct

    2025

  23. [23]

    SIFT: Building an internet of safe things,

    C.-J. M. Liang, B. F. Karlsson, N. D. Lane, F. Zhao, J. Zhang, Z. Pan, Z. Li, and Y . Yu, “SIFT: Building an internet of safe things,” inProc. IPSN ’15, 2015, pp. 298–309,ISBN: 9781450334754.DOI: 10 . 1145 / 2737095.2737115

    arXiv 2015

  24. [24]

    LowRange,A warning not to rely on SmartThings, Jan. 2021. [Online]. Available: https : / / community . smartthings . com / t / a - warning - not - to - rely - on - smartthings/218296

    2021

  25. [25]

    MEGATOMI,HomeKit automations are broken in iOS 16, Sep. 2022. [Online]. Available: https://discussions. apple.com/thread/254199872

    arXiv 2022

  26. [26]

    Mett03,HomeKit automation not working after iOS 17, Sep. 2023. [Online]. Available: https : / / discussions . apple.com/thread/255155940

    arXiv 2023

  27. [27]

    IOTA: A calculus for internet of things automation,

    J. L. Newcomb, S. Chandra, J.-B. Jeannin, C. Schlesinger, and M. Sridharan, “IOTA: A calculus for internet of things automation,” inProc. SIGPLAN On- ward! ’17, 2017, pp. 119–133,ISBN: 9781450355308. DOI: 10.1145/3133850.3133860

    arXiv 2017

  28. [28]

    Samsung,Samsung service terms and conditions - SmartThings services supplement, Feb. 2024. [Online]. Available: https://v3.account.samsung.com/policies/ specials/smartthings.html

    2024

  29. [29]

    Samsung,Samsung SmartThings, Jan. 2024. [Online]. Available: https://www.smartthings.com/

    2024

  30. [30]

    tomg15,HomeKit automations not working (again), Nov. 2022. [Online]. Available: https : / / discussions . apple.com/thread/254390066

    arXiv 2022

  31. [31]

    APEX: Automatic precondition execution with isolation and atomicity in internet-of- things,

    Q. Zhou and F. Ye, “APEX: Automatic precondition execution with isolation and atomicity in internet-of- things,” inProc. IoTDI ’19, 2019, pp. 25–36,ISBN: 9781450362832.DOI: 10.1145/3302505.3310066 APPENDIX Theorem V .1(NP-Hardness: Single).The Single Routine Safety problem is NP-hard. Proof.We prove for just one safety rule. LetSingleRouti- neSafetybe an ...

    arXiv 2019

  32. [2024]

    Available: https : / / developers

    [Online]. Available: https : / / developers . home - assistant.io/

  33. [2025]

    Available: https : / / iot - analytics

    [Online]. Available: https : / / iot - analytics . com / number-connected-iot-devices/