View Proposal

---

Proposer

Rob Stewart

Title

Reasoning about Smart Home automation rules

Goal

Apply LTL model checking to validate Home Assistant automation rules

Description

Home Assistant is widely used open source home automation software. It allows users to set up automation rules, with triggers based on many things, including sensor readings (person detection) and time (after 6pm). These rules follow the If-This-Then-That model of Trigger Action Programming (TAP). These rules can be expressed as YAML files, or using the Home Assistant GUI, or using a 3rd party tool GUI like Node-RED. They typically have (1) a trigger, (2) optional additional preconditions, and (3) an action. For large home automations, a user may have Home Assistant dozens if not hundreds of automation rules. These can contradict each other (turn a light on when someone enters the room and turn light off when someone enters the room), or cause race conditions (if light off then turn on and if light on then turn off). Sometimes they are quite subtle race conditions, e.g. turn light on when luminescence is low and turn light off when luminescence is high because the light bulbs emits light which alters the luminescence. More generally, multiple issues across rules can arise: (1) rule latency: A TAP rule’s action may not be executed immediately when its trigger activates, (2) rule interaction: There are channels that can chain TAP rules unexpectedly via physical attributes and underpin security issues, (3) safety properties: i.e., something bad should never happen and (4) liveness properties: i.e., something good eventually happens. Moreover, chains of rules can lead to privilege escalation and privacy leakage, where threat modelling can identify home safety (e.g. fire risks) and security (e.g. unlocked windows/doors). See recent related work: "Temporal Specification Oriented Fuzzing for Trigger-Action-Programming Smart Home Integrations" https://dl.acm.org/doi/pdf/10.1145/3744916.3764543 "TAPInspector: Safety and Liveness Verification of Concurrent Trigger-Action IoT Systems" https://arxiv.org/pdf/2102.01468 "SAFECHAIN: Securing Trigger-Action Programming from Attack Chains" https://arxiv.org/pdf/1903.03760 This project will build on this work. Either by extending their methods, or by performing systematic comparisons of their methods, or by implementing these methods in open-source home automation projects like Home Assistant to have real-world impact. Alternatively, another recent trend is for users to ask LLMs to simplify their TAP automation rules: instead, could the methods in the recent literature be used to avoid the uncertainty of LLM-based approaches for automation simplification?

Resources

Background

Url

External Link

Difficulty Level

Moderate

Ethical Approval

Full

Number Of Students

1

Supervisor

Rob Stewart

Keywords

Degrees

Bachelor of Science in Computer Science
Bachelor of Science in Computer Systems
Bachelor of Science in Information Systems
Bachelor of Science in Software Development for Business (GA)
Master of Engineering in Software Engineering
Master of Design in Games Design and Development
Master of Science in Artificial Intelligence
Master of Science in Artificial Intelligence with SMI
Master of Science in Business Information Management
Master of Science in Computer Science for Cyber Security
Master of Science in Computer Systems Management
Master of Science in Computing (2 Years)
Master of Science in Data Science
Master of Science in Human Robot Interaction
Master of Science in Information Technology (Software Systems)
Master of Science in Network Security
Master of Science in Robotics
Master of Science in Software Engineering
Bachelor of Science in Computing Science
Bachelor of Engineering in Robotics
Bachelor of Science in Computer Science (Cyber Security)
Master of Science in Robotics with Industrial Application
Postgraduate Diploma in Artificial Intelligence
Bachelor of Science in Statistical Data Science
BSc Data Sciences
MSc Applied Cyber Security
BSc Information Systems with Data Analytics
Bachelor of Science in Computational Sciences and Software Engineering