Poster: A Novel Formal Threat Analyzer for Activity Monitoring-based Smart Home Heating, Ventilation, and Cooling Control System

ABSTRACTContemporary home control systems determine real-time heating/cooling demands utilizing smart sensor devices, giving rise to demand control heating, ventilation, and cooling (DCHVAC) systems, thus improving the home's energy efficiency. The adoption of activity monitoring in the smart home control system further augments the controller efficiency and improves occupants' comfort and productivity, elderly monitoring, and so forth. Additionally, the learned occupants' activity patterns help embed machine learning (ML)-based abnormality detection capability to track inconsistencies among the zone sensor measurements. Hence, the incorporation of an activity monitoring system assists anomaly detection models (ADMs) in detecting false data injection (FDI) attacks that are being glowingly researched due to their massive damage capability. However, in this work, we propose a novel attack strategy that identified that the knowledge of occupants' activities along with indoor air quality (IAQ) and occupancy sensor measurements allows the attackers to launch even more hazardous attack (i.e., significant increment in energy cost/ worsening health conditions for the occupants). Hence, it is crucial to analyze the security of the activity monitoring-based smart home DCHVAC system. Accordingly, we propose a novel formal threat analyzer that analyzes the threat space of the smart home DCHVAC control system, which is modeled by rule-based control policies and ML-based ADMs. The rules from the ADM are extracted through an efficient algorithm. The constraints associated with the rules are solved through a satisfiability module theorem (SMT)-based solver. %We performed our initial evaluation of the proposed threat analyzer's effectiveness on the Center of Advanced Studies in Adaptive Systems (CASAS) dataset using some metrics. We will further experiment with other metrics along experimenting with our collaborator's dataset (KTH live-in lab) and open-source Örebro datasets for assessing the framework with realistic occupants' activity. Moreover, we also created our prototype testbed for evaluating the feasibility of the proposed attack and threat analyzer.