arXiv CSopen access

Knox: Fortifying Smart Spaces With Safety Guarantees

Knox: Fortifying Smart Spaces With Safety Guarantees Rishabh Menezes, Jadon T. Schuler, Kaimeng Zhu, Oliver Rogalski, Indranil Gupta

arXiv:2607.29198v1 [cs.DC] 31 Jul 2026

University of Illinois at Urbana-Champaign {menezes4, jadonts2, kaimeng2, oliverr3, indy}@illinois.edu

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.

I. I NTRODUCTION In a smart space—a home, building, or campus—Internet of Things (IoT) devices from multiple vendors cover all aspects of operation, including smart plugs, windows, doors, kitchen appliances, gardening, and cleaning. The smart home market alone is expected to grow from $127 B today to over $500 B by 2030 [15], with an expected 39 Billion IoT devices [22] from 3000+ vendors [21]. Devices are coordinated by a central hub, such as Alexa [4], Google Home [14], or SmartThings [29], which (i) communicates with IoT devices through the wireless network, and (ii) launches user-programmed automations. The most common form of automation today is called a routine [4], [5], [14], [20], [29]. A routine is a (small) program containing a sequence of commands, each executing one operation on one device; thus a routine may access different devices. Once submitted by a user, routines are held by the hub, and each is activated via one or more triggers: time, a sensor (e.g., thermostat setting crossing a threshold temperature), or the actions of another routine. Any routine may also be manually triggered at any time by the user via an app, their voice, etc. Example routines are: Accepted for publication in the Proceedings of the 2026 IEEE International Symposium on Reliable Distributed Systems (SRDS). This is the authors’ extended version, which additionally includes the full proofs of all theorems in the appendix. © 2026 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.

• R1: ⟨Trigger: time = 8pm⟩ outdoorCamera = ON; door = LOCKED; porchLight = ON; • R2: ⟨time = 1am⟩ porchLight = OFF; • R3: ⟨no motion for 10 mins⟩ floodLight=OFF;

When a routine is triggered, the hub sequentially launches its commands (IoT devices themselves do not manage routines, as device firmware is immutable). As routines may be triggered by time, sensors, or user input, it is common for arbitrarily many routines to be running concurrently inside a smart space. This creates a major reliability challenge that a smart space as a whole may enter unsafe and unreliable states [1]. Maintaining reliability in a smart space requires that users have the ability to specify safety expectations that hold across the space at all times, i.e., common concerns regardless of which routines are running. These safety expectations range from life-critical (e.g., camera’s field of view must be lit, or exhaust fan must be on whenever oven is on) to everyday concerns (e.g., TV must not come on during an ongoing Zoom call). It is unreasonable to hope that users will carefully architect each routine to satisfy their myriad safety expectations; safety clauses must therefore be specified separately from routines. Unfortunately, today’s automation systems are best-effort only. They neither allow users to specify safety clauses nor detect violations. Google Home states that “routines are for convenience only, not safety- or security-critical use cases” [13], and Samsung SmartThings recommends avoiding devices “which could cause damage to or loss of any property” [28]. Yet smart spaces are safety critical, and incidents continue to violate users’ reliability expectations [12], [25], [26], [30], e.g., a failed automation overheated a room to 40°C [24]. This paper presents the theoretical foundations for Knox, the first system to ensure static safety in smart environments, allowing both specification and automatic static checking of an arbitrary number of safety clauses under an arbitrary number of routines and devices. An example safety clause in Knox is: S1: IF (outdoorCamera == ON) THEN (porchLight == ON OR floodLight == ON).

At night, this safety clause ensures that whenever the camera is on, there is sufficient light in its field of view. Yet, since outdoorCamera, porchLight, and floodLight can each be switched on or off by other concurrent routines, the clause may be violated: given routines R1, R2, and R3 above, S1 is violated at 1 am. If any combination of a set of routines

has the possibility of violating a safety clause, the system is unsafe and should be detected as such when R1, R2, R3, and S1 are submitted to the hub. Today, there are no methods for specifying S1, nor algorithms for the hub to detect if a given set of routines could ever violate it. In this paper we (I) propose a new grammar for specifying safety clauses in a smart space and (II) design and analyze algorithms for statically checking a set of safety clauses for a given set of routines, reporting all safety violations. Our system, Knox, is safe: it does not miss any safety violations. Concretely, under (II), we need to solve three problems: 1. Feasibility: Existence of at least one space state where all safety clauses are satisfied. 2. Single Routine Safety: When a new routine is first written and submitted to the hub, that routine itself does not violate any safety clauses. 3. Concurrent Routine Safety: Given a set of submitted routines at the hub, find all subgroups of routines with at least one interleaving that violates any safety clause. An additional requirement is Explainability: for detected violations of either Single Routine Safety or Concurrent Routine Safety, we should pinpoint the exact commands that violated a given safety clause. As misunderstandings of concurrent program behavior in IoT environments are common among novice-programmer users [7], [9], [18], [27], this feedback helps identify and fix culprit routines. We solve the static versions of these problems where all checks run when a new routine or a new safety clause is submitted to the hub. This has the advantage of securing all static safety properties before runtime, so no dynamic checks of the same properties are needed. (Dynamic issues, including failures, are beyond our current scope and are left for future work.) First, the smart space’s devices may be in arbitrary initial states, making safety checking (2) & (3) hard. Second, the state space is finite, but massive. In a smart space with only 30 devices, each of which can be in one of 4 states (e.g., HI, MED, LO, OFF), there are over 1018 unique states! This means manual checking is untenable, and even automated brute-force solutions are too slow. Model checkers specialized for infinite-state systems are also unsuitable [11]. Feasibility (1) turns out to be easy to solve: an SMT (Satisfiability Modulo Theories)-based solver suffices. However, for Single Routine Safety (2) and Concurrent Routine Safety (3), large state spaces make SMT-based approaches prohibitively expensive—with R routines each containing k possible interleavings! Naively instructions, there are (Rk)! (k!)R checking safety for each command pair of every interleaving · Rk) times. Our new techniques are instead runs SMT ( (Rk)! (k!)R guided by the principle of erring on the side of safety: they detect all safety violations and never miss any (zero false negatives), though false positives may occur, i.e., Knox may flag a few cases that are not actually violations (we measure this). The contributions of this paper are: 1) A new expressive grammar for specifying safety clauses in IoT settings (Section IV).

2) New fast algorithms for Single and Concurrent Routine Safety checking (Section V). 3) Two new optimizations to reduce runtime (Section VI). 4) Formal proofs of correctness (Sections V & VI). 5) Experiments to measure speed & accuracy, comparison vs. a baseline (Section VII). To the best of our knowledge, Knox provides the first fully-specified formal grammar and associated safety checking algorithms for efficient static verificati on of concurrent automations in smart space environments. II. S YSTEM M ODEL Knox makes the following system assumptions. Physical Components: The smart space consists of a single centralized hub and a series of devices: • Devices have different types of state — including binary (on, off), multi (colors, operation modes), or numerical (light intensity, temperature). • Each device can receive and execute device-specific commands. E.g., for a smart plug: {ON, OFF}. For a sprinkler, {ON, OFF, flow:0-100}. • A centralized hub stores and initiates routines (by time, sensor value, manual, etc.) that control any present devices by issuing commands. Examples are Alexa, Google Home Hub, Samsung Smart Things hub, etc. • Neither the hub nor the devices fail. We will show that even without failures, which we leave to future work, safety violations pose a challenging problem. Logical Components: These assumptions define command execution and organization: • Commands are device specific and may be short (e.g., light on) or long (e.g., preheat oven, open garage door, etc.). • Routines contain a finite sequence of commands, without any conditionals or branches (this is consistent with routines in Alexa, Google Home, etc.). • A device’s state may only be modified by a command. • One or more submitted routines exist, held at the hub. • Once triggered, a routine’s commands execute sequentially. • A routine may be activated (triggered) at any arbitrary time. Multiple routines may be active simultaneously (including multiple copies of the same routine). We define the state space as the collective mapping of all devices to their respective states. III. R ELATED W ORK Classical human-computer interaction work indicates that smart space application design must anticipate conflicting goals: smart space software should help users “manage their lives rather than manage individual devices” [10]. Table I summarizes the closest related work w.r.t. our goals: static and dynamic safety checks, an expressive safety language, and support for routines. To the best of our knowledge, Knox is the first to satisfy all four (its static checking also ensures no dynamic conflicts).

Auditor

Static

Dynamic

Expressive

Routines

SafeHome [3] APEX [31] SIFT [23] TapChecker [8] Knox

✗ ✗ ✓ ✓ ✓

✗ ✓ ✗ ✗ implied

✓ N/A ✗ ✓ ✓

✗ ✗ ✗ ✗ ✓

TABLE I

Related Systems Comparison: We compare safety checkers by the properties they consider: static (submission time) or dynamic (run time). We also consider how expressive their rules can be and their support for routine programming.

Safety Rule

Explanation

1. thermostat>60 AND thermostat<80

Regulate Temp. Range

2. AT MOST 2 (sprinkler1==ON, sprinkler2==ON, sprinkler3==ON)

Insufficient Water Pressure

3. IF window==OPEN THEN AC==OFF

Energy Savings

4. IF (backyardGrill==ON OR backyardSmoker==ON) THEN backyardWindow==CLOSED

Prevent indoor smoke

TABLE II Examples of Safron Safety Rules Fig. 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 usersubmitted preconditions which it satisfies before executing a command. But APEX fails to consider contrapositives. Consider 2 preconditions: 1. (AC ON =⇒ Window CLOSED), and 2. (Bleach counters =⇒ Window OPEN)1 . APEX treats these two rules independently. In turning on the AC, APEX first automatically closes the windows, even if there are bleach fumes in the kitchen! Not only does this allow rule violations, it may actively create new violations. SIFT [23] targets safety, but limits routines to a single command and its safety rules to conditionals, making it less expressive than Knox. TapChecker [8] uses SMT verification to detect various types of conflicts in trigger-action programming (TAP) statements, with SMT-expressible safety rules. As SMT expressions only capture a TAP statement’s end result, TapChecker cannot analyze multi-command routines or conflicts from concurrent interleavings, and it checks routines only pairwise, potentially allowing rule violations between 3 or more routines (Figure 1). Hence, while TapChecker never marks safe routines as unsafe (no false positives), it misses many potential violations (false negatives). Knox never misses any violations but has occasional false positives. Erring on the side of safety is more practical for real deployments, as Section VII’s experiments show. IOTA [27] is a formal calculus for modeling concurrent devices and automations to specify IoT programs. IOTA neither considers user-provided safety rules, nor optimizes conflict search beyond reducing predicates on numerical device state to boolean expressions, so its safety checking suffers from combinatorial interleaving, which Knox addresses. SafeHome [2], [3] features an “Eventual Consistency” scheduling algorithm for concurrent routines, but does not design or implement 1 In APEX, the LHS is a precondition for executing the RHS. We instead normalize arrow directions here for exposition.

RULE BINOP IMP SINGLE

NUM LIST ELEM ATOM OP

:= BINOP | IMP | ELEM := ELEM AND ELEM | ELEM OR ELEM := IF ELEM THEN ELEM ELSE ELEM | IF ELEM THEN ELEM := ANY(LIST) | ALL(LIST) | AT LEAST NUM (LIST) | AT MOST NUM (LIST) | EXACTLY NUM (LIST) | !ELEM | ATOM := [1-9][0-9]* := RULE, LIST | RULE := SINGLE | (RULE) := DeviceID.StateID OP value := == | < | > | <= | >=

Fig. 2. Safron: Grammar for Safety Among Routines

safety. SafeHome can use Knox orthogonally. Formal verification for distributed systems has flourished [16], [17]. However, smart space users are lay users and cannot be expected to learn formal verification tools. IV. T HE S AFRON G RAMMAR Knox allows safety clauses to be written using our Safron (Safety Among Routines) grammar, defined in Figure 2. Safety rules can come prebaked with the smart space or alternatively can be added at any time by a user. Admitted rules are held at the hub. The grammar is quantifier-free and time-free, as rules are expected to hold at all times. Table II shows example rules written in Safron. A base (ATOM) Safron clause expresses a boolean predicate on a single device’s state. Operations include standard boolean connectors such as NOT (!), AND, OR, and IF conditions, with ANY and ALL aggregate statements serving as syntactic sugar. k-constraint operators such as AT LEAST, AT MOST, and EXACTLY are common for smart spaces. Tree Representation of Safety Rules: We auto-translate each rule into a parse tree, first by rewriting (Table III) and then creating a tree (Figure 3). The leaves represent atomic device states (ATOM rule) and internal nodes are logical connectors (e.g., AND). Edges are subexpressions with logical connectors. V. K NOX A LGORITHMS A. Approach We outline Knox’s three key contributions below and detail them in the following sections. Table IV shows variable

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 (...)

Fig. 3. Parse Tree Example For Rule 4 of Table II

Term

Definition

S D Ds R h

Set of feasible safety rules Set of all smart devices in the smart space Set of all possible device states Set of all routines in the smart space Space state, a mapping h : D → Ds

TABLE IV Key Terms and Variables

TABLE III Parsing Modifications

false positives in certain conditions. Knox’s safety assurances hold no matter the initial space state. B. NP-Hardness Theorem V.1 (NP-Hardness: Single). The Single Routine Safety problem is NP-hard. (Proof in Appendix) The problem remains NP-hard even if the search starts from states that satisfy all safety rules, or safe states.

Routine

Explanation

outdoorCamera = ON; frontDoor = LOCKED; porchLight = ON;

Evening Safety Setup

Theorem V.2 (NP-Hardness: Safe Initial State). The Single Routine Safety problem, when limited to safe initial states, is NP-hard. (Proof in Appendix)

thermo.mode = FROSTGUARD; faucet.mode = DRIP;

Cold Weather Precautions

Theorem V.3 (NP-Hardness: Concurrent). The Concurrent Routine Safety problem is NP-hard.

TABLE V

Examples of Routines

definitions. Feasibility: Given a set of safety rules, denoted as S, is there at least one space state h : D → Ds that satisfies every rule in S? If rules are infeasible, no routine could ever be safe! Solving feasibility is equivalent to expressing safety rules as an SMT problem, so Knox uses an SMT solver, cvc5 [6]. The overhead is small since feasibility is only needs to be verified once for a given rule set, independent of routines, which change more frequently than rules. Hence we do not discuss Feasibility further. Single Routine Safety: Does a single routine violate any given rule in S? Table V provides routine examples, from which we introduce the cut, a point between execution of consecutive routine commands. Cuts use rule semantics to make a per-rule worst-case assumption of any relevant unset states, avoiding an exhaustive search of all unset state combinations. We check safety at cuts and derive a causal relation that extends per-cut analyses. Concurrent Routine Safety: Are there any interleavings among a given set of routines R which would violate at least one safety rule in S? We assume S, R satisfy both Feasibility and Single Routine Safety. We adapt the Single Routine Safety solution via multi-routine cuts: points in time between execution of consecutive commands that may be from different routines, while maintaining sequentiality within each routine. Completeness and Accuracy: Knox is complete and detects any existing safety violations, but may be inaccurate, reporting

Proof Sketch: Since Single Routine Safety is a special case of Concurrent Routine Safety, this is also NP-hard. As perfect solutions to these problems are not tractable, Knox’s approach makes use of heuristics and potentially allows false positives—a rule-satisfying safe routine could be marked as rule-violating, or unsafe. C. Stateful Trees Given one or more routines, analyzing a given tree (which represents one safety rule) requires capturing possible state changes caused by the routines. To do so, we instantiate each rule’s parse tree T as a stateful tree: Definition V.4 (Stateful Tree). A stateful tree ST is a map from each node in a rule parse tree T to a truth value, either true or false: ST : (n ∈ T ) → {true, false}. Each node’s state indicates whether that subclause (in the subtree rooted at that node) is considered satisfied (true) or not (false). Leaves are set to true if the device state is correct, e.g., Rule 4 in Table II will have window leaf (W0 in Figure 3) set to true if the window is indeed closed. For Rule 2, each of the three leaves is true if its respective sprinkler is ON. Once leaves are set, we propagate values up to the root, following internal nodes’ operations. Definition V.5 (Rule Satisfaction/Violation). If a stateful tree ST maps its root to true, then the rule is satisfied, else violated. Determining Rule Satisfaction or Violation takes O(NT ) time, where NT = number of nodes in T .

Operand 1

Operand 2

Result

Any cut state x Any cut state x Any cut state x true

x unset conflict false

x x conflict conflict

TABLE VI Merge Cut State Operation

D. Representing Device State Through Cuts Cuts (Section V-A) capture the space state as it pertains to a single rule between consecutive commands, either from a single routine or interleaved across multiple routines which allows us examine safe and unsafe space states without searching all interleavings. As we assume arbitrary initial device states, a device’s state in a cut (a leaf in a rule parse tree) can take on one of many values: Definition V.6 (Cut State). Each leaf l in a rule parse tree is set to one of the following cut states within a cut: • Unset: No routine has modified l’s truth value • Conflict: Two or more routines have set differing values • True: A routine set l to true, and no others set l to false • False: A routine set l to false, and no others set l to true Now we can formally define: Definition V.7 (Single Routine Cut). Given a rule parse tree T and routine Ri , a single routine cut contains: • Location: Similar to a “Program Counter”, an integer i ≥ 0, ≤ |Ri | representing how many commands of Ri have completed executing, i.e., a point between two commands. • Cut State List: A recording of the most recent cut state for each leaf in T . Note that conflict is not possible for a single routine. Example: Consider Table II’s Rule 1: thermostat > 60 AND thermostat < 80, with Routine thermostat = 72. The two leaves (> 60 and < 80) are both unset at location 0; at location 1, a temperature of 72 satisfies both conditions, so both map to true. Next we handle multiple interleaving routines: Definition V.8 (Multi-Routine Cut). Given a rule parse tree T and set of single routine cuts C across routine set RC , the multi-routine cut is the result of merging all cuts in C to form a single merged cut. It contains: • Location Vector: A vector of the locations li within each routine Ri in RC : < l1 , ..., li , ..., l|RC | >. • Merged Cut State List: Most recent merged cut states for each leaf in T . Merging is done via the rules in Table VI and is both commutative and associative. Example: Consider Rule 1 again, with two concurrent routines, Routine 1: thermostat = 72, and Routine 2: thermostat = 68, and the merged cut at location 1 of each. The ultimate thermostat setting may be unknown (since routines are concurrent), but this is unnecessary for safety checking—both single routine cuts set their leaves (> 60 and

Fig. 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 conflict. Ordering Cuts: We define a causal relationship among cuts, used in later analysis. It captures whether one cut follows another and applies transitively: a cut C is a causal predecessor of C ′ if, starting from C, one or more commands are executed to reach C ′ . Formally: Definition V.9 (Predecessor & Successor Cuts). Let cuts C, C ′ be defined as C = (I, M ), C ′ = (I ′ , M ′ ), where I and I ′ are location vectors {l1 , ..., ln } and {l1′ , ..., ln′ }, respectively, and M and M ′ are the respective merged cut state lists. Then C ′ precedes C iff for every i ∈ {1...n}, li′ ≤ li and ∃j ∈ {1...n} such that lj′ < lj . We also say that C succeeds C ′ . Definition V.10 (Immediate Predecessor and Immediate Successor Cuts). Let cut C have predecessor P . P is an immediate predecessor of C if and only if li′ = li for every i ̸= j ∈ {1...n} and lj′ = lj − 1 for some j. Hence, we also call C an immediate successor of P . This notion has similarities to vector timestamps: Figure 4 shows C1 preceding C2 , yet both are incomparable to C3 . E. Node Contribution When a leaf’s cut state is unset or conflict (Section V-D), its ultimate truth value—true or false—is still to be determined. Rather than enumerating all combinations across leaves, Knox adopts a heuristic that errs on the side of safety. We choose each leaf’s worst-case truth value, i.e., the one that brings the stateful representation of the root “closer” to false. To calculate this value for each node in a tree, we introduce the notion of that node’s contribution. A node’s setting contributes to exactly one of rule satisfaction or violation. A child set to true contributes to satisfaction of AND, OR, and AT LEAST subtrees. A child set to false contributes to satisfaction of NOT (‘!’ in the grammar) and AT MOST subtrees. For instance, in a disjunction A ∨ B ∨ C, setting more terms (leaves) to false brings the overall statement closer to false. As rules grow larger or use more complex Safron grammar elements (Section IV), a leaf setting’s effect on overall safety is no longer clear at a glance. Hence we define, for root and descendant:

Definition V.11 (Root Contribution). Let r be the root of a tree T with stateful tree mapping ST . If ST (r) = true, then we say r contributes to rule satisfaction. If ST (r) = false, then we say r contributes to rule violation. Definition V.12 (Descendant Contribution). Let A, D1 , ...DN be nodes of a tree T with stateful tree mapping ST , and let {D1 ...Dn } be descendants of node A. Let A have initial truth value sA . For arbitrary i ∈ {1...n}, there is a combination of truth values {sD1 , sD2 , ...sDn } − {sDi } such that when Di is set to value sDi , A’s value is changed to s′A , defined as s′A = ¬sA . s′A contributing to rule satisfaction for the subtree rooted at A is necessary and sufficient to state that sDi contributes to rule satisfaction for A. The same holds for rule violation. For contribution to be usable in analyzing state changes on a tree, it must be deterministic, meaning that a state assignment should have one outcome with respect to rule satisfaction or violation. The following theorem addresses this concern: Theorem V.13 (One-To-One Contribution). Given a tree T for a rule, and a node n ∈ ST , a specific truth value of node n can contribute only to exactly one of either rule satisfaction or rule violation. (Proof in Appendix) For example, in Table II’s Rule 4 (tree in Figure 3), turning off the backyard grill contributes to rule satisfaction. If the smoker is also off, the parent OR is set to false, inductively bringing the root closer to true. The same action can never make the parent OR true, so it only contributes to rule satisfaction. F. Attack and Defense States Given a safety rule (tree), a node state that brings the system closer to violating it is called an attack state. One that takes it away from violation is called a defense state. Formally: Definition V.14 (Attack and Defense States). Given a rule parse tree T and a stateful tree ST , if a node n ∈ T ’s truth value ST (n) contributes to ST ’s violation, we say n is in its attack state A. In contrast, if a node n ∈ T ’s value ST (n) contributes to ST ’s satisfaction, we say n is in its defense state D. By Theorem V.13, each possible truth value of a node is either an attack or a defense state. Hence every node must have both, depending on the tree structure. Now we can present Algorithm 1 to calculate attack and defense states. Analyzing a rule parse tree T takes O(NT ) time, where NT is the number of nodes P in T . For all rules, this takes O(NS ) time, where NS = T ∈S NT is the total number of nodes across all trees. Choosing Unset/Conflict States: When a leaf’s cut state (Section V-D) is either unset or conflict, we err on the side of caution, setting each of these leaves to their attack states (contributing to rule violation). A corner case occurs when multiple leaves within a rule refer to the same device, which may produce contradictory states. Ex.: for the degenerate rule AC == ON OR AC == OFF with unknown AC state,

Algorithm 1: Determining attack/defense states Input: Rule parse tree T Output: Modified rule parse tree with att/def states on nodes 1 foreach node n in a pre-order traversal of T do 2 if n is the root then 3 {n.attackState, n.defenseState} ← {false, true}; 4 else if n’s parent’s operation is AND, OR, or AT LEAST then 5 {n.attackState, n.defenseState} ← {n.parent.attackState, n.parent.defenseState} 6 else 7 {n.attackState, n.defenseState} ← {n.parent.defenseState, n.parent.attackState}; 8 end

we assume the worst case for both leaves: leaf AC == ON assumes the AC is off, and leaf AC == OFF assumes it is on. This is naturally one reason why Knox may experience false positives, though recurrence of a device in multiple clauses is rare in simple safety rules. (This degenerate rule is vacuously true, so it would not be admitted to the system.) G. Determining Cut Safety We now leverage cuts (Section V-D) to check for rule violations without having to enumerate all possible interleavings. The Cut Contextualizer algorithm (Algorithm 2) starts from a cut and constructs a stateful tree. It then makes worst-case decisions for leaves set to unset or conflict, while retaining settings of true or false. Algorithm 2: Cut Contextualizer Input: Rule parse tree T , Cut C Output: Stateful tree ST 1 foreach leaf l ∈ T do 2 ST (l) ← C(l) if C(l) is true or false; 3 ST (l) ← l.attackState otherwise; 4 end 5 Evaluate ST (Section V-C); 6 return ST ;

Theorem V.15. A cut C is safe at its location vector if the stateful tree ST via the Cut Contextualizer is satisfied. Proof. The stateful tree ST is an explicit evaluation of a safety rule (Section IV). Leaves set to true or false by the cut are guaranteed—all interleavings agree on this state. Leaves set to conflict or unset assume their attack state, which by Theorem V.13 must contribute to rule violation. Thus if the stateful tree’s root is set to true, then the values of explicitly known devices are sufficient for rule satisfaction. ■ In Algorithm 2, cut safety in a rule parse tree T with NT nodes takes O(NT )Ptime. A set of rules in S takes O(NS ) time, where NS = T ∈S NT . H. Correctness of Routine Safety To avoid exploring all interleavings among routines while checking for safety, we combine the fact that cuts record the worst-case result of interleavings up to their location vector with the notion of cut causality from Section V-D. The result is that cut safety can be extended to ensure interleaving safety, which we formalize below as a correctness theorem:

Theorem V.16 (Correctness of Routine Safety). Assume we have two safe multi-routine cuts C1 and C2, such that C1 precedes C2. If all cuts that succeed C1 and precede C2 are safe, then there exists no unsafe interleaving of the commands between C1 and C2’s location vectors. (Proof in Appendix) Corollary V.17. If all cuts in a routine or routine group are safe, then single/concurrent routine safety is satisfied. The above provides explainability for rule violation: 1) Given an unsafe interleaving, we can point to exactly which safety rule was violated. 2) We can provide the exact commands that may cause an unsafe interleaving for a rule by taking the most recent settings of non-defense leaves. 3) Using the causal relationship, we can determine that interleavings between subgroups of the checked routine set are safe. This holds even if an unsafe interleaving exists at a different location vector. I. Knox’s Baseline Routine Safety Algorithm 3 provides an overview of our system. We first analyze rules for their attack/defense states based on contribution (Section V-E). Then, Algorithm 4 finds and reports statically safe and unsafe individual routines by constructing and analyzing a stateful tree for each rule and single-routine cut. Finally, Algorithm 5 finds and reports all unsafe cuts by constructing and checking multi-routine cuts for every location vector in the routine set. Algorithm 3: Core System Input: Feasible safety rule parse trees S, Routines R, Devices D, Device States Ds Output: SafeRoutines, UnsafeRoutines, UnsafeCuts 1 foreach T ∈ S do 2 Analyze leaves in T for contribution (Section V-E); 3 end 4 Construct all single routine cuts; 5 SafeRoutines, UnsafeRoutines ← SingleRoutineSaf ety(S, R, D, Ds ) (Algorithm 4); 6 UnsafeCuts ← ConcurrentSaf ety(S, SafeRoutines, D, Ds ) (Algorithm 5); 7 return {SafeRoutines, UnsafeRoutines, UnsafeCuts};

1) Runtime Complexity Analysis: Single Routine Safety: To construct all single routine cuts, we consider all locations. We define P the total number of locations across all routines as K = Ri ∈R (|Ri | + 1). We assume a data structure mapping devices to leaves in rule parse trees, built when each routine is inserted in time proportional to the routine’s size. When examining a command, we consult the mapping to find the leaves modified while constructing a cut. For each location and rule, we construct the leaf mapping in O(LT ) time,P where LT is the number of leaves in tree T . Defining LS = T ∈S LT , constructing all single routine cuts across all rules takes O(K · LS ) time. For single routine safety, we simply check each of these single routine cuts for safety using the Cut Contextualizer (Algorithm 2), which takes O(K · NS ) time. Concurrent Routine Safety: This checks multi-routine cuts at Q each possible location vector. Define V = Ri ∈R (|Ri | + 1)

Algorithm 4: Single Routine Safety (Baseline Knox) Input: Feasible safety rule parse trees S, Routines R, Devices D, Device States Ds Output: SafeRoutines, UnsafeRoutines 1 SafeRoutines, UnsafeRoutines ← ∅; 2 foreach R ∈ R do 3 foreach T ∈ S do 4 if R has no effect on T then 5 continue; 6 foreach Single Routine Cut C in R do 7 Stateful Tree ST ← CutContextualizer(C); 8 if ST violated then 9 UnsafeRoutines ← UnsafeRoutines ∪{R}; 10 go to next routine; 11 end 12 end 13 SafeRoutines ← SafeRoutines ∪{R}; 14 end 15 return SafeRoutines, UnsafeRoutines;

Algorithm 5: Concurrent Routine Safety (Baseline Knox) Input: Feasible safety rule parse trees S, Routines r1..n , Devices D, Device States Ds Output: UnsafeCuts 1 UnsafeCuts ← ∅; 2 foreach location vector < i1 , ..., i|R| > do 3 Construct multi-routine cut C for this location vector; 4 Stateful Tree ST ← CutContextualizer(C); 5 if ST violated then 6 UnsafeCuts ← UnsafeCuts ∪{C}; 7 end 8 return UnsafeCuts;

as total number of location vectors. To construct all multiroutine cuts, we follow a lattice (using memoization), merging in one new single routine cut in O(LS ) time each iteration for a total runtime of O(V · LS ). For each, we must run the Cut Contextualizer to determine safety, for a total runtime of O(V · (LS + NS )). We note that V = O(|Rmax ||R| ), where Rmax has the maximum number of commands of any routine. The Cut Contextualizer complexity is linear, as opposed to using SMT to solve the Single and Concurrent Routine Safety problems, which would have made the complexity exponential. Adding and Removing Routines and Safety Rules: When a new rule is inserted, the above algorithms only check existing routines against that rule. A new routine is checked only against all existing rules, along with cuts involving all routines (this is unavoidable as the new routine will have interleavings with existing ones). Removal of routines or safety rules never Variable

Definition

Rmax K V NT NS LT LS

The maximum length routine Total single routine cut locations across all routines Total multi routine cut locations across all routines Node count in tree T Node count across all trees of safety rules in S Leaf count in tree T Leaf count across all trees of safety rules in S TABLE VII Recurring Runtime Analysis Variables

makes a safe system unsafe, though cuts previously considered unsafe may be updated. J. Reducing False Positives By design, Knox misses no unsafe cuts, but as it errs on the side of safety it may be prone to false positives: points in execution where a cut is identified as unsafe, but no interleaving from some initial state violates a rule. Under certain conditions, however, Knox can guarantee these cannot occur: Theorem V.18 (Single-Routine: Avoidance of False Positives). For a single routine, and a rule parse tree T , if T has at most one leaf for each device in the smart space, then Knox avoids false positives. (Proof in Appendix) We first extend notions of attack and defense states (from Section V-F): Definition V.19 (Command Classification: Attack, Defense, and Ambiguous Commands). For a rule parse tree, a command c is: (i) an attack command if c sets all affected leaves to attack states; (ii) a defense command if c sets all affected leaves to defense states; (iii) otherwise it is an ambiguous command. We call this derivation Command Classification. Intuitively, attack commands can only ever contribute to rule violation while defense commands do the opposite (w.r.t. a given rule). Ambiguous commands need special care, as they induce both attack and defense states. Example: Consider Table II’s Rule 3. Command AC = OFF is a defense command: the leaf AC == OFF would be set to true, which is its defense state. Command window = OPEN is an attack: setting leaf window == OPEN to true would put the leaf in attack state. Example: Consider the rule (A1 AND B2 ) OR A2 . The command A = A1 is ambiguous, setting leaf A == A1 to its defense state true, but A == A2 to its attack state false. Now we can prove that under some conditions, multi-routine safety incurs no false positives: Theorem V.20 (Multi-Routine: Avoidance of False Positives). An unsafe multi-routine cut C exists if and only if an unsafe interleaving exists for some initial state, provided either conditions (A1 AND A2) are true, or B is true, i.e.: • (A1) The rule parse tree T has at most one leaf for each device in the smart space, AND • (A2) For all leaves in C set to conflict, all routines execute attack commands after defense commands OR • (B) At most one leaf in C is set to conflict. VI. O PTIMIZATIONS Two optimizations further reduce safety checking runtime— Attack/Defense and Wall/Siege.

A. Attack/Defense First, we re-apply the Command Classifications on attack and defense commands (Definition V.19). This helps skip certain safety checks without violating completeness. Theorem VI.1 (Irrelevant Cuts). A cut that satisfies one of: • Case 1. Has a safe immediate predecessor, where lj′ is a defense command (recall Definition V.10) • Case 2. Has an immediate successor (no safety qualification needed), where lj′ is an attack command are irrelevant, and are not needed to detect rule violation. Proof. Consider an arbitrary cut C. We consider both cases: Case 1: Our cut has some safe immediate predecessor, with the differing command a defense. A defense only allows the leaf it touches to contribute towards rule satisfaction: • If the leaf was in its attack state in the immediate predecessor, then it will be a defense state if the attack was from the same routine or a conflict if not. • If the leaf was in conflict or defense states, it remains. • If the leaf was unset, it will be set to its defense state. In all three subcases, no leaf that contributed to rule satisfaction is changed to contribute to violation. Since the predecessor cut was already safe and the only changes increase the total leaves contributing to rule satisfaction, C remains safe, with no further checking required. Case 2: Our cut has some immediate successor, where the differing command is an attack. Attack commands allow only contributions to rule violation: • If the leaf was in its defense state in C then it is set to its attack state in the immediate successor (if defense was from the same routine as the attack command) or a conflict if not. • If the leaf was unset, then it is set to its attack state in the immediate successor. • If the leaf was in conflict or attack states, it remains. In all 3 subcases, the immediate successor’s leaf records an attack state. So if C was unsafe, all changes only raise the number of leaves violating the rule. Hence the immediate successor is unsafe, and we can skip checking C. ■ Theorem VI.2. If the multi-routine cut located before any routine commands execute is safe, then any cut located immediately after a defense command is irrelevant and can be skipped for safety checking. (Proof in Appendix) Theorems VI.1 and VI.2 are powerful because they imply that given a safe initial state, we need not evaluate immediate successors of defense commands. Hence the Attack/Defense optimization modifies the Baseline Knox algorithm of Section V-I by first executing Command Classification (Definition V.19) and then assuming a safe start. Multi-routine cuts are verified only if they are located (i) after the end of an attack command sequence, or (ii) after an ambiguous command. Its runtime is:

Theorem VI.3 (Attack/Defense Runtime). With P Kad = Ri ∈R |R2i | , runtime of checking concurrent routine safety after applying the Attack/Defense optimization is  |R| | O(NS + Kad · LS + Kad · NS + |Rmax · (LS + NS )) 2 (Notations are in Table VII). (Proof in Appendix)

B. Wall/Siege The nature of cut state merging (Table VI) leads us to another optimization. As we progress through the concurrent routine safety algorithm, we can limit our focus to only the leaves which contribute to rule satisfaction. The merge operation guarantees that this set can only shrink as we check more routines, allowing a quick short-circuit once it is empty (i.e., once nothing can satisfy the rule). As the set shrinks, it also determines a minimal set of leaves sufficient for rule satisfaction, letting us safely ignore changes to leaves outside it. We thus become more efficient as checking progresses, with the potential to outperform the Attack/Defense optimization. Combining these short-circuit and shrinking-set optimizations powerfully reduces the number of checks required by the base algorithm. Formally, once a leaf in a cut is set to conflict or its attack state (Definition V.6), it will continue to remain in its attack state in the search, regardless of any future merges 2 . Call the collection of leaves that have not entered this preserved attack state a Wall. We then define safety-conforming procedures called Sieges that remove leaves from it: Definition VI.4 (Wall). For a given rule parse tree T , its leaves TL , and a cut C, a wall is a partial map: W : TL → {true, false, unset, conflict} such that any leaves l that are Unset or in their Defense State are contained within the partial mapping. These leaves l have a defined W (l) = M (l) giving their known cut state with respect to C. We say this wall corresponds to cut C. Definition VI.5 (Siege). A single routine cut C can siege the wall W and produce a new wall W ′ by: (1) Removing any leaf mappings in W that record an attack or conflict cut state in C, (2) Updating state of any leaves in W that previously recorded an Unset state to a defense state recorded in C. Let W correspond to cut D. Then we say W ′ corresponds to merged result of C and D. Note that a siege can only preserve or reduce a wall’s total leaf mappings, i.e., walls change only monotonically after construction. Sieges function similarly to merges (Section V-D) but occur between a wall and a single routine cut rather than two cuts of any disjoint single routine composition. Theorem VI.6 (Wall Equivalence). For an arbitrary wall W corresponding to an arbitrary cut C, let L1 be a set of truth values defined by both criteria: (1) All leaves inside W are set to a value defined by the Cut Contextualizer, (2) All leaves 2 Recall the merge operation from Table VI: if an attack state is merged with a matching state, it is preserved; else the merge causes a Conflict, which Cut Contextualizer (Section V-G) presumes is attack.

Fig. 5. Average runtime comparison for routines with different complexity 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’s leaf mappings). So: Theorem VI.7 (Wall Transitivity). Consider a single routine cut C and a safe multi-routine cut M with a 0 component for C’s routine. Let M ’s wall be WM , and assume sieging with C removes no leaves. Then any other safe multi-routine cut M ′ sharing M ’s non-zero location vector components (0 component for C’s routine) is safe after merging with C. (Proof in Appendix)

Theorem VI.8 (Wall-Siege Concurrent Routine Safety Runtime). Using walls and sieges, concurrent routine safety run
LS time is: O(V · LS + |R| · NS ) (Proof in Appendix) LS · |Rmax | This is smaller than Baseline’s runtime from Section V-I1. VII. E VALUATION We implemented Knox in C++ and integrated it with the popular HomeAssistant framework [19]. We answer four research questions: 1) How fast is Knox at checking a routine+safety clause set? 2) How does Knox scale with number of safety clauses? 3) What is Knox’s false positive/negative behavior? 4) How does Knox perform against TapChecker [8]? Due to the scarcity of real smart space benchmarks, we evaluate Knox under a diversity of scenarios, using synthetic, realistic, and trace-based workloads. A. Baseline Comparisons We simulate a medium-sized home with 20 smart devices, 1 hub, and safety clauses touching 3-7 devices. (These scales are typical of today’s homes.) We generate routines and safety rules with varying concurrency, length, and distribution. Figure 5 compares Baseline Knox (Section V-I), Knox + Attack/Defense Optimization (Section VI-A), vs. Knox + Attack/Defense + Wall/Siege (Section VI-B). We show the runtime to check the entire routine+safety clause set for all safety violations, under varying routine workloads: (a) Simple workloads have 3 concurrent routines each with 3 commands, (b) Complex workloads have 7 concurrent routines each with 7 commands. In each, routines pick devices based on either (i) exponential distribution (simulates more overlap among routines), or (ii) uniform distribution (less overlap). All data points use an average of 1000 trials.

Run Type

2×2 Unif

2×2 Expo

3×3 Unif

3×3 Expo

Accuracy

0.989

0.988

0.961

0.963

(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.)

TABLE VIII

50 Routines

Accuracy Rates for Various Routine Sets: Unsafe cut reports from Knox are compared against brute-force checks. False positive rates stay below 4%.

Runtime (seconds)

104

Attack/Defense Wall/Siege

103

500 Routines

LR

BR

LR

BR

TapChecker Knox

.66 s .029 s

.65 s .027 s

69.365 s .238 s

69.372 s .239 s

Speedup

22.76×

24.07×

291.45×

290.26×

102

TABLE IX

Knox and TapChecker [8] Performance and Routine Scalability. Living Room (LR), Bedroom (BR)

101 100 0

100

200

300

Number of Devices

400

500

Fig. 6. Device Scalability: Average runtime vs. number of devices.

Average Runtime (ms)

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 complex routines, Brute Force took too long to measure). Further, (3) our two optimizations—Attack/Defense & Wall/Siege— reduce runtime over Baseline Knox on complex routines, up to 277× and 4717× respectively. B. Scalability Table VIII shows accuracy (Section V-J) with {2,3} concurrent routines × {2,3} commands and a randomly generated safety tree of 5 device states. Accuracy = (1 - FPR), where the false positive rate (FPR) is the ratio of nonexistent unsafe cut reports from Knox to the total number of unsafe cut reports, measured by matching Knox’s output against corresponding brute-force results. We observe (i) high accuracy and (ii) insignificant accuracy drop for complex routines, with no missed violations (false negatives = 0). Figure 6 evaluates scalability with respect to devices. We also scaled the size of the safety tree from 8 to 256 leaf nodes, (correlated with the device count), along with routine sizes from 5×5 to 8×8. Each data point is averaged over 100 trials. Wall/Siege shows a consistent advantage over Attack/Defense with a 2.76×–133.4× speedup when scaling to hundreds of smart devices (Baseline Knox was prohibitively slow to test). C. Home Assistant Room Simulation We use the HomeAssistant integration to generate a smart room containing 7 devices, 5 routines (2-5 commands/routine), and 2 safety rules with a total of 4 device states involving range queries (⋚ comparisons). Figure 7 shows that 0.06 0.04

D. Comparison vs. TapChecker To compare Knox with TapChecker [8] in a fair way, we borrow that paper’s workload of 2011 routines in total. Table IX evaluates scalability with respect to routines. It shows that Knox runtime is 22.76× to 291.45× faster than TapChecker. In terms of accuracy, TapChecker only considers pairwise (2-way) conflicts among routines. To compare fairly against Knox (which considers conflicts from any number of concurrent routines), we extended TapChecker’s original implementation to detect 3-way conflicts. We use 17 routines, and then inject 12 crafted rules that can only be violated by 2way or 3-way concurrent routines. Table X shows that even the augmented TapChecker can have false negative rates (missed violations) up to 12.2%, but Knox has none. Three-way Rules Added TC-triple Knox

Fig. 7. Home Assistant Experiments: Average runtime comparison

for realistic routines in a room simulation.

4

3.44% 0%

8.89% 0%

12.2% 0%

TABLE X

VIII. S UMMARY We have presented the first algorithms that statically check the satisfaction of safety clauses in a smart space containing an arbitrary number of devices running an arbitrary number of concurrent routines, along with an expressive grammar for specifying such clauses. Knox checks safety properties quickly (without brute-force enumeration) and accurately (no missed violations, low false positive rates). Our work opens up new future directions including tackling dynamic versions of this problem, characterizing errors to further lower false positives, and considering additional error types, such as security violations. Acknowledgments: This work was supported in part by grants from NSF (CNS 1908888, CNS 2504595) and the IBM-IL Discovery Accelerator Institute (IIDAI). [1]

Baseline Attack/Defense Wall/Siege Knox Algorithm

3

False Negative (FN) Rates for Varying Numbers of Three-way Safety Rules: Conflicts missed. Knox never misses conflicts.

0.02 0.00

1

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

[2]

[3]

[4] [5] [6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14] [15]

S. B. Ahsan, R. Yang, S. A. Noghabi, and I. Gupta, “Home, SafeHome: Smart home reliability with visibility and atomicity,” in Proc. EuroSys ’21, Online Event, United Kingdom, 2021, pp. 590–605, ISBN: 9781450383349. DOI: 10.1145/3447786.3456261 S. B. Ahsan, R. Yang, S. A. Noghabi, and I. Gupta, “Home, SafeHome: Ensuring a safe and reliable home using the edge,” in HotEdge 19, 2019. Amazon, Amazon Alexa, Jan. 2024. [Online]. Available: https://developer.amazon.com/en-US/alexa Apple, Apple Home, Jan. 2024. [Online]. Available: https://www.apple.com/home-app/ H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, 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- 3030-99524-9 24 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,” in Proc. CHI ’19, 2019, pp. 1–12, ISBN: 9781450359702. DOI: 10.1145/3290605.3300782 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 F. Corno, L. De Russis, and A. Monge Roffarello, “Empowering end users in debugging trigger-action rules,” in Proc. CHI, 2019, pp. 1–13, ISBN: 9781450359702. S. Davidoff, M. K. Lee, C. Yiu, J. Zimmerman, and A. K. Dey, “Principles of smart home control,” in Proc. Ubicomp, 2006, pp. 19–34, ISBN: 9783540396345. F. Durán, 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 / article / pii / S2352220818301135 fabiom91, HomeKit unreliable: Unresponsive accessories, Mar. 2022. [Online]. Available: https : / / discussions.apple.com/thread/253711255 Google, Create and manage routines for Google Home automations, Jan. 2024. [Online]. Available: https : / / support.google.com/googlenest/answer/7029585 Google, Google Home, Jan. 2024. [Online]. Available: https://home.google.com/welcome/ Grand-View-Research, Smart home market, 2026. [Online]. Available: https://www.grandviewresearch.com/ industry-analysis/smart-homes-industry

[16]

[17]

[18]

[19]

[20] [21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29] [30]

[31]

T. Hance, M. Heule, R. Martins, and B. Parno, “Finding invariants of distributed systems: It’s a small (enough) world after all,” in NSDI ’21, Apr. 2021, pp. 115–131, ISBN : 978-1-939133-21-2. 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 W. He, J. Martinez, R. Padhi, L. Zhang, and B. Ur, “When smart devices are stupid: Negative experiences using home smart devices,” in IEEE SPW, 2019, pp. 150–155. DOI: 10.1109/SPW.2019.00036 HomeAssistant, Home Assistant developer docs, Oct. 2024. [Online]. Available: https : / / developers . home assistant.io/ IFTTT, IFTTT, Jan. 2024. [Online]. Available: https : //ifttt.com/ IoT-Analytics, IoT Startup Landscape 2024: 7 notable insights, Jul. 2024. [Online]. Available: https : / / iot analytics.com/iot-startup-landscape/ IoT-Analytics, State of IoT 2025: Number of connected IoT devices growing 14% to 21.1 billion globally, Oct. 2025. [Online]. Available: https : / / iot - analytics . com / number-connected-iot-devices/ 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,” in Proc. IPSN ’15, 2015, pp. 298–309, ISBN: 9781450334754. DOI: 10 . 1145 / 2737095.2737115 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 MEGATOMI, HomeKit automations are broken in iOS 16, Sep. 2022. [Online]. Available: https://discussions. apple.com/thread/254199872 Mett03, HomeKit automation not working after iOS 17, Sep. 2023. [Online]. Available: https : / / discussions . apple.com/thread/255155940 J. L. Newcomb, S. Chandra, J.-B. Jeannin, C. Schlesinger, and M. Sridharan, “IOTA: A calculus for internet of things automation,” in Proc. SIGPLAN Onward! ’17, 2017, pp. 119–133, ISBN: 9781450355308. DOI : 10.1145/3133850.3133860 Samsung, Samsung service terms and conditions SmartThings services supplement, Feb. 2024. [Online]. Available: https : / / v3 . account . samsung . com / policies / specials/smartthings.html Samsung, Samsung SmartThings, Jan. 2024. [Online]. Available: https://www.smartthings.com/ tomg15, HomeKit automations not working (again), Nov. 2022. [Online]. Available: https : / / discussions . apple.com/thread/254390066 Q. Zhou and F. Ye, “APEX: Automatic precondition execution with isolation and atomicity in internet-of-

things,” in Proc. IoTDI ’19, 2019, pp. 25–36, ISBN: 9781450362832. DOI: 10.1145/3302505.3310066

A PPENDIX Theorem V.1 (NP-Hardness: Single). The Single Routine Safety problem is NP-hard. Proof. We prove for just one safety rule. Let SingleRoutineSafety be an algorithm to solve the Single Routine Safety problem. Algorithm 6 shows the reduction from SAT: Algorithm 6: SAT Reduction to SingleRoutineSafety Input: Boolean expression B Output: “YES” or “NO” 1 Define boolean a: a = Device D in state Ds ; 2 Construct Safety Rule S from expression B and a: S = a ∧ ¬(B); 3 Construct routine R: R = {Set D to Ds }; 4 Output “YES” iff SingleRoutineSafety(R, S) outputs “NO”; 5 Otherwise output “NO”;

SingleRoutineSafety(R, S) returns “YES” iff there is no setting that makes ¬(B) false, i.e., iff B is not satisfiable. Due to this reduction, our problem is NP-hard. ■ Theorem V.2 (NP-Hardness: Safe Initial State). The Single Routine Safety problem, when limited to safe initial states, is NP-hard. Proof. We again limit ourselves to one safety rule. Let SingleRoutineSafety be an algorithm to solve the Single Routine Safety problem, limited to safe initial states. Algorithm 7 shows the reduction from SAT: Algorithm 7: SAT Reduction to SingleRoutineSafety with safe initial states Input: Boolean expression B Output: “YES” or “NO” 1 Define boolean a: a = Device D in state Ds ; 2 Construct Safety Rule S from expression B and a: S = a ∨ ¬(B); 3 Construct routine R: R = {Set Device D to state Ds′ , Ds ̸= Ds′ }; 4 Output “YES” iff SingleRoutineSafety(R, S) outputs “NO”; 5 Otherwise output “NO”; If B is not satisfiable, then S is trivially safe. However, if B is satisfiable, we can choose such a setting, with D in state Ds (a = True) as our safe starting state. But entering state Ds′ (violating a) will violate safety! Therefore, SingleRoutineSafety(R, S) returns “YES” iff B is not satisfiable, and the problem is NP-hard. ■

that n’s setting can only contribute to one truth value for its parent, which then contributes to satisfaction or violation. We have five possibilities: • n’s parent is a NOT node: The claim is trivially satisfied. • n’s parent is an OR node: If ST (n) = false, then setting ST (n) = true trivially satisfies the parent, no matter the other sibling values of n. Likewise, if all other siblings are false, then setting ST (n) = false violates the parent, and there exists no setting of siblings such that setting ST (n) = false changes parent’s value from false to true. • n’s parent is an AND node: If all siblings are set to true, then setting ST (n) to true satisfies the parent, and there exists no setting of other siblings such that setting ST (n) = true changes the parent’s value from true to false. Likewise, if ST (n) = true, then setting ST (n) = false trivially violates the parent, no matter n’s other sibling values. • n’s parent is AT MOST k: If k siblings of n are set to true, then setting ST (n) to true violates the parent. There exists no setting of n’s siblings such that setting ST (n) = true changes the parent’s value from false to true. Likewise, if k siblings and n are true, then setting ST (n) to false satisfies the parent. There is no setting of n’s siblings such that setting n to false changes the parent’s value from true to false. • n’s parent is AT LEAST k: If k − 1 siblings and n are set to true, then setting ST (n) to false violates the parent. There is no setting to n’s siblings such that setting ST (n) to false changes the parent’s value from false to true. Likewise, if k − 1 siblings are set to true, then setting n to true satisfies the parent. There is no setting to n’s siblings such that setting n to true changes the parent’s value from true to false. Hence, each node’s setting can contribute only a single truth value to its parent, and by extension to exactly one of rule satisfaction or violation. Additionally, this result shows that a setting contributing to satisfaction is the opposite of the corresponding setting for violation. By induction, these properties hold for the entire tree. ■

Theorem V.13 (One-To-One Contribution). Given a tree T for a rule, and a node n ∈ ST , a specific truth value of node n can contribute only to exactly one of either rule satisfaction or rule violation.

Theorem V.16 (Correctness of Routine Safety). Assume we have two safe multi-routine cuts C1 and C2, such that C1 precedes C2. If all cuts that succeed C1 and precede C2 are safe, then there exists no unsafe interleaving of the commands between C1 and C2’s location vectors.

Proof. By induction. Base Case: n is the root, and trivially satisfies the theorem by Definition V.11. Inductive Case: Assume n’s parent’s setting can contribute to only rule satisfaction or rule violation. It is sufficient to show

Proof. We define C1’s location vector as < m1 , ..., m|R| > and C2’s location vector as < i1 , ..., i|R| >, and proceed with a proof by contradiction. Assume a safety rule S is violated at some arbitrary location vector t =< j1 , ..., j|R| >, with mk ≤ jk ≤ ik for all 1 ≤

k ≤ |R|. Let C ′ be the result of merging cuts taken from each routine Rk at location jk , assumed to be safe. Let the ordered leaf states for C ′ and t be LC ′ and Lt , respectively. Let ∆s be the set of leaves in S’s tree, such that for every leaf l ∈ ∆s, l’s state in Lt and l’s state in LC ′ differ. Note ∆s ̸= ∅ iff LC ′ and Lt disagree on at least one leaf state. For an arbitrary l ∈ ∆s, consider the cause of the disagreement. By definition, cuts arising from multiple routines preserve the exact state recorded from constituent routines in a state list, with two notable exceptions. A merge can consist of routines that 1. never set that device state, in which case the cut records unset, or 2. disagree on a device state, in which case the cut records conflict. In both cases, Cut Contextualizer assumes an attack state for the leaf in question. Lt , on the other hand, is exactly a record of leaf states taken at time t. So every l must have the property of being an attack in LC ′ and a defense in Lt . Next we construct Lt from LC ′ . From ∆s’s definition, this transformation is merely changing the state of every l ∈ ∆s. If every l was an attack in LC ′ , then it must be a defense in Lt . Since LC ′ satisfies S by assumption, Lt must also satisfy S. Thus, such a location vector t (violating S) cannot exist. ■ Theorem V.18 (Single-Routine: Avoidance of False Positives). For a single routine, and a rule parse tree T , if T has at most one leaf for each device in the smart space, then Knox avoids false positives. Proof. If no false positives exist, then an unsafe single routine cut C exists if and only if a point of execution exists where the routine violates safety for some initial state. Theorem V.16’s result implies the contrapositive: if there is an unsafe interleaving, there must be an unsafe cut. Without loss of generality we only consider devices present in T , and consider C as a subroutine executing C’s location number of commands. Note that when considering a single routine, a cut state of conflict is not possible; only leaves that are unset are not explicitly known. Further, since there is at most one leaf for each device in T , there are no contradictory values (Section V-F). We construct initial home state h: for each device in T , we set it to its attack state. Since unset leaves are by definition not modified by the subroutine, these leaves must still be in their attack state. Thus, the home state after executing the subroutine is exactly the state that the Cut Contextualizer constructs. Since stateful trees are direct evaluations of safety, if there is an unsafe cut, there is an unsafe interleaving. ■ Theorem V.20 (Multi-Routine: Avoidance of False Positives). An unsafe multi-routine cut C exists if and only if an unsafe interleaving exists for some initial state, provided either conditions (A1 AND A2) are true, or B is true, i.e.: • (A1) The rule parse tree T has at most one leaf for each device in the smart space, AND • (A2) For all leaves in C set to conflict, all routines execute attack commands after defense commands

OR • (B) At most one leaf in C is set to conflict. Proof. We follow the thinking of Theorem V.18 for multiroutine cuts. For the first condition pair, since there is at most one leaf per device, every command that acts on that device would set all relevant leaves to their attack or defense states, so no commands are ambiguous. For leaves in conflict, when choosing an interleaving, order their respective commands so that all routines execute their defense commands first, and then all routines execute their attack commands. We can do this since all routines execute attacks after defenses for conflict leaves (by assumption). For condition (B), assuming a single conflict leaf l, there must be at least one routine that set it to its attack state and at least one other that set it to its defense state. Without loss of generality, let routine R1 be one of the former and routine R2 be one of the latter. An unsafe interleaving will run all routines other than R1 and R2 in any arbitrary order. Then, when running R1 and R2 afterwards, execute R2 ’s defense command first, and R1 ’s attack command second. In both cases, since all other devices are explicitly known by C’s location vector, they do not need to be ordered. All conflict leaves in the selected interleaving are by construction in their attack state. Thus, the home state after executing this interleaving has exactly the state that the Cut Contextualizer constructs. Since stateful trees are direct evaluations of safety, there is an unsafe cut if and only if there is an unsafe interleaving. ■ Theorem VI.2. If the multi-routine cut located before any routine commands execute is safe, then any cut located immediately after a defense command is irrelevant and can be skipped for safety checking. Proof. To use Theorem VI.1 we need the immediate predecessor to be safe. There are two cases— either it is the cut before all routine commands (assumed safe), or it is preceded by an attack or ambiguous command in which case it is relevant and checked for safety. ■ Theorem VI.3 (Attack/Defense Runtime). With P Kad = Ri ∈R |R2i | , runtime of checking concurrent routine safety after applying the Attack/Defense optimization is  |R| | O(NS + Kad · LS + Kad · NS + |Rmax · (LS + NS )) 2 (Notations are in Table VII).

Proof. Command Classification requires every unique command across all routines to be categorized against a rule. The classification is remade for every rule. Based on Section V-I1’s variables, if the worst case total unique command count is I = ΣRi ∈R |Ri | and total leaves across all safety rules is LS , then Command Classification takes O(I · LS ) time. The total number of multi-routine cuts to be checked for safety depends on the product of number of single routine cuts from each routine, and total routine count. Theorem VI.1

can reduce the first term. A worst-case scenario is a rule set S and a routine set R where every command in the routine set is classified as ambiguous for every safety rule in S. Each multi-routine cut in Section V-I must be checked for safety, requiring O(NS + K · LS + |Rmax ||R| · (LS + NS ) + I · LS ). This can be reduced if S and R are restricted such that no commands in R are classified as ambiguous across all rules in S. Routines should start with an attack command and then alternate between defenses and attacks — the only irrelevant cuts are those between a defense command and the following attack command (or after the last command if a defense). Thus total locations needed for single routine checking, K, can be reduced to a Kad . Since we halve the number ofPcuts to be checked and ignore the starting |Ri | cut, Kad = Ri ∈R 2 . The same reasoning means that the number of location vectors as multi-routine cuts that are needed to ensure concurrent routine safety are also reduced:  |R| |Rmax | . Therefore, the adjusted worst case runtime is 2  |R| | O(NS + Kad · LS + Kad · NS + |Rmax · (LS + NS )). ■ 2

inside the wall (by definition) the same state in L1 & L2 . Hence ∀ leaves: L1 = L2 . ■

Theorem VI.6 (Wall Equivalence). For an arbitrary wall W corresponding to an arbitrary cut C, let L1 be a set of truth values defined by both criteria: (1) All leaves inside W are set to a value defined by the Cut Contextualizer, (2) All leaves 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. Safety evaluation is needed only when a leaf is removed from the wall. In the worst case, each non-zero component of a multi-routine cut location vector removes exactly 1 leaf when comparing walls (else we were still safe). Once a wall is empty, further cuts are trivially unsafe. Constructing all multi-routine cuts takes O(V · LS ) time (Section V-I1), where Q V = Ri ∈R (|Ri | + 1). The complexity comes from number of location vectors with exactly LS non-zero components:
|R| · |R |LS , where Rmax has the maximum commands max LS of any routine. This gives a runtime upper bound:
LS O(V · LS + |R| · NS ) LS · |Rmax |

Proof. Consider leaves outside the wall. By definition, these must either be conflict cut state or attack state, both of which our Cut Contextualizer sets to attack state. We assign leaves Theorem VI.8 (Wall-Siege Concurrent Routine Safety Runtime). Using walls and sieges, concurrent routine safety run
time is: O(V · LS + |R| · |R |LS · NS ) max LS

Theorem VI.7 (Wall Transitivity). Consider a single routine cut C and a safe multi-routine cut M with a 0 component for C’s routine. Let M ’s wall be WM , and assume sieging with C removes no leaves. Then any other safe multi-routine cut M ′ sharing M ’s non-zero location vector components (0 component for C’s routine) is safe after merging with C. Proof. Since Table VI’s operations are commutative, let M ′ siege WM . Then, WM ′ ⊆ WM . M ′ is safe by assumption, sieging WM with C removes no leaves, and WM ′ ⊆ WM , so sieging WM ′ with C also removes no leaves. By Theorem VI.6, the leaves both inside and outside the wall take the states that the Cut Contextualizer assumes. Therefore, if a safe multi routine cut’s wall remains unchanged after merging a new single routine cut, the result is still safe. Since M and M ′ are each safe, merging C is also safe as the wall remains unchanged. ■

■