Delay Wreaks Havoc on Your Smart Home: Delay-based Automation Interference Attacks

I. INTRODUCTION

Rapid development of Internet of Things (IoT) has led to flourishing smart environments, (e.g., smart homes, offices, and laboratories). IoT platforms, such as Apple HomeKit [1], Samsung SmartThings [2], and Amazon Alexa [3], enable configurations of automation rules for interactions between IoT devices in a home, also known as home automation. For example, users can create automations on SmartThings, or routines on Alexa, to have their devices automatically react to sensor measurements, device status, time, etc. 1 When multiple rules interplay in a physical environment, they may interfere with each other and cause unexpected automation. The cross-rule interference (CRI) problem has been intensively studied (on individual platforms) [4], [5], [6], [7], [8], [9], [10], [11], [12], [13]. However, existing work that studies the CRI problem makes the following two assumptions: (1) They assume that all rules run on the same platform [6], [7], [9], [10], [5], [12], [13], [8] (or rules on different platforms do not interact with one another and can be analyzed separately [11]); (2) They also assume that all IoT 1 We refer to automations and routines as automation rules or rules. messages are transmitted with identical delays. For example, the first systematic categorization of CRI [4], [5] assumes both.

The assumptions, however, do not necessarily hold true in real-world systems. Due to the fragmented IoT ecosystem [14], [15], different platforms are compatible with different subsets of IoT devices. When users cannot find a single platform to work with all their devices, they need to use multiple platforms. Furthermore, different devices use heterogeneous communication technologies and transmit messages through different paths. For example, a ZigBee device talks with a platform A's server via an IoT hub, while a WiFi-based device talks with its vendor's cloud B, which then delegates access to the device to the platform A. The communication paths are different and thus have different transmission delays. Worse, such delays can be manipulated by attackers without relying on any implementation vulnerabilities (Section II-C).

We thus consider a more general and realistic smart home system, where (1) users may use more than one platform to support their devices and install automation, and (2) IoT devices can transmit messages via more than one communication path. We classify smart home systems into three categories: single-platform single-path (SPSP) systems, single-platform multi-path (SPMP) systems, and multi-platform (MP) systems, which certainly contain multiple paths (Section III describes the three categories in details). By incorporating message transmission delays as a factor, we study two issues which do not exist in SPSP (where the two assumptions aforementioned hold): disorder and inconsistency. Disorder occurs when two IoT events (or commands) arrive at platforms (or devices) in an order different from their actual occurrence order, while inconsistency arises when two platforms have inconsistent observations on the state of the same device.

We then re-examine cross-rule interference (CRI) in SPMP and MP systems, and reveal a new family of attacks that are overlooked by previous work, referred to as Delay-based Automation Interference (DAI) attacks, which exploit the interaction of automation rules in SPMP or MP systems. Fig. 1 illustrates an example. If the button-pressed event (which sets the home mode on both platforms to ªAwayº) sent to Platform B is delayed by an attacker, the automation rule on Platform A succeeds in closing garage door when the homeowner's car leaves, but the rule on Platform B fails to lock the front door. We utilize two attack primitives [16], selective event delaying and selective command delaying (which leverage TCP hijacking attacks to significantly delay IoT events and commands without requiring session keys or triggering any alarms), as a building block to realize the DAI attacks. In short, an attacker exacerbates the inconsistency and disorder issues to launch DAI attacks, which exploit new CRI patterns and cannot be detected by existing work on CRI [6], [7], [8], [9], [10], [5], [11], [12], [13].

To demonstrate and evaluate the new attacks, we set up two real-world testbeds in two apartments. In the testbeds, we examine a variety of IoT devices, six cloud-based platforms and two local platforms. We validate all of the new attacks in the testbeds and verify that the attacks put the devices into insecure, unsafe or unexpected states. The one-week data from both testbeds also demonstrate that the attackers have adequate opportunities to launch the attacks. Finally, we discuss countermeasures. Our contributions are as follows:

• Given the fragmented IoT ecosystem, we present a much more general and realistic smart home model, where multiple IoT devices associated with multiple IoT platforms interact in the same physical space. Under this model, we study the disorder and inconsistency issues and leverage delay-attack primitives to exacerbate them. • Compared to existing work on CRI [4], [5], we are the first to incorporate the delay factor into analyzing CRI problems.

We are thus able to reveal new CRI patterns and build Delaybased Automation Interference attacks that are overlooked by existing work. These attacks do not rely on any leaked tokens or implementation vulnerabilities. Unlike jamming or discarding packets, the attacks do not trigger alarms at any layers of the IoT protocol stack. • We evaluate the proposed attacks in two real-world testbeds, where commercial off-the-shelf (COTS) IoT devices and multiple popular platforms are used. It is demonstrated that the attacks can cause various problematic home automations and put the IoT devices and home in hazardous states.

II. BACKGROUND AND ATTACK MODEL A. Smart Home Systems

In modern smart homes, various components (e.g., IoT devices, IoT hubs, home router, and IoT platforms) interact in the same physical space. We show the architecture of a modern smart home ecosystem in Fig. 2.

Devices and Hubs: IoT devices consist of sensors and actuators. A sensor (e.g., temperature sensor) simply reports measurements of a physical property, while an actuator (e.g., smart lock) can receive and execute commands (e.g., unlock/lock) to change its status and report that after executing a command. The sensor measurements and actuator statuses are sent to an IoT platform via events. The current sensor measurement or actuator status is called the device's state. A device's state at a platform is updated by the device's latest event.

IoT devices employ a variety of techniques (e.g., WiFi, Zig-Bee, Z-Wave, Bluetooth) to send events or receive commands. 2Devices that use WiFi (e.g., LIFX bulbs, Amazon Echo speakers) can connect to the home router directly 1 ; those that use non-IP protocols (e.g., ZigBee, Z-Wave, Bluetooth, etc.) usually require a hub. The hub converts non-IP payloads from IoT devices 2 to IP-based payloads, which can be sent to the home router 3 . The home router then forwards the IP-based payloads to cloud servers 4 or to other devices in the local area network (LAN) 5 for further processing. A local platform (e.g., HomeKit) can connect non-IP devices directly ( 6 ). Multiple IoT hubs may be deployed in a home to accommodate their supported devices.

Platforms: Cloud-based IoT platforms may be classified into three types: endpoint, service, and hybrid. An endpoint platform is a messaging cloud that mediates communication between IoT devices and service platforms. It may be maintained by a device manufacturer or a third-party service provider (e.g., AWS IoT [17]). A service platform such as IFTTT (If This Then That) is a cloud that runs automation rules and usually obtains access to devices from endpoint platforms, via a cloud-to-cloud integration 7 . A hybrid platform is a combination of an endpoint and a service platform. Many popular smart home platforms, such as Amazon Alexa and SmartThings, belong to this category. In contrast to the aforementioned cloud-based platforms, a local platform (e.g., HomeKit, openHAB) is usually hosted on a local device (e.g., PC, laptop, HomePod speaker) in the home area network, and can connect with IoT devices directly, via non-IP protocols (e.g., ZigBee, Z-Wave, Bluetooth) 6 or via LAN 1 → 5 . A local platform can also access devices that have been connected to an IoT hub ( 2 → 3 → 5 ) or an endpoint/hybrid platform ( 1 → 4 → 9 → 5 or 1 → 4 → 7 → 8 → 5 ), by using the APIs provided by the hub (e.g., Hue bridge) or the endpoint/hybrid platform (e.g., LIFX cloud), respectively. For the sake of brevity, in this paper, we collectively use the term platforms to denote all service, hybrid, and local platforms that can run automation rules.

Automation: An automation rule is a reactive app that follows a trigger-condition-action paradigm. A rule's trigger specifies a constraint that a certain type of event (termed as trigger event) must satisfy to activate the rule. Before an action in a rule is taken, its condition is checked to verify whether states (e.g., devices states, time) have satisfied the predefined constraints. Different platforms may have distinct supports for defining rule conditions. For instance, SmartThings allows using both device states and time to define rule conditions, Philips Hue only allows the usage of time in conditions, and Amazon Alexa only supports trigger-action rules.

C. Selective Event/Command Delaying

In smart home systems, most communication paths (see Fig. 2) between an IoT device/hub and a platform go through a home router. 3 On IP/TCP links, events and commands are typically transmitted using the SSL/TLS protocol, which runs on top of the transport layer. Each pair of an IoT device/hub and a cloud establishes a unique TLS session. IoT events and commands are conveyed in a specific type of TLS record, i.e., Application record, whose type field in header is ª0x17º.

Although TLS provides the confidentiality and orderpreserving features, neither TLS nor the upper applicationlayer protocols used by smart home systems, such as HTTP and MQTT, have a strict liveness checking on messages. IoT devices and clouds usually exchange TLS-protected heartbeat (a.k.a., keep-alive) messages periodically. If an IoT device/cloud cannot receive a heartbeart request/reply or an event/command ack from the other side within a pre-defined time period (usually tens of seconds; see Section V-B), i.e., a timeout occurs, it will actively disconnect the TCP connection and try to reconnect. If an attacker succeeds in performing a TCP hijacking attack (see Section II-D) between an IoT device/hub and a platform, he can establish a TCP connection with each side, becoming a relay node in the middle. Although the MITM attacker cannot decrypt TLS-protected messages, he can delay forwarding the messages. Delaying messages cannot be detected by the IoT protocol stack as long as it does not trigger a timeout. An attacker can recognize IoT events and commands from the encrypted packets through side-channel analysis (Section II-B) and selectively delay a specific event or command, which is referred to as two attack primitives: selective event delaying and selective command delaying. Our prior work [16] discussed the two attack primitives in detail. In this paper, we use the two primitives as a building block.

D. Attack Model

Who Can Launch the Attacks? We are concerned with an attacker who can eavesdrop and delay the encrypted traffic between IoT devices/hubs and the IoT cloud/local platforms. For example, he can compromise the WiFi router in the victim home, or perform ARP spoofing attacks [33], [34] from a local IoT device (e.g., compromised by Mirai attacks [35], [36]). When the attacker and the victim share a WiFi (e.g., at a company, hospital, or facility campus), the attacker can launch sniffing and ARP spoofing from his own device conveniently. If an attacker has compromised an ISP router, he can launch attacks at scale against many homes that use cloudbased platforms. Through the attack, the attacker obtains two capabilities: (1) passively analyzing traffic; and (2) actively delaying events/commands. Passive Observation. For this purpose, sniffing attacks are sufficient (i.e., TCP hijacking is not needed). Specifically, the attacker has access to headers of the data link, network and transport layers (such as device MAC addresses, IP addresses and ports), and the type and length of TLS records. The attacker utilizes the techniques discussed in Section II-B to obtain knowledge of the victim home and recognize events/commands from the traffic. Active Delaying. The attacker selectively delays events/commands transmitted over a hijacked TCP session. To evade detection, the attacker does not discard any events/commands or delay them for an excessive period. The delay range (without being detected) depends on the type of IoT devices and platforms (more details are given in Table IV).

III. EVENT/COMMAND DISORDER AND INCONSISTENCY

In a smart home where all IoT devices use the same TCP/IP communication path to exchange events and commands with a single platform, as shown in Fig. 3, two properties hold: 3 Fig. 3: Single-platform single-path device connection. Fig. 4: Single-platform multi-path device connection.

• Same Order. All events arrive at the IoT platform in the same order as they arrived at the hub. This holds for all events that are transmitted on the same TLS session (i.e., the hub-platform path), as each TLS record includes a Message Authentication Code that checks data integrity and the sequence number [37]. Likewise, a command sent earlier by the platform arrives at the hub earlier.

• Consistency. The executions of all automation rules are based on a consistent observation about the smart home, because the same database maintained by the platform is queried for data (e.g., device states, home mode, etc.).

Although existing research on CRI [38], [39], [6], [7], [8], [26], [9], [40], [5] considers or implicitly assumes the singleplatform single-path (SPSP) deployment model, it does not reflect the reality. Over time, users may purchase a variety of IoT devices and connect them with multiple platforms. Therefore, the following two deployment models are common in reality: the single-platform multi-path (SPMP) model and the multi-platform (MP) model. According to our online survey (see Appendix A for details) including 85 realistic smart homes, SPSP, SPMP and MP deployments account for 17.6%, 20.0% and 62.4%, respectively.

B. Multi-Platform: Disorder and Inconsistency

In multi-platform systems, there exist multiple TCP/IP paths between IoT devices and platforms. Therefore, the disorder issue certainly exists. Plus, when an IoT device is connected to two or more platforms, the platforms may have different observations on the same device's state. This is because a new event from the device may have different delays when transmitted to the platforms (via different paths). As shown in Fig. 5, a WeMo smart plug communicates with the WeMo cloud (a.k.a., an endpoint cloud) through the Internet, and talks in the local area network with a HomePod that hosts HomeKit or with a SmartThings hub which forwards communication to the SmartThings cloud. Thus, the WeMo smart plug uses three different paths to connect with the three platforms. The transmission delays could create a time window, during which platforms have inconsistent observations on the state of the plug (i.e., ON/OFF). We refer to this issue as inconsistency.

In non-adversarial scenarios where the network delays are usually small, e.g., less than one second, the disorder and inconsistency issues are not severe. However, in the presence of an attacker who intentionally delays events/commands, the disorder and inconsistency issues may be manipulated by the attacker to cause serious security and safety threats to a smart home (e.g., leaving the front door unlocked when the owners are not home), and this is discussed in Section IV.

Bedroom 15

When motion is detected, if user is at home, turn off camera. 16 When motion is detected, if user is away, ring alarm and send live video to security company. 17

When motion is detected, turn on the ceiling lamp. 18

When motion is detected, if luminance is below 20 lux, turn on the floor lamp.

Fig. 6: A smart home illustrating part of the deployed IoT devices and automation rules.

, where all devices D 1 ∪ D 2 are connected to an oracle platform L * , both rules R1 and R2 run on L * , and all its communication paths incur identical delays. That is, Sys * runs the same rules and devices in the same environment as Sys but suffers no DAI attacks.

Observation equivalence is a property that two or more concurrent systems are indistinguishable regarding their observable implications (e.g., the states of sensors and actuators). Therefore, if the real system Sys (with DAI attacks) and specification system Sys * (without DAI attacks) are observationally equivalent while they evolve, i.e., the automation results (resultant device states) are always the same no matter how rules are triggered the same way in both systems, we say that the two automation rules R1 and R2 in the deployment Sys are CRI-resistant to DAI attacks. With this notion, we not only can verify if rules are CRI-resistant after formalizing a given smart home deployment, but also find all possible types of DAI attacks by traversing different attack strategies (i.e., which communication paths to delay). Due to the page limit, we defer full details of the formal modeling, and the methodology for observation equivalence analysis and DAI attack categorization, to Appendices B and C, respectively.

C. DAI Attacks

We summarize seven types of DAI attacks in Table I. For each type, Table I lists the attack name, the section interpreting Fig. 7: Condition overlapping attack. The conditions of Rules i and j are satisfied when the device state is 0 and 1, respectively. Here, 0 and 1 broadly denote the values of a binary attribute, e.g., inactive and active of a motion sensor. it, the rule pattern describing the attack, the message(s) that should be delayed, the issue exploited and the consequence.

1) Condition Overlapping Attack: Existing works [6], [7], [9], [10], [5], [11], [12], [13] assume that rules do not run simultaneously if their conditions are exclusive, (e.g., ªif motion sensor is activeº vs. ªif motion sensor is inactiveº). As shown in Fig. 7, suppose the conditions of Rules i and j check the state of a device, and this device has two possible states 0 and 1. When there are no attacks, the condition-satisfaction period during which Rule i's condition (e.g., ªif the state is 0º) is satisfied has no overlap with that of Rule j, (e.g., ªif the state is 1º). However, if Rules i and j run on two different platforms A and B, respectively, by delaying the arrival of event 1 on platform A and/or the arrival of event 0 on platform B (see Fig. 7), the condition-satisfaction periods of the two rules will have overlaps. As a result, if both rules are triggered during the overlapping period, they will be executed during the same period, violating the expectation that they are mutually exclusive. We collectively define condition-overlapping attacks (COA) as attacks that exploit inconsistency issues to cause rules with exclusive conditions to run simultaneously. Under this attack, rules that are considered interference-free by prior 5 TABLE I: Summary of DAI attacks. The DAI attacks are derived from a systematic categorization show in Appendix C. The Rule Pattern column shows the pattern of victim rules targeted by each DAI attack. Ri = (Ti, Ci, Ai), i = 1, 2 denotes two victim rules, where Ti, Ci, Ai are the trigger, condition, and action, respectively. ⊥ denotes ªmutually exclusiveº; ∧ denotes ªoverlapsº; ¬ denotes that ªmutually contradictoryº; ⇒ and ⇏ denotes ªenablesº and ªdisablesº, respectively; <≈ denotes ªis close but precedent toº; ⊣ denotes ªrequiresº; ⊎ denotes ªguarded byº.

Attack

Section # Rule Pattern What to Delay? 1 Issue Exploited Consequence

is achieved by delaying the event, checked by T (•) or C (•) , to the platform where R (•) runs. For instance, C1 → R2 denotes that an event (e.g., motion active) which makes the condition C1 (e.g., ªif the motion is detectedº) true should be delayed when it is transmitted to the platform hosting the rule R2. Delaying an action A (•) is realized by delaying the command issued by A (•) when the command is sent to the destined device.

work become problematic. Below, we present three sub-types of the attack and use concrete examples to demonstrate how they lead to incorrect automation results. Action Conflict. Through the condition overlapping attack, an attacker can cause an action conflict. Consider Rules 15 and 16 (in Fig. 6) which protect user's privacy and detect burglary respectively, based on the user's presence when motion is detected in the bedroom. As shown in Fig. 8, if they are installed on different platforms A and B, the attacker can delay the user-away event from a presence sensor to platform A. Thus, when triggered by the motion-active event, Rules 15 and 16 have different observations on the user's presence: ªuser is at homeº and ªuser is awayº, from the databases of platforms A and B, respectively, and perform conflicting actions. Consequently, Rule 15 turns off the camera, preventing Rule 16 from recording live videos. Infinite Loop. Rules 13 and 14 are configured to control lights in the living room, based on luminance and user motion.

According to the recent research [6], [5], [9], the two rules have no interference, since their conditions, ªif motion is activeº and ªif motion is inactiveº, are mutually exclusive. Specifically, when Rule 13 turns on the lights and brightens the room (which means the motion is active), Rule 14 is activated but its condition is not satisfied; thus, Rules 13 and 14 cannot trigger each other according to existing work. However, when the rules run on two different platforms, the condition overlapping attack can delay the most recent motionactive event sent to the platform hosting Rule 14. As a result, when Rule 13 turns on the lights, Rule 14 will be triggered to turn them off, which triggers Rule 13 once again; during the period the motion-active event is delayed, an infinite loop will make the lights continuously flash on and off. Chained Execution. Chained execution of rules [5] (also referred to as interaction chain [40], rule chains [44], or feature chaining [45]) is a well-studied CRI pattern, which occurs when the action of one rule activates the trigger of another rule. Let's consider Rule 9 in Figure 6, which turns on an Internet-connected space heater (such as [46]) during cooking time (12pm and 7pm). For energy-saving and safety reasons, Rule 10 turns off the smart plug when appliances connected to it increase power consumption over a threshold if nobody is in the kitchen. Rule 9 uses a condition, ªif motion is activeº, to avoid chaining with Rule 10, whose condition is ªif motion is inactiveº. Without attacks, the coexistence of Rules 9 and 10 will not cause chained execution. However, if Rules 9 and 10 run on different platforms, A and B, respectively, the attacker can delay a motion-active event being sent to platform B, causing Rule 10's condition to be kept true. This way, when Rule 9 is activated at cooking time, an unexpected chained execution of Rule 10 occurs to turn off the smart plug.

2) Trigger-Condition Overlapping Attack: Some automation rules avoid chained execution by making the trigger of one rule and the condition of another mutually exclusive. However, the exclusiveness is broken by delaying a trigger event. Consider Rules 6 and 11 in Fig. 6. Rule 6 unlocks the front door when the user arrives home (detected by a presence sensor); Rule 11 automatically sounds an alarm and call the police when it detects a possible break-in: the front door is unlocked while the user is not present. Rules 6 and 11 play their own roles and do not chain when they have consistent observations on the presence sensor. Suppose Rules 6 and 11 run on two platforms, A and B, respectively. If a user-present event sent to platform B is delayed by the attacker, Rule 11 uses outdated information (i.e., the user is not present) to evaluate its condition when it is triggered by the door-unlocked event (caused by Rule 6's action). As a result, it causes a false burglar alarm.

3) Condition Diverging Attack:

In contrast to the condition overlapping attack, which causes rules with exclusive conditions to interact, the condition diverging attack prevents rules with overlapping rules from interacting. Although chained execution is recognized as a CRI pattern, it is sometimes an important feature for grouping rules for specific goals if it is utilized properly. For example, Rules 4 and 5 use this feature to 6 290 close the garage door and lock the doors in a row, which do not cause any problem if they run on the same platform. However, the condition diverging attack can disable the desired chained execution. Suppose Rules 4 and 5 run on different platforms, A and B, respectively. The attack can desynchronize the mode on platforms A and B by delaying the ªawayº message sent to B. Thus, when the user drives away, Rule 4 is executed to close the garage door, while Rule 5's condition is not satisfied, failing to lock the front and hall doors.

4) Action Disordering Attack: This attack changes the arrival order of commands issued by different rules. Consider Rules 8 and 12 in Fig. 6: Normally, a user first enters her home through the door and then her motion in the living room is detected; as a result, Rule 8 is first triggered by the door-open event to turn on smart plugs, and then Rule 12 is triggered, which turns on the humidifier and TV. This order is presumably ensured by the order of physical activities. However, if the command due to Rule 8 is delayed by attacks, Rule 12 will fail to turn on the humidifier and TV.

More generally, an action disordering attack can be achieved by delaying the trigger event, command, or both. Assume that Rule i is supposed to take its action before Rule j (assume neither rule involves the use of timers). As shown in Fig. 9(a), when Rule i's trigger event is delayed for a sufficient period, Rule i is executed after Rule j. Fig. 9(b) shows another attack strategy: an attacker can delay the command of Rule i and make it arrive at the destined device later than the command of Rule j, even though Rule i executes before Rule j. Alternatively, the attacker can delay both the trigger event and command of Rule i to increase the total delay. 5) Condition Disabling Attack: If a rule's action changes a device's state to a value that dissatisfies the condition of another rule, it is called Condition Block [9] CRI. Prior work [5] empirically demonstrates that, if the two rules subscribe to the same trigger event and run on the same platform, Condition Block is unlikely to happen. However, as shown in Fig. 10, when the two rules are on different platforms, a condition disabling attack becomes possible, because the attacker can delay the trigger event sent to the platform hosting Rule i, such that Rule j changes the device state (green), which disables the condition of Rule i.

Let's consider Rules 17 and 18. When a user enters the bedroom, Rule 17 on platform A turns on the ceiling lamp; if the room is too dark, Rule 18 turns on the floor lamp as well. If Rule 18 is also installed on platform A, the two rules ensure that when the user enters the bedroom, either (1) only the ceiling lamp is turned on if initially there is at least 20 lux luminance, or (2) both lamps are turned on if luminance is below 20 lux. However, as platform A (such as Amazon Alexa) does not support defining rule conditions, Rule 18 is installed on another platform B. The automation now becomes vulnerable to the condition disabling attack. An attacker can delay the motion-active event to platform B. Thus, when motion is detected, Rule 17 first turns on the ceiling lamp, increasing the measurement of the luminance sensor to a higher value, say 22 lux. The new luminance value will then be sent to platform B. When the delay attack ends, Platform B receives the motion-active event and Rule 18 is triggered. As Rule 18 now observes the new illuminance value, the condition disabling attack disables Rule 18 to take its action.

6) Condition Enabling Attack:

This attack materializes another CRI pattern Condition Bypass which happens when Rule j's action changes a device's state to one that satisfies Rule i's condition. Similar to Condition Block, Condition Bypass can hardly happen when Rules i and j run the same platform, but becomes possible if they are on different platforms.

For example, Rules 1 and 3 in Fig. 6, which are used for controlling the garage door. Suppose the home mode is ªawayº when both rules are triggered by the hall door-closed event.

If they run on the same platform, it is impossible for Rule 1's action (set to ªhomeº mode) to have any impact on Rule 3's condition, since Rules 1 and 3 are triggered simultaneously. However, if Rules 1 and 3 run on different platforms A and B, respectively, the condition-enabling attack can be launched by selectively delaying the door-closed event to the platform B. When Rule 3 receives the delayed door-closed event, the mode has been set to ªhomeº on platform B. As a result, Rule 3 will pass its condition checking and leave the garage door open, which causes safety issues.

7) Action Delaying Attack: Some rules are configured to run together for certain purposes, i.e., they are usually triggered in parallel by the same event, or in a row through a chained execution, and one rule's action can safeguard another. For instance, a user installs Rule 6 (see Fig. 6) to unlock the garage door when he arrives home. However, he is concerned that this rule is unsafe because the presence sensor (based on the location of a smartphone or specialized device) usually has a low precision, i.e., Rule 6 may unlock the door even when the user just passes by or is approaching but still far away 7 from his home, leaving a chance for burglary. To secure Rule 6, Rule 7 is installed to monitor the door with a surveillance camera when the door is unlocked. Rules 6 and 7 run one after another because the action of Rule 6 triggers Rule 7. However, the action delaying attack can delay the action of turning on the camera in Rule 7 for a sufficiently-long period, such that Rule 7 fails to secure Rule 6. Similar to an action disordering attack, an action delaying attack can be realized by delaying the target rule's trigger event, command, or both.

D. Factors Affecting Attack Successes

Rules are vulnerable to a certain type of attack if they satisfy the corresponding Rule Pattern and Deployment Model (see Table I). An attacker launches attacks by delaying the events/commands as shown in What to Delay? (in Table I).

Given a pair of vulnerable rules and the applicable attack type, whether an attack can succeed depends on two factors:

(1) allowed message delay length, and (2) user behaviors. A larger delay gives a wider time window for delaying a trigger event/a command that enables or disables a rule condition. The allowed delay length, denoted as ∆T allowed , depends on the IoT device and platform (see the Delay Range testing in Section V-B1).

User behaviors affect the order and time interval the vulnerable rules are triggered. Consider the action disordering attack on Rules 8 and 12 in Section IV-C4 as an example. Rules 8 and 12 are triggered by two user activities: opening the front door and entering the living room, which generate door-open and motion-active events, respectively. The interval between the two activities is denoted as ∆T interval . If the user approaches the motion sensor in the living room within ∆T allowed after she opens the front door (i.e., ∆T allowed > ∆T interval ; note that we have ignored the difference between the transmission time for sending the two trigger events, as it is usually negligible when there are no attacks), Rule 12 will be triggered earlier than Rule 8 (i.e., the execution order is reversed), leading to a successful attack. Otherwise, the attack fails.

While user behaviors change time by time, there usually exists a pattern and the pattern can be learned from historical events and commands, which can be inferred using side channel attacks [27], [30], [31] (see Section II-B). If the attacker finds that the user never goes to the living room within ∆T allowed after she opens the front door (i.e., ∆T allowed < ∆T interval ), he chooses not to perform an action disordering attack on Rules 8 and 12 since it will never succeed. If ∆T interval is smaller than ∆T allowed with a high probability, then the attack success rate is also high. Note that failed DAI attack attempts remain stealthy since the delay does not trigger alarms at any layers of the IoT protocol stack.

A. Smart Home Testbeds and Attack Implementation

There are no public datasets of smart homes (including devices, rule sets, and configuration). Thus, like previous work on IoT security research [8], [26], [47], we set up smart home testbeds, denoted as T 1 and T 2 , which are in two real homes to evaluate the DAI attacks. We received the IRB approval (see Appendix D for details). There are two persons (a male graduate student and a female graduate student in their 30s and 29s, respectively) living in testbed T 1 , and one person in T 2 (a 27-year-old male graduate student). None of the testbed members are the authors. The smart home layouts and the IoT devices in each smart home are given in Fig. 11 and Table II, respectively. In total, 36 automation rules are installed on 4 automation platforms to interact with 55 IoT devices. The automation rules, which are listed in Table III, are chosen from the official app stores [48] or open-source datasets [49], and the final configurations are based on the discussion between the researchers and the residents living in the testbeds. Each testbed has a WiFi router, providing a WiFi access point and a few Ethernet ports for the deployed IoT devices.

A Raspberry Pi 4 Model B with a 2GB RAM and a 32GB MicroSD card is placed in each testbed to simulate a device compromised by the attacker. It is worth noting that if the attacker and the victim share a WiFi (e.g., at a factory, company, hospital, or university), or the attacker has stolen the WiFi password, the attacker can launch the attacks directly from his device. Plus, an attacker who has compromised the smart home router or has physical contact with the cable can also launch attacks without relying on ARP spoofing. Note ARP spoofing is decades-old mature attacks for hijacking traffic. A famous tool, IoT Inspector [50], has demonstrated that ARP spoofing can hijack a large amount of IoT traffic without causing network instability. We use the ARP spoofing-based technique to turn the Raspberry Pi into a relay node that can examine and delay the traffic between IoT devices/hubs and the WiFi router, or between IoT devices and hubs. By configuring the firewall rules through iptables, all traffic forwarded by the Raspberry Pi is under the control of our attack script. The attack script uses the approach in [29] to recognize events/commands from encrypted traffic. The approach [29] constructs packet-level signatures of IoT events and commands based on source & destination IPs and payload lengths in an offline phase, and then detects events and commands with the signatures in runtime with an accuracy over 97%. The attack script utilizes a DFA matching approach [26] to infer automation rules from the event and command logs of a couple of days (one week in our experiment), achieving an accuracy of 94%. DAI attacks are performed based on the inferred home configuration.

B. Validation of Attacks

We present the methodology and results for validating the DAI attacks in the two testbeds.

1) Methodology: To ease the validation, we ask the testbed members to assist in triggering the automation rules by behaving in controlled patterns. The given instructions incorporate 8 ST multipurpose sensor

• ⇌ST hub⇌ST cloud 1 • denotes the device itself. For simplicity, router is omitted in the connection path.

2 HomePod is the hub of HomeKit. HomeKit automations run on HomePod, not on iCloud. 3 Connected by a smart heater switch 3 , a non-smart microwave and a non-smart oven. 4 Carried with a person. certain daily activities such as leaving/entering home through the garage door, entering a specific room, etc. In particular, when triggering Rules 14, 15 in T 1 and Rules 8, 9 in T 2 , which are triggered by smoke or water leaks, we ask the testbed members to physically trigger the smoke and water sensors in a safe manner. Also, due to the physical restrictions on installing the water valve and sprinkler in the testbeds, we use these rules to control smart switches instead of the real water valve and sprinkler. Although the victim rules are being triggered by the testbed members, our attack script runs to attack the victim rules by delaying the actual device events (e.g., smoke) or commands (see Table IV). To obtain the ground truth for validating if the attacks are successful, we repeat the above process for two days. On the first day, we set the delay period to 0 for all events and commands, i.e., no attacks are conducted. On the second day, we perform DAI attacks by setting some specific time periods to delay the target event or command of the victim rules. We collect the event and command logs for analyzing automation results.

The automation result on the first day is used as the ground truth for comparison. We compare the automation result of each pair of victim rules on the second day (with attack) with those from the first day (without attack). If the results are the same, the rules are not attacked on the second day. Otherwise, the rules may be attacked. To confirm, we manually check whether the automation result on the second day is consistent with the expected attack result; if so, the attack is validated.

Device Logs. Device logs are needed to evaluate the correctness of automation. Among the nine platforms deployed in the testbeds, three of them (i.e., SmartThings, HomeKit, and Alexa) are used as non-endpoint platforms which have access to a broader range of device types. Alexa does not provide a convenient logging tool. Therefore, we choose to use the built-in logging functions on the SmartThings mobile app and on a third-party mobile app, Home+ 4, that can access and export the HomeKit data.

Since the Alexa devices in the two testbeds can be accessed by SmartThings and/or HomeKit, all device events in the testbeds can be collected by at least one of the two methods. Note that we do not collect logs of hub devices since they are not used in automation rules. For the convenience of analysis, we convert the raw event logs from the SmartThings and Home+ 4 apps, denoted as E ST , E HK , to a uniform format. Each element (event) in the reformatted logs is a tuple: ⟨TestbedID, DeviceID, Attribute, Value, Timestamp⟩, where the combination of TestbedID, DeviceID, Attribute and Value uniquely identifies an event type. For example, a motion active event sent by device 7 in testbed T 1 can be denoted as ⟨1, 7 , motion, active⟩. An event type may have multiple instances at different Timestamps.

The new event log is sorted by Timestamp. Note that the timestamps of events are the time instances when the platforms receive the events, which may have been delayed by an attack. This is the reason why we use events on the first day, in the absence of attacks, as ground truth. Based on the event logs E ST and E HK on both days, we can easily track the execution of rules as in existing work [26], [51].

TABLE IV:

A summary of the details for attacking the victim rules in the testbeds, including delayed devices and events/commands, the channels which are utilized to realize the delay, and the delay range that have been tested. COA: Condition Overlapping Attack. III for the rules referred by the given RIDs.

2 See Table II for the devices referred by the given device IDs. 3 The upper bound is non-deterministic because it depends on the HomePod's dynamic behavior in runtime.

Delay Range. Although larger event/command delays usually create larger time windows for performing DAI attacks, the allowable delay length (without causing timeouts) is determined by the implementation of the IoT devices and/or platforms. Delaying the communication for too long will usually trigger timeout behaviors from either the device or platform side. We obtain the allowable delay range of device events and commands by reviewing the specification [52] and analyzing the traffic patterns on the target channels shown in Table IV. We find that the allowable delay range is typically determined by three factors: (1) the interval of periodical messages between an IoT device/hub and a platform, e.g., keep-alive requests (a.k.a., heartbeat) or platform-initiated requests; (2) the maximum allowable delay of keep-alive reply; (3) the maximum allowable delay of event/command reply.

The SmartThings hub sends a keep-alive request to the SmartThings cloud if it has not sent any keep-alive request or device events to the cloud (i.e., the session is idle) for 31 seconds. Then, it sets a timer for 16 seconds and waits for the keep-alive reply. If the hub does not receive a keepalive reply when the timer fires, it will trigger a timeout and disconnect the TCP connection with the cloud. On the other hand, the cloud also listens to the session. If the session is idle for 31 seconds, it will also set a 16-second timer. The cloud disconnects the TCP connection with the hub if it does not receive any message from the hub when the timer fires. The actual maximum delay of an event in runtime is dynamic because it also depends on the timing of the event, i.e., the temporal distance between the event and the last message on the session. An attacker needs to release the event (as well as 10 other messages in the message queue) if he finds that the hub or cloud is about to trigger a timeout. Therefore, the delay range is predictable (between 16-47 seconds) but the attacker needs to dynamically adjust the actual delay length to avoid causing timeout behaviors which may trigger alarms. Philips Hue bridge/Homebridge and HomePod (hosting HomeKit) do not exchange periodic keep-alive messages. Homepod only occasionally initiates a request to query the states of devices that are connected to the bridge and allows for 10-second delay for the reply. According to the HomeKit Accessory Protocol (HAP [52], used by HomeKit), devices, after sending an event message, do not get a reply from HomeKit (on HomePod). Thus, we can delay the events from a Philips Hue bridge or Homebridge until HomeKit requests the device's state (which requires a reply within 10 seconds). Thus, the delay range has a lower bound of 10 seconds and an unbounded upper bound since the HomeKit-initiated request is unpredictable. According to our tests, events can be delayed by more than 10 minutes. In similar ways, we obtain the delay range for other channels. The results are presented in the last column of Table IV.

2) Verifying Results: All attacks listed in Table IV are successfully verified, as shown in Table V. The automation results also show that successful attacks lead to annoyance, inconvenience, and even severe safety threats to the smart home owners. Aside from the verification of the testbeds, we also verify the attack results in a controlled environment, by observing the physical states of devices instead of the IoT events/commands. All the cases in Table IV are physically verified, except for Rules 10 and 11 in testbed T 1 and Rules 5 and 6 in testbed T 2 . During the attack, the humidifiers and lights are offline and cannot receive the turn-on command from Rule 11 in T 1 (or Rule 6 in T 2 ) because their outlets are still in OFF status. When the outlets are turned on, the humidifiers and lights will not receive another turn-on command. As a result, Rule 11 in T 1 (or Rule 6 in T 2 ) fails to work. The humidifiers were indeed not turned on. Interestingly, we observe that the lights (bulbs) are forced to turn on when the connecting outlets turn on. Thus, the attack does not disable the bulbs from being turned on, but only delays them for several seconds.

C. Attack Opportunities

As discussed in Section IV, some of the DAI attacks are opportunistic and can only be successful when a homeowner behaves in certain manners. To evaluate the possibility of DAI attacks on smart homes, we run the two testbeds on a natural daily basis for one week, without providing any guidelines or restrictions on the daily activities to the testbed members. Infrequent automation rules, i.e., Rules 14 & 15 in T 1 and Rules 8 & 9 in T 2 , are excluded in this experiment since they are hardly ever triggered (the triggers are either smoke or water leaks). With the experiment, we aim to answer this question: ªWhat are the opportunities an attacker has to attack the victim rules and what is the success rate of the attack, when the testbed members behave in a natural way?º 1) Methodology: We run both testbeds for one week and collect the device events, without performing any attacks. The collected event logs are transformed to a ⟨TestbedID, DeviceID, Attribute, Value, Timestamp⟩ (same format as in Section V-B). By traversing the event logs, we are able to track the executions of each automation rule. We record each execution instance as a tuple ⟨TestbedID, RuleID, Timestamp⟩. By doing this, we obtain the collection of execution tuples of every rule. Generally speaking, DAI attacks can only be performed when victim rules are triggered by users. To find out attack opportunities in the week, we perform a case-by-case analysis on the combination of the event log and the execution tuples of every pair of victim rules (listed in Table IV). Consider the victim rules 6 and 7 in testbed T 1 . For each execution tuple of Rule 6 in testbed T 1 (i.e., ⟨1, 6, t 1 ⟩), we examine if there is an execution tuple of Rule 7 (i.e., ⟨1, 7, t 2 ⟩), such that 0 ≤ t 2t 1 ≤ 2 (in seconds), and if there is a door-closed event of the garage door 21 (i.e., ⟨1, 21 , door, closed, t 3 ⟩) in the event log, such that t 1 ≤ t 3 ≤ t 2 . If true, it means that Rule 6 closed the garage door, which in turn triggered the execution of Rule 7, which is an interaction that can be attacked by the DAI attacks; we mark the executions of both rules as an attack opportunity.

As discussed in Section IV, to successfully launch an attack, the attacker need to delay specific events by a sufficient period. For Rules 6 and 7, we trace back the event logs to find the most recent away mode event (denoted as ⟨1, N/A, mode, away, t 4 ⟩).

If the time difference between t 2 and t 4 is smaller than a threshold ∆T ′ (i.e., the maximum allowable delay of the away mode event), i.e., t 2t 4 < ∆T ′ , Rules 6 & 7 can be attacked successfully; otherwise, the attack fails. In this way, we obtain the number of attack opportunities and successful attacks for every victim rule pair.

Note that, in order to evaluate attack opportunities (i.e., number of successful attacks), we choose not to perform real attacks on the testbeds, for two major reasons. First, real attacks can cause severe safety issues to the testbed members. Second, the attacks against different victim rule pairs may have conflicts in delaying a specific channel.

2) Results: In Table VI, we present the number of attack opportunities and successful attacks over a week. The victim rule pairs are triggered between 3 to 12 times, creating sufficient opportunities for the attacks. The numbers of successful attacks that took place each day are also presented.

The average success rate of all attacks is 0.864. Most attacks have a success rate of 1.00, i.e., they can successfully cause CRI on the victim rules. The attacks on Rules 6 & 7, 8 & 9 in testbed T 1 and Rules 5 & 6 in T 2 fail several times due to the restriction of the allowed delay ∆T allowed (see Section IV-D about factors affecting attack successes). For example, an attack attempts to change the execution order of Rules 5 & 6 in T 2 by delaying the door-open event. Assuming the interval between the time she opens the door and that she enters the study room is ∆T interval , if ∆T interval > ∆T allowed , the attack fails, because it cannot delay the door-open event 11 (which triggers Rule 5) as much as until the user enters the study room (which triggers Rule 6). Note that DAI attacks are independent in general, unless two concurrent attacks require different delays on the same event(s) or command(s). When an attack fails, no TCP session is disconnected and the attacker can make attempts to perform other attacks seamlessly.

In short, the results in Table VI show that the attacker has sufficient opportunities to launch attacks, raising severe safety and security concerns.

D. Comparison with Jamming Attacks

Jamming does not require the victim home's WiFi password. We thus evaluate whether jamming can be used to construct DAI attacks. Two jamming techniques are investigated. The first one is WiFi micro-jamming [53], which can slightly delay the wireless communications by switching on and off transmitting disruptive signals in high frequency. The test result shows that the introduced delay (10 millisecond or so) is too short to conduct effective attacks. Another technique [54] jams wireless communication by cramming the wireless medium with random frames. Following this technique, we use an Alfa AWUS036NHA wireless adapter that is powered by the open-source code [55] to jam WiFi frames. For each attack listed in Table IV, we use jamming to discard (i.e., infinitely delay) the events/commands listed in the Event/Command to Delay? column and observe the consequences.

The results in Table VII show that jamming replicates some of the attacks on the victim rule pairs (6 out of 11). This indicates jamming, as a low-level attack method alternative to TCP hijacking and ARP spoofing, can be used to attain the same effect of some DAI attacks, which is alarming. The differences of the two attack methods are as follows. First, the TCP-hijacking based method only delays events/commands but does not discard them, while jamming that discards messages can only construct some of the attack types. For example, if a trigger event is discarded (rather than delayed), the subscribing rule will not be triggered. Second, general jamming frequently causes TCP timeout and disconnection alerts. We discuss reactive jamming that does not discard messages or cause disconnection in Section VI-B.

A. Countermeasures Against DAI Attacks

First, the smart home end users can raise the bar for attackers to intrude into the IoT network by using strong WiFi passwords and setting up an isolated sub-network for IoT if they share a WiFi network with other people. Also, vendors of IoT devices/hubs and WiFi routers should enhance the security of their products. For example, we find that many IoT devices and home routers are not resistant to ARP spoofing (also verified in the IoT Inspector project [50]), although effective defenses against ARP spoofing exist. One possible reason that explains the wide feasibility of ARP spoofing is that TLS gives the illusion of ªsufficientº protection under traffic hijacking 12 attacks, while our work illustrates the contrary. We estimate there is a long way to go to eliminate ARP spoofing attacks.

Second, device vendors and platform providers can reduce the intervals of TLS-protected heartbeat (a.k.a., keep-alive) messages and enforce two-way liveness checking of event and command messages, which can significantly reduce the allowed delays. However, this requires IoT vendors to modify their protocols and device firmware. Plus, more frequent heartbeat messages lead to a higher overhead, which should be considered carefully in the IoT design.

Third, there are known synchronization and recovery techniques for handling inconsistency and disorder issues in distributed systems [56], [57], [58]. A challenge to deploy such techniques in IoT is the lack of a central entity that has a global view and control on heterogeneous IoT devices and multiple proprietary IoT platforms, or a mechanism for distributed platforms to collaboratively synchronize correct observations on devices in the fragmented IoT ecosystem.

Fourth, researchers can design approaches to detecting potential DAI attacks. Various techniques in the state-ofthe-art works [6], [47], [26], [5] can be utilized to extract deployment information (such as devices, rules, and platforms) from a given smart home system. After incorporating the extracted information into our formal model, the observation equivalence based technique (described in Section IV-A and Appendix C) can be used to detect potential DAI attacks by verifying whether any pair of rules are not CRI-resistant in the presence of delay attacks. The detection result can be presented to the user, who can then re-configure the rules. An alternative mitigation strategy is to enforce security properties/goals, which prevent devices from transitioning into unsafe states [8].

IX. CONCLUSION

We studied unique cross-rule interference (CRI) problem due to the inconsistency and disorder issues in single-platform multi-path and multi-platform smart home systems. We uncovered that selective messages delay attacks have detrimental impacts on smart home automation, causing various CRI problems that cannot be detected by existing detectors. We revealed seven categories of such attacks, referred to as Delay-based Automation Interference (DAI) attacks, which were analyzed and demonstrated using two smart homes. The evaluation results show that DAI attacks of all the seven categories can be launched, and an attacker can conduct DAI attacks with a high success rate, without raising alerts in any layer of the current IoT protocol stack.

Methodology. We design a survey asking people who have experience with IoT devices and automation to provide information of their own deployments. Specifically, we ask them to answer simple questions such as the number of devices and mobile/web companion apps in their home, and more complex questions by writing down the list of their devices, companion apps, and automation rules. The survey questions and responses are made publicly available at https://github.com/HaotianChi/SH-survey.git

Results. We receive 85 responses from the survey participants. Through a qualitative analysis on the collected information of devices, companion apps and automation rules, we rebuild the deployment of each participant's home. The result shows that the number of SPSP, SPMP and MP deployments are 15 (17.6%), 17 (20.0%) and 53 (62.4%), respectively. Among the 53 MP deployments, 36 use two platforms, 11 use three, 5 use four and 1 uses five. A total of 82.4% deployments in the survey are SPMP or MP deployments. The results show that the testbed setup in Section V is realistic.

B. Formal Modeling of Smart Home Systems

We use the process calculus [41] to formally model multipath multi-platform smart home systems and delay-based attacks. The process calculus extends the timed process calculus [42] with two action prefixes: reading sensor values and writing values to actuators. Physical Environment. Let F ⊂ F be a set of physical features (e.g., temperature), Ŝ ⊂ S a set of sensors, Â ⊂ A a set of actuators. Note that in this paper, each actuatable device (e.g., a lock) is conceptually split into an actuator that executes commands and a sensor that measures the device state. For a set of names N , we define R N as the set of functions that assign a real value (broadly, integers and Booleans are replaceable with reals) to each name in N . A physical environment E is a 5-tuple ⟨ξ f , ξa, evol, ξs, meas⟩: ξ f ∈ R F ∪ Â is the state (i.e., physical features or actuator values) function that returns the value of the state; ξ a ∈ R Â is the actuator function that returns the current value of an actuator; evol : R F ∪ Â × R Â → R F ∪ Â is the evolution function, which returns the next state function upon changes of actuators; meas : R F ∪ Â → R Ŝ is the measurement function that returns the reading of a sensor.

In addition to physical features, we include actuators in the state function to model the dependence between actuators. For example, a smart microwave, even turned on, cannot function if its power cable is connected to a smart plug that is OFF. It is not the focus of this paper to precisely model the physical evolution laws. For the simplicity of analysis, we assume that the evolution function evol only takes as input the state function ξ f and actuator function ξ a to determine a new state function. 4 Also, we assume the sensors S measures physical features (i.e., the meas function) without errors. Local hub devices are omitted since they only forward messages. IoT Processes. Processes are defined in the following syntax:

Terminated process is written as nil. The process idle.P continues as P after sleeping for one time unit. Action prefixes (ranged over π, π 1 , and π 2 ) contain six actions: sending values to channels (snd c⟨v⟩), receiving values from channels (rcv c(x)), reading new sensor measurements (read s(x)), reading new actuator states (read a(x)), and writing values on actuators (wrt ā(v)) and unobservable action (τ ). P \c behaves as P but the channel name c is restricted to P and can only be used for communications between components within P . We use P {v/x} to denote the substitution of the variable x with the value v in P . The process π 1 .P + π 2 .Q is called summations (or sums) and can enact either π 1 .P or π 2 .Q. The process P ∥ Q denotes the parallel composition of concurrent processes P and Q. The process if (b) {P } else {Q} is a standard conditional statement. H⟨w 1 , • • • , w k ⟩ denotes a recursive process and can be considered as an invocation, with actual parameters w

Each platform L has access to a subset of all sensors S ⊂ Ŝ and actuators Ã ⊂ Â. The database on the platform maintains a function ξ ′ s ∈ R S that returns the current state of each sensor. For convenience, we define two database primitives: a function value in db that returns the values of specified devices x and a meta-process update db that updates the value of a sensor:

Example. We use an automation rule (when the homeowner arrives, unlock the door) on platform A and another one (when the user says ªI am homeº, if the door is unlocked, lock it) on platform B as a running example to concretize a system. A presence sensor PS and a smart lock LK connect with a platform A that runs R1, and a smart speaker SP and the smart lock LK connect with platform B running R2. For the sake of brevity, we omit all components (e.g., IoT hubs, routers, endpoint clouds) that only forward messages. Thus, the smart home is Sys = E P where the physical environment E = ⟨ξ f , ξa, evol, ξs, meas⟩ is defined as

ªI am homeº DETECTED else CLEAR)}. The timestamp i = 0 • • • n denotes the discrete time clock and the process P is the parallel composition of the following sub-processes; 16 300 -SenPS = read PS(val).snd eventA(PS, val).idle.SenPS -SenSP = read SP(val).snd eventB(SP, val).idle.SenSP -SenLK = read LK(val).snd eventA(LK, val).snd eventB (LK, val) .idle.SenLK -ActLK = rcv cmdA(LK, val).wrt LK(val).idle.ActLK + rcv cmdB(LK, val).wrt LK(val).idle.ActLK -SrvPltA = rcv eventA(id, val).snd update A (id, val)

.snd trigger R1 (id, val).idle.SrvPltA + rcv actionR1(id, val).snd cmdA(id, val).idle.SrvPltA -SrvPltB = rcv eventB(id, val).snd update B (id, val)

.snd trigger R2 (id, val).idle.SrvPltB + rcv actionR2(id, val).snd cmdB(id, val).idle.SrvPltB -RuleR1 = rcv triggerR1(id, val t) , where P ( t) = P (c → c′ ) ∥ Delay (c, c′ , ĩd, ṽ al, t). Specifically, P (c → c′ ) substitutes new channels c′ for ones c that are used by the rcv actions in P. The sub-processes that read from the attacked channels c are converted to ones that read from the corresponding channels c′ maintained by the delay attack processes. Labelled Transition Semantics. A smart home system is modelled as a labelled transition system (LTS) in the structural operational semantics (SOS) style. The transitions are of kind P α -→ Q for actions (a.k.a., labels) ranged over by α in the set {idle, τ, snd c⟨v⟩, rcv c(x), read s(x), read a(x), wrt ā⟨v⟩}. The transition rules are shown in Table VIII. Most of them are the same as the standard ones [41], [42], except that we distinguish the transition rules for parallel compositions under delay-absent and delay-present situations where (NoDelayCom) and (DelayCom) are used, respectively. For brevity, we sometimes use the original notations Sys = E P to denote a system under delay attacks, without rewriting the attacked channels.

C. Formal Verification and Categorization of DAI Attacks

We use a shorthand Sys = E • R[ D ▷ L] to denote a system where each rule R j ∈ R run on a platform L j ∈ L and reads/writes a set of devices D j ∈ D. To make a practical sense, we only consider well-formed systems where every platform has access to all devices used by the rules running on it, i.e., D j ⊂ ( S ∪ Ã). E denotes the physical environment. Consider an attack-present system Sys

where two automation rules R1 and R2 are installed on two platforms L 1 and L 2 , respectively. L 1 and L 2 can be the same or different platforms. We define a specification system which runs R1 and R2 on an oracle platform L which accesses devices without any delays, i.e.,

). Sys and Sys * describe the real system and the mentally expected system by users, respectively.

Verification in SPSP Systems. A recent work [12] adopts Generalized Non Deducibility on Composition (GNDC) [78] to define a CRI-free system: a rule R1 does not interfere with another rule R2 if the compositional runtime behavior of R1 and R2 does not differ from the behavior of R2 when running along. Formally, R1 does not interfere with R2 under a hiding weak bisimulation notion:

for H R1 def = obserable(R1) denoting a set of hidden actions of R1 that yield to observable results. Two rules R1 and R2 are CRI-free when R1 and R2 do not interfere with each other.

However, this only considers an SPSP scenario where all automation rules run on a platform equivalent to an oracle platform L * and can only detect CRI rooted from misprogramming or mis-configuration, subject to the same limitations of other existing work [5], [6], [7], [9].

Verification in SPMP and MP Systems. In this paper, we aim to model the uncovered CRI scenarios in a situation where two rules automation rules R 1 and R 2 may run on different platforms and the communication channels suffer from delays. In this sense, R 1 and R 2 are CRI-free if in addition to the hiding weak bisimulation, a standard weak bisimulation holds:

Formula 2 ensures that the interactions between R1 and R2 in the real system and specification system are equivalent at every time unit. However, it is a sufficient but not necessary condition. It is too strict to say that the real system has a significant CRI problem if it only deviates from the specification system at a specific time unit. For example, if the attacker delays all communications evenly by one time unit, the real system will lag behind the specification system but may still produce the correct automation result. Thus, verifying CRI with Formula 2 usually causes false alarms. To address this problem, we define an idle-insensitive weak bisimulation ≈ idle . Let ⇒ idle def = {τ,idle} ------→ * denote a sequence of zero or more transitions each of which could be a τ or idle transition. We replace the notion of an experiment e = ⇒ in the definition of standard weak bisimulation [41], [79] -----→ Q ′ Delay(c,c ′ ,id,val,t)

Provided a specific home deployment and attack strategy (the target event/command), we can use Formula 3 to verify if the system yields different automation results from a specification system, or say if the real system has unique CRI issues under the attack. We can easily prove that the two rules in the running example always generate the correct result in SPSP system even under delay attacks. However, when the two rules run on different platforms, delaying the UNLOCKED value on channel event B results in a violation of Formula 3. Due to the space limit, proofs are omitted. Methodology for Systematic Categorization. To systematically and comprehensively discover possible DAI attacks that cause CRI problems, we generalize a smart home deployment and represent it as the smart home calculus parametric on some enumerable factors (sensor measurements, automation rules, attack strategies). We then enumerate these factors to find violation scenarios of the CRI-free condition (Formula 3). State explosion challenges exist since smart home deployments are highly diverse and it is infeasible to enumerate all deployments and states. To address this challenge, we make several assumptions or abstractions to reduce the complexity of smart home deployments and the enumeration space.

First, we assume that the natural communication delays are negligible compared to the injected delays by the attacker. We omit the sub-processes that only forward messages, such as hubs, endpoint clouds, routers, and add up the communication delays on these channels (if any) to the end-to-end delay between a device and a platform.

Second, we simplify the models of IoT devices and rules. Note that automation rules follow a trigger-condition-action paradigm. A rule's trigger is actually a boolean expression that checks a device value (e.g., when temperature exceeds 75 • F ) and its condition is a set of such boolean expressions. A rule action is not always binary (e.g., dim the light to 75%). However, the interaction relation between a rule's action and another rule's trigger, condition, or action is binary. For example, one may ask if a rule R1's action can control an actuator (e.g., turn on lights) to a value that makes another rule R2's trigger (e.g., when the brightness is high) or condition (e.g., if the lights are on) satisfied, or if the action is contradictory to another rule R2's action (i.e., turn off lights). Therefore, we binarize the automation rules and device values. We consider that each device has two values (0 and 1) and each rule deals with binary values of devices. Without loss of generality, we assume each rule condition only checks one device.

Third, we simplify the rule-device bindings. Without a specific home deployment, one cannot know what devices are bound to each rule. In our simplification, three devices are granted to each rule for its trigger, condition and action, respectively. Thus, two rules R1 and R2 choose from a set of six devices D = {d 1 , d 2 , • • • , d 6 }. In practice, a rule's trigger and condition always check different devices. We pick D 1 = {d 1 , d 2 , d k |k ∈ {1, 2, 3}} for R1 and D 2 = {d i , d j , d k |d i , d j , d k ∈ D; i ̸ = j; x < y if x > 3, y > 3, x ∈ {i, j}, y ∈ {j, k}} for R2. We only consider the interactions between two automation rules R1 and R2 since most, if not all, interactions among more than two rules contain sub-interactions between two rules.

With the above abstractions, we enumerate the rules, ruledevice bindings, initial device states and the attacker's target events/commands and verify CRI in each configuration. In this process, we observe that the attacks against some different configurations essentially belong to the same category. Therefore, we perform a manual qualitative analysis to combine the similar attack scenarios and classify DAI attacks into seven categories (see Section IV-B). Note that the above abstractions are only for easing the exploration of possible attacks. Provided a specific deployment, our theoretic technique (calculus) can verify CRI without the abstractions.