Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

TAPFixer: Automatic Detection and Repair of Home Automation Vulnerabilities based on Negated-property Reasoning

Yinbo Yu, Yuanqi Xu, Kepu Huang, Jiajia Liu

TL;DR

This work tackles safety vulnerabilities arising from rule interactions in Trigger-Action Programming (TAP) for home automation. It introduces TAPFixer, which statically detects vulnerabilities by modeling TAP rules as a finite automaton with latency and physical-channel effects, uses model checking against a set of 53 properties, and automatically derives patches via a novel negated-property reasoning (NPR) algorithm. The approach is evaluated on market HA apps (1177 TAP rules, 53 properties) with an average repair success of 86.65%, plus a user study confirming practical usefulness. The results demonstrate that TAPFixer can effectively eliminate root causes of rule interactions in both logical and physical spaces, enabling safer TAP-based automation before deployment.

Abstract

Trigger-Action Programming (TAP) is a popular end-user programming framework in the home automation (HA) system, which eases users to customize home automation and control devices as expected. However, its simplified syntax also introduces new safety threats to HA systems through vulnerable rule interactions. Accurately fixing these vulnerabilities by logically and physically eliminating their root causes is essential before rules are deployed. However, it has not been well studied. In this paper, we present TAPFixer, a novel framework to automatically detect and repair rule interaction vulnerabilities in HA systems. It extracts TAP rules from HA profiles, translates them into an automaton model with physical and latency features, and performs model checking with various correctness properties. It then uses a novel negated-property reasoning algorithm to automatically infer a patch via model abstraction and refinement and model checking based on negated-properties. We evaluate TAPFixer on market HA apps (1177 TAP rules and 53 properties) and find that it can achieve an 86.65% success rate in repairing rule interaction vulnerabilities. We additionally recruit 23 HA users to conduct a user study that demonstrates the usefulness of TAPFixer for vulnerability repair in practical HA scenarios.

TAPFixer: Automatic Detection and Repair of Home Automation Vulnerabilities based on Negated-property Reasoning

TL;DR

This work tackles safety vulnerabilities arising from rule interactions in Trigger-Action Programming (TAP) for home automation. It introduces TAPFixer, which statically detects vulnerabilities by modeling TAP rules as a finite automaton with latency and physical-channel effects, uses model checking against a set of 53 properties, and automatically derives patches via a novel negated-property reasoning (NPR) algorithm. The approach is evaluated on market HA apps (1177 TAP rules, 53 properties) with an average repair success of 86.65%, plus a user study confirming practical usefulness. The results demonstrate that TAPFixer can effectively eliminate root causes of rule interactions in both logical and physical spaces, enabling safer TAP-based automation before deployment.

Abstract

Trigger-Action Programming (TAP) is a popular end-user programming framework in the home automation (HA) system, which eases users to customize home automation and control devices as expected. However, its simplified syntax also introduces new safety threats to HA systems through vulnerable rule interactions. Accurately fixing these vulnerabilities by logically and physically eliminating their root causes is essential before rules are deployed. However, it has not been well studied. In this paper, we present TAPFixer, a novel framework to automatically detect and repair rule interaction vulnerabilities in HA systems. It extracts TAP rules from HA profiles, translates them into an automaton model with physical and latency features, and performs model checking with various correctness properties. It then uses a novel negated-property reasoning algorithm to automatically infer a patch via model abstraction and refinement and model checking based on negated-properties. We evaluate TAPFixer on market HA apps (1177 TAP rules and 53 properties) and find that it can achieve an 86.65% success rate in repairing rule interaction vulnerabilities. We additionally recruit 23 HA users to conduct a user study that demonstrates the usefulness of TAPFixer for vulnerability repair in practical HA scenarios.
Paper Structure (32 sections, 4 theorems, 22 equations, 8 figures, 15 tables, 1 algorithm)

This paper contains 32 sections, 4 theorems, 22 equations, 8 figures, 15 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminary
  3. TAP Rule Formulation
  4. Rule Interaction Vulnerabilities
  5. Overview
  6. Motivation and Threat Model
  7. TAPFixer Design Intuition
  8. Rule Modeling and Vulnerability Detection
  9. Modeling Information Extraction
  10. Rule Interaction Modeling
  11. Property Specification and Prioritization
  12. Vulnerability Detection
  13. Rule Interaction Vulnerability Repair
  14. Negated Property Generation and Spurious Indicator Identification
  15. Patch Reasoning
  16. ...and 17 more sections

Key Result

Theorem 1

The single-state correctness property is logically equivalent to the multi-state one since it is obviously a special case of multi-state properties where $n$ in $\land_{i=1}^n state_{i}$ is equal to 1.

Figures (8)

  • Figure 1: Motivation examples of rule interactions.
  • Figure 2: Overview of TAPFixer.
  • Figure 3: The core idea of our NPR algorithm for vulnerability repair. Model abstraction via interpolation is used to involve a larger state space for patch searching, so the negated counterexample $CEX^{\neg\phi}$ can contain repair patches for the vulnerability $CEX^{\phi}$.
  • Figure 4: Example of counterexamples and their violating state. We use @ to denote the event and omit entity attributes that do not change or are irrelevant to the violation. The state with double circles denotes the violating state.
  • Figure 5: Repair success rate and the number of generated patches for G8-G23 with 110 rule groups. The numbers in parentheses represent the number of properties contained in the property set.
  • ...and 3 more figures

Theorems & Definitions (6)

  • Theorem 1
  • Theorem 2
  • Theorem 3
  • proof
  • Theorem 4
  • proof