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

TL;DR

TAPFixer is an automated framework that detects and repairs vulnerabilities in home automation rules caused by unsafe interactions, using negated-property reasoning and model checking to improve safety.

Contribution

It introduces a novel negated-property reasoning algorithm for automatically repairing home automation rule vulnerabilities, enhancing safety in user-friendly systems.

Findings

Achieves 86.65% success rate in repairing vulnerabilities

Effectively detects rule interaction vulnerabilities in real-world apps

User study confirms practical usefulness of TAPFixer

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.