Source-linked AI summary
Soteria: Automated IoT Safety and Security Analysis
Z. Berkay Celik, Patrick McDaniel, Gang Tan
TL;DR
Existing IoT platforms cannot generally determine whether apps or app environments are safe, secure, and function correctly. SOTERIA translates IoT code into an intermediate representation, extracts state models, and applies model checking to identified properties. Its evaluations found violations in individual apps, combined environments, and the MALIOT test corpus, while also exposing limitations around reflection, dynamic configuration, and platform scope.
Problem
Existing IoT platforms lack general mechanisms to evaluate whether an IoT app or environment adheres to safety, security, and functional properties.
Method
SOTERIA translates platform-specific IoT source code into an intermediate representation, extracts app state models, and applies model checking to specified properties.
Results
SOTERIA found property violations in individual SmartThings apps and multi-app groups, and correctly identified 17 of 20 unique violations in MALIOT.
Takeaways & Limitations
SOTERIA identifies safety, security, and functional errors both in isolated IoT apps and in interactions among apps used together.
Takeaways & Limitations
SOTERIA can produce false positives for reflective calls, does not fully handle dynamic device permissions and configurations, and its implementation and evaluation focus on SmartThings.
Abstract
from arXiv · showhide
Broadly defined as the Internet of Things (IoT), the growth of commodity devices that integrate physical processes with digital systems have changed the way we live, play and work. Yet existing IoT platforms cannot evaluate whether an IoT app or environment is safe, secure, and operates correctly. In this paper, we present Soteria, a static analysis system for validating whether an IoT app or IoT environment (collection of apps working in concert) adheres to identified safety, security, and functional properties. Soteria operates in three phases; (a) translation of platform-specific IoT source code into an intermediate representation (IR), (b) extracting a state model from the IR, (c) applying model checking to verify desired properties. We evaluate Soteria on 65 SmartThings market apps through 35 properties and find nine (14%) individual apps violate ten (29%) properties. Further, our study of combined app environments uncovered eleven property violations not exhibited in the isolated apps. Lastly, we demonstrate Soteria on MalIoT, a novel open-source test suite containing 17 apps with 20 unique violations.
1 Introduction
IoT systems can affect physical environments, but existing platforms lack general mechanisms to determine whether apps and environments are safe, secure, and function correctly. SOTERIA addresses this gap with static analysis and model checking.
- IoT apps can control devices in ways that create unsafe or damaging conditions, including unlocking doors or turning off heat.
- Existing IoT platforms provide policies and vetting, but tools for evaluating general safety and security remain limited.
- SOTERIA translates IoT source code into an intermediate representation, extracts state models, and model-checks safety, security, and functional properties.
- SOTERIA was evaluated on 65 SmartThings apps and used to develop MALIOT, an open-source corpus of 17 flawed apps.
2 Background
SmartThings provides an IoT software stack in which apps control devices through capabilities, events, and actions, but app review and formal verification remain distinct processes. Model checking represents programs as state machines and checks them against temporal properties; Soteria’s examples show failures in individual and interacting apps.
- SmartThings connects a hub, apps, and cloud backend, with the hub mediating communication among devices, backend services, and mobile apps.
- Device capabilities combine actions and events: actions control device states, while events are triggered by state changes and drive app handlers.
- Official SmartThings market apps undergo source-code review, whereas self-published apps do not receive an official review process.
- Model checking represents programs as state-machine models and checks their executions against properties expressed with temporal logic.
- Soteria’s Smoke-Alarm example illustrates that an environment can violate a property when individually analyzed apps interact.
3 Motivation and Assumptions
Soteria motivates automated analysis through examples where an individual app contains a safety bug and otherwise-safe apps create a hazard when combined. The approach models app behavior, encodes safety properties in temporal logic, and checks the resulting models while excluding cryptographic attacks and user privacy from scope.
- The Smoke-Alarm app is intended to sound an alarm and activate related devices when smoke and heat conditions indicate a fire.
- Soteria models the Smoke-Alarm source code as a transition system whose states change according to smoke-detection outputs.
- Soteria’s architecture analyzes IoT applications and environments through a static-analysis workflow that supports the illustrated single-app and multi-app cases.
- The analysis found that the actual Smoke-Alarm implementation stops sounding moments after smoke is detected, violating the property that the alarm always sounds with smoke.
- The combined Smoke-Alarm and Water-Leak-Detector environment violates sprinkler activation because the leak detector shuts off the water valve when sprinklers release water.
- The threat model includes design flaws and malicious code but excludes adversaries thwarting security measures and investigations of user privacy.
4 SOTERIA
SOTERIA translates IoT source code into an intermediate representation, extracts state models, and uses model checking to validate safety, security, and functional properties. Its analyses model both individual apps and interacting environments, while addressing state explosion, model precision, and contextual property selection.
- System analysis: SOTERIA analyzes IoT apps through an intermediate representation, state-model extraction, property identification, and model checking.The IR captures app lifecycle elements, including entry points, event handlers, and call graphs; model checking assesses apps independently or alongside other apps.
- From source code to IR: The IR records permissions, event/action subscriptions, and call graphs to represent devices, inputs, event handlers, and invoked methods.SOTERIA extracts devices and user inputs from permissions, associates events with handlers, and creates separate call graphs for entry points.
- State model extraction: SOTERIA models an app as a deterministic state machine and reports nondeterministic state models as safety violations.The state model is defined by states, transition labels, and a state-transition function; deterministic operation is treated as a condition for safe IoT-device operation.
- Limitations: Reflective calls and dynamic device permissions or configurations limit analysis precision and can produce false positives or property violations.Imprecise reflective-call targets enlarge state models, while dynamic permissions and configurations may yield violations because of erroneous device and input configurations.
- Identifying IoT properties: SOTERIA’s property set is not universally determined: environments may need to tailor property discovery to their specific security and safety needs.The paper notes that identifying the correct properties is difficult and that contextual property-discovery methods are partly judgment-based.
- Identifying IoT properties: Property discovery uses assets, functional requirements, and functional constraints to define general and app-specific properties over states and transitions.Examples include preventing conflicting writes on a control-flow path, preventing conflicting writes across handlers, keeping a door locked when the user is away, and shutting a valve during a water leak.
- Validating properties: SOTERIA constructs multi-app state models by combining app states, enabling analysis of interactions that can create conflicting or unsafe behavior.Examples include Smoke-Alarm and App2 issuing conflicting switch commands under the same smoke-detected event, and a three-app environment locking a door during smoke at home.
5 Implementation
SOTERIA builds its intermediate representation and state model directly from Groovy ASTs, then translates the model for visualization and NuSMV-based verification. The implementation avoids bytecode-based analysis because Groovy’s reflective calls hinder Soot’s results.
- IR and State Model Construction: SOTERIA builds the IR directly from Groovy AST nodes using compiler hooks and AST visitors.The visitors collect compilation information, including class resolution, imports, variable scopes, and method calls.
- IR and State Model Construction: Groovy bytecode analysis with Soot was infeasible because the compiler translates direct method calls into reflection.The Smoke-Alarm app compiled to bytecode with 14 reflective calls, and Soot did not produce good analysis results for reflective input.
- Framework Overview: SOTERIA’s framework separates the analysis frame, an intermediate representation and state-model visualization, and property-violation output.The middle region shows the IR and a visual state model for an example IoT app.
- Model Checking: SOTERIA visualizes state models with GraphViz and verifies temporal-logic properties using the NuSMV symbolic model checker.NuSMV confirms satisfied properties or produces counterexamples for false properties.
- Model Checking: To address state explosion, SOTERIA combines BDD-based and SAT-based model checking through NuSMV options.
6 Evaluation
SOTERIA was evaluated on market and synthetic SmartThings apps, including isolated and multi-app environments, property verification, state reduction, and runtime overhead. It identified verified violations in individual apps, additional interaction-related violations, and most MALIOT violations while keeping verification fast.
- Market App Evaluation: 65 SmartThings apps were analyzed against general and app-specific properties, with nine individual apps and three multi-app groups flagged for violations.Manual checking verified that all reported market-app violations were true positives.
- Market App Evaluation: None of the official apps were flagged, while one third-party app violated multiple properties and eight third-party apps violated a single property.The authors associate the absence of official-app violations with the official market’s lengthy manual vetting.
- Multi-App Analysis: 17 apps across three examined groups violated 11 properties in multi-app environments.The groups represent apps that users may install together and authorize to use the same devices.
- MALIOT Evaluation: 17 of 20 unique MALIOT property violations were correctly identified across 17 flawed apps.SOTERIA produced a false warning for reflective calls and missed sensitive-data leakage and dynamic-device-permission violations outside its analysis scope.
- MicroBenchmarks: State reduction often produced an order-of-magnitude decrease in states for apps with numerical-valued device attributes.Reduction applied to 14 apps accessing ten such devices; three apps had unchanged state counts.
- MicroBenchmarks: The average state-model generation time was 17.3±2 seconds for an app with 180 states, while property verification took milliseconds.Extraction time includes IR extraction, graphical-model generation, SMV generation, and logging; runtime depends partly on state-reduction algorithms.
7 Limitations and Discussion
The discussion identifies limitations from imprecise reflection handling, dynamic configurations and permissions, and evaluation restricted to SmartThings home automation. The authors propose refining reflection analysis and extending SOTERIA to other IoT platforms.
- Analysis Limitations: Reflective calls are modeled as targeting any method, enlarging state models and potentially producing false positives during property checking.The authors plan to use string analysis to refine reflective-call target sets.
- Analysis Limitations: Dynamic device permissions and app configurations can yield violations from erroneous user-supplied settings, such as leaving a door unlocked overnight.The limitation concerns configurations made at installation time.
- Scope: SOTERIA’s implementation and evaluation are based on SmartThings, a home-automation platform, rather than other IoT domains.The authors identify agriculture, healthcare, and automobile platforms as targets for future extension.
8 Related Work
Prior IoT research examined platform and device security, vulnerability analysis, sensitive-data leaks, and correctness. SOTERIA differs by automatically extracting IoT-app state models from an intermediate representation and checking them against desired properties.
- IoT Security and Safety: Prior work studied security in emerging IoT platforms and devices, including vulnerability analysis for light systems and smart locks.These studies found that apps can be exploited to gain unauthorized device control.
- Formal Verification: Model checking has been used to analyze correctness in security-critical systems, including network vulnerabilities and Android privacy leaks.These efforts provide related applications of model checking beyond IoT app analysis.
- SOTERIA’s Distinction: SOTERIA is presented as the first system to automatically extract state models from IoT-app IR and check correctness against desired properties.Earlier work modeled diverse software systems to explore their state spaces.
9 Conclusions
The paper presents SOTERIA for extracting state models from IoT code and finding security, safety, and functional errors, evaluated on SmartThings apps and the MALIOT corpus. The authors report violations in isolated and multi-app environments and plan broader analyses and tools.
- Contribution: SOTERIA extracts state models from IoT code to find security, safety, and functional errors.The system was evaluated in studies of SmartThings-market apps and the MALIOT app corpus.
- Findings: The evaluations found property violations both in isolated apps and in apps used together in multi-app environments.Future work includes extending analysis kinds and developing tools for IoT implementations and environments.
A Source Code and IR of Example Apps
The appendix presents source code and intermediate representations for three example IoT apps: Smoke-Alarm, Water-Leak-Detector, and Thermostat-Energy-Control.
- The appendix covers three example apps: Smoke-Alarm, Water-Leak-Detector, and Thermostat-Energy-Control.
- Each example is presented with its Groovy source code and Intermediate Representation (IR).
- The examples are organized in Sections A.1, A.2, and A.3, respectively.
A.1 Smoke-Alarm App
The Smoke-Alarm app monitors smoke and battery events, uses configured devices and a threshold, and represents its behavior through an IR.
- The Smoke-Alarm app is provided in both Groovy source code and IR listings.
- When the battery level falls below the configured threshold, the source code turns on the switch and logs a low-battery warning.
- The app subscribes to smoke-detector and battery events in its IR.
- Its configuration selects smoke detector, switch, alarm, valve, and battery devices, plus a user-defined threshold.
A.2 Water Leak Detector App
The appendix presents source code and IR for the Water-Leak-Detector and Thermostat-Energy-Control apps, including event handling, device actions, notifications, and application properties.
- A.2 Water Leak Detector App: The Water-Leak-Detector source code and IR are presented in Listings 3 and 4.
- A.2 Water Leak Detector App: The Water-Leak-Detector app can notify contacts, send a push notification, or send an SMS after detecting a leak.
- A.2 Water Leak Detector App: The Water-Leak-Detector app closes its valve when the water sensor reports a wet event.
- Thermostat-Energy-Control App: The Thermostat-Energy-Control app subscribes to location-mode and power-meter events in its IR.
- General IoT properties are listed in Table 1, while application-specific IoT properties are listed in Table 2.
C MALIOT Test Suite Applications
The MALIOT test-suite section categorizes applications by property-violation ground truth and reports SOTERIA results alongside general and application-specific property descriptions.
- Table 3 categorizes MALIOT applications according to their property-violation ground truth.
- The MALIOT app source code is available in the IoTBench repository.
- Table 1 describes general properties, while Table 2 describes application-specific properties.
- General properties are defined according to the device access granted to an app.
- Some properties are validated using predicates supplied by users or developers.
- The property-results notation distinguishes true positives, false positives, cases requiring dynamic analysis, and properties excluded from the attacker model.