PaperlayerView exact revision on arXiv

Source-linked AI summary

IoTSan: Fortifying the Safety of IoT Systems

Dang Tu Nguyen, Chengyu Song, Zhiyun Qian, Srikanth V. Krishnamurthy, Edward J. M. Colbert, Patrick McDaniel

arXiv:1810.09551v2cs.CR

TL;DR

IoT safety flaws can arise from app interactions, device or communication failures, and misconfiguration, while much prior work examined components or cyberspace rather than the system holistically. IoTSan applies model checking with IoT-focused optimizations, app translation, and attribution; its evaluation found 147 possible safety violations among 150 SmartThings apps.

  • Problem

    IoT safety research has often focused on individual components or cyberspace, with few holistic analyses of physical-space safety and interactions across a system.

    Source: §1 · p. 1

  • Method

    IoTSan uses model checking with state-space optimizations, translates apps into a model-checker-ready form, and attributes violations to bad apps or misconfigurations.

    Source: §1 · p. 2

  • Results

    IoTSan discovered 147 possible safety violations while evaluating 150 SmartThings apps.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The system’s scope includes unsafe states associated with misconfiguration, information leakage, and device or communication failures.

    Source: §4 · p. 5

    The prototype handles systems of about 30 apps and cannot handle apps that dynamically discover devices and interact with them.

    Source: §11 · p. 11

Abstract

from arXiv · show

Today's IoT systems include event-driven smart applications (apps) that interact with sensors and actuators. A problem specific to IoT systems is that buggy apps, unforeseen bad app interactions, or device/communication failures, can cause unsafe and dangerous physical states. Detecting flaws that lead to such states, requires a holistic view of installed apps, component devices, their configurations, and more importantly, how they interact. In this paper, we design IoTSan, a novel practical system that uses model checking as a building block to reveal "interaction-level" flaws by identifying events that can lead the system to unsafe states. In building IoTSan, we design novel techniques tailored to IoT systems, to alleviate the state explosion associated with model checking. IoTSan also automatically translates IoT apps into a format amenable to model checking. Finally, to understand the root cause of a detected vulnerability, we design an attribution mechanism to identify problematic and potentially malicious apps. We evaluate IoTSan on the Samsung SmartThings platform. From 76 manually configured systems, IoTSan detects 147 vulnerabilities. We also evaluate IoTSan with malicious SmartThings apps from a previous effort. IoTSan detects the potential safety violations and also effectively attributes these apps as malicious.

1 INTRODUCTION

IoTSan addresses IoT safety as a holistic problem: interactions among apps, devices, and failures can create unsafe states that component-focused or cyberspace-only studies may miss. It uses model checking, app translation, state-space reductions, and attribution to find and classify such violations.

1 INTRODUCTION

  • IoT safety research often examines individual components or cyberspace, while few efforts take a holistic view that includes physical-space safety.Apps, devices, configurations, interactions, and device or communication failures can combine to produce bad states.Source: §1 · p. 1
  • IoTSan maps safety checking to model checking and reduces state-space growth by analyzing interacting apps and eliminating unnecessary interleavings.Its attribution module flags potentially malicious apps and assigns other unsafe states to bad design or misconfiguration.Source: §1 · p. 2
  • Across 76 configurations of 150 apps, IoTSan found 147 violations of 20 properties: 135 from app interactions and 12 from device/communication failures.In one case, four apps had to interact to cause a violation, making it difficult to spot manually.Source: §1 · p. 2
  • The prototype translates SmartThings apps written in Groovy into Promela for Spin model checking.The evaluation also examined 150 SmartThings apps across 76 configurations.Source: §1 · p. 2
  • IoTSan attributes safety violations to bad apps or misconfigurations and attributed all nine evaluated known malicious apps as potentially malicious.The attribution method was reported to achieve 100% accuracy on those nine apps.Source: §1 · p. 2

2 BACKGROUND AND SYNOPSIS

The section introduces IoT system components and SmartThings, illustrates how user configuration can create unsafe behavior, and motivates model checking as a way to reason about system states and interactions.

2 BACKGROUND AND SYNOPSIS

  • An IoT system is described as including a hub and devices, a platform for smart apps, and a companion mobile or web app for configuration and control.The approach is framed around smart homes but is described as conceptually applicable to other platforms and settings.Source: §2 · p. 2

2.1 Samsung SmartThings

  • SmartThings apps use Groovy and interact with devices through handlers; apps can subscribe to device events, control actuators, and register callbacks for external events or timers.The hub communicates with devices over protocols such as ZigBee or Z-Wave; the described ZigBee setup uses multiple retransmissions, making unsafe transitions from benign packet loss rare.Source: §2.1 · p. 2

2.2 Misconfiguration Problems

  • Misconfiguration is a common source of safety violations, and unclear descriptions, many options, or limited user domain knowledge can contribute.In a user study, five of seven volunteers configured Virtual Thermostat to control both heater and AC outlets, contrary to the app’s intended either/or use.Source: §2.2 · pp. 2–3

2.3 Model Checking as a Building Block

  • As apps and devices grow in number, analyzing all their possible interactions becomes difficult; static analyses can produce false positives, while dynamic analyses can miss flaws..Source: §2.3 · p. 3
  • Model checking systematically explores program states against a specification, but exhaustive exploration is computationally challenging, so it is often used to find a violating computation in part of the reachable state space.This bug-finding use is also called bounded model checking.Source: §2.3 · p. 3
  • The authors adopt model checking for flexible property verification, concrete counterexamples, holistic app-interaction analysis, and efficiency relative to exhaustive testing.The state space can still grow unwieldy and require exponential time to explore.Source: §2.3 · p. 3
  • Spin’s BITSTATE mode stores state hashes rather than full states, an approximate approach that does not provide complete verification but has evidence of effective state coverage.The paper uses Spin to check whether safety properties can be violated.Source: §2.3 · p. 3

3 SCOPE AND THREAT MODEL

IoTSan targets vulnerabilities that attackers can exploit to cause unsafe physical states or leak sensitive information. Its scope includes natural device failures and certain physical or communication attacks, while treating devices, the cloud, and the companion app as trusted.

3 SCOPE AND THREAT MODEL

  • IoTSan targets vulnerabilities exploitable by attackers to cause bad physical states or leak sensitive information, with safety requirements supplied by users or security experts.Examples include an unlocked front door when nobody is home and a heater turned off below a predefined temperature.Source: §3 · p. 3
  • Private information may be sent through messaging interfaces only, and message recipients must match configured phone numbers or contacts.The policy treats network-interface transmissions as disallowed for private information; users decide whether to allow control information sent to servers.Source: §3 · p. 4
  • Devices, the cloud, and the companion app are trusted, but IoTSan considers physical event injection and maliciously induced device or communication failures.Targeted defenses against attacks such as sensor spoofing or jamming are out of scope.Source: §3 · p. 4
  • IoTSan also examines whether natural device failures, including depleted batteries, can lead an IoT system into a bad physical state.The passage names ZigBee and Z-Wave sensors and garage door openers among devices whose failures users have reported.Source: §3 · p. 4
  • Attribution identifies apps as possibly malicious, but confirmation is left to human experts or other systems.Malicious apps may exploit configuration weaknesses and introduce problematic events that affect other apps.Source: §3 · p. 4

4 SYSTEM OVERVIEW

IoTSan models event-driven IoT behavior and analyzes related app handlers to find unsafe states. Its modules translate apps, extract configurations, check safety properties, and help identify causes of violations.

4 SYSTEM OVERVIEW

  • IoT events can trigger long cyber-physical sequences, so IoTSan analyzes interactions across a system rather than isolated handlers.Its architecture includes an App Dependency Analyzer, Translator, Configuration Extractor, Model Generator, and Output Analyzer.Source: §4 · p. 4, Figure 3 · p. 4
  • The App Dependency Analyzer identifies handlers that must be checked together, while the Translator converts Groovy programs into Promela.The analyzer avoids checking unrelated handlers; the Translator addresses Groovy features that complicate model checking.Source: §4 · p. 4
  • The Configuration Extractor obtains system settings, and the Model Generator combines them with event-handler code and safety properties for Spin.It uses sequential modeling to reduce unnecessary interleaving before checking for property violations.Source: §4 · p. 4
  • The Output Analyzer attributes violations to potentially malicious apps, poor designs, or misconfiguration and suggests removing apps or changing settings.IoTSan also checks for information leakage and whether device or communication failures and misconfiguration can cause unsafe states.Source: §4 · pp. 4–5

5 APP DEPENDENCY ANALYZER

The App Dependency Analyzer builds a graph of event-handler interactions and groups related handlers for joint model checking. It merges sets when handlers can produce conflicting outputs and removes redundant subsets.

5 APP DEPENDENCY ANALYZER

  • Handlers are linked when one handler’s output events overlap another handler’s input events; strongly connected components become composite vertices.Static analysis identifies inputs from subscriptions, device-state reads, and scheduled interrupts, and outputs from device-state-changing APIs.Source: §5 · p. 5
  • A leaf vertex’s initial related set contains itself and all its ancestors, so handlers that may influence it can be analyzed together.The example graph’s arrows represent input and output events, and its vertices illustrate parent-child relationships.Source: §5 · p. 5
  • Related sets are merged when handlers share output events of different types, such as switch/off and switch/on.Checking potential output conflicts takes O(E^2) links in the worst case, where E is the number of output edges.Source: §5 · p. 5
  • After removing related sets that are subsets of larger sets, the remaining sets are jointly analyzed without rechecking those subsets.The model checker verifies a subset when it verifies the larger related set containing it.Source: §5 · p. 5

6 TRANSLATOR

The Translator converts SmartThings Groovy apps into Java representations that Bandera can process, addressing platform-specific syntax, dynamic typing, and Groovy utilities. It infers types and maps supported collection operations into Java arrays and code.

6 TRANSLATOR

  • Bandera supports Java but not Groovy, while SmartThings adds language features and Groovy’s dynamic typing and utilities complicate conversion.SmartThings’ compiler is not open sourced, and Bandera natively supports Java arrays rather than Groovy collections.Source: §6 · p. 5
  • The G2J Translator converts smart-app Groovy source into Java ASTs, with separate components handling SmartThings syntax and regular Groovy parsing.The system extends the Groovy compiler and integrates it into Bandera’s front end.Source: §6 · pp. 5–6
  • The SmartThings Handler parses platform-specific syntax into vanilla Groovy and extracts app input declarations as global variables.It also adds definitions for predefined objects and APIs absent from vanilla Groovy.Source: §6 · p. 6
  • Type inference propagates types from declarations, constants, known APIs, and objects through method calls until no further variables can be inferred.The procedure tracks calling-context arguments and return values to find type information.Source: §6 · p. 6
  • The translator maps commonly used Groovy collection types to Java arrays and converts supported operations such as list addition into Java code.For example, it infers a list return type and translates it into a Java array type, adding an explicit return statement for non-void methods.Source: §6 · pp. 6–7

7 CONFIGURATION EXTRACTOR

IoTSan extracts installed apps, devices, and configurations, then models their event-driven interactions to check safety properties. Its model generator also accounts for device and communication failures and can expose unsafe outcomes caused by app interactions.

7 CONFIGURATION EXTRACTOR

  • The Configuration Extractor gathers installed devices, smart apps, and app configurations from the SmartThings management interface for the Model Generator.For generic devices, users provide device-association information, such as which appliance an outlet controls.Source: §7 · p. 7

8 MODEL GENERATOR

  • The model generator processes sensor events through subscribed app handlers, whose actuator commands can update device state and trigger further events.It enumerates event permutations up to a configuration-specific maximum; system time and scheduled callbacks are also modeled.Source: §8 · p. 7
  • Device and communication failures are modeled by considering offline devices and failed communications, which can prevent state changes or event broadcasts.Sensor events are considered with the sensor online or offline; actuator command handling likewise considers availability and communication success or failure.Source: §8 · pp. 7–8
  • Sequential modeling considers permutations of external events and handles their resulting internal events atomically, reducing verification time compared with strict interleavings.In small-system experiments, the sequential approach found all violations found by the strict concurrent model.Source: §8 · p. 8
  • IoTSan checks for conflicting and repeated actuator commands, including commands that may indicate a denial-of-service or replay attack.These command checks are among 45 selected safety properties.Source: §8 · p. 8
  • The checked properties also cover desired physical states, suspicious commands and information leakage, and app responses to device or communication failures.The paper describes 38 physical-state properties, four suspicious-behavior properties, and one robustness property.Source: §8 · p. 8
  • A modeled chain from a presence event through a location-mode change to an unlock command leaves the main door unlocked when no one is home.The example reveals that the Unlock Door app's implementation also reacts to mode changes, although its description says it unlocks only on user input.Source: §8 · p. 8

9 OUTPUT ANALYZER

The Output Analyzer distinguishes violations attributed to a newly installed app from those attributed to configuration. It tests configurations individually and in combination with previously installed apps.

9 OUTPUT ANALYZER

  • The Output Analyzer first verifies a new app across its possible configurations; if the violation ratio exceeds a threshold such as 90%, it attributes the app as malicious.The ratio is the proportion of configurations that violate the user-defined properties.Source: §9 · pp. 8–9
  • If the first phase does not meet the threshold, the analyzer checks the new app alongside previously installed apps across configurations.A violation ratio above the threshold attributes the new app as bad; otherwise, the violation is attributed to misconfiguration and safe-configuration suggestions are provided.Source: §9 · pp. 8–9

10 EVALUATIONS

Across SmartThings configurations and app groups, IoTSan identifies safety violations, attributes malicious apps, and evaluates techniques to reduce analysis cost. The evaluation also compares sequential and concurrent model checking.

10.1 Test Cases and Configurations

  • The evaluation used SmartThings market apps with author- and volunteer-chosen configurations, prior malicious apps, and selected good and bad app groups for performance tests.The experiments also measured running time and the scale ratio, which quantifies reductions in event handlers jointly verified.Source: §10 · p. 9, §10.1 · pp. 9–10

10.2 Identifying Unsafe Configurations

  • 38 violations of 11 properties appeared in expert-configured market apps without device or communication failures; failures caused violations of 9 additional properties.One reported case leaves the main door unlocked while people sleep; a failure case also prevents an intrusion notification from being sent to law enforcement.Source: §10.2 · p. 10
  • 97 violations of 10 properties occurred across 70 volunteer configurations for 10 app groups; one AC-and-heater property was violated in 21 configurations across 5 groups.Some configurations violated multiple properties, so the violation count exceeded the number of configurations.Source: §10.2 · p. 10

10.3 Violation Attribution

  • IotSan correctly attributed all ContexIoT malicious apps; among 11 market apps, it detected 6 with 100% violation ratios, attributing them as bad apps, while the remaining apps were attributed to bad configurations.The remaining apps had violation ratios of 70% or lower because safe configurations with no violations existed.Source: §10.3 · p. 10

10.4 Scalability

  • 3.4x was the average reduction in problem size from the App Dependency Analyzer across 150 market apps.The reduction is measured in event handlers jointly considered for verification.Source: §10.4 · p. 10

10.5 Concurrent vs. Sequential

  • Sequential design significantly reduced verification runtime relative to concurrent design in the tested good app group; the concurrent run was stopped after a week when it ran forever.The sequential approach verified a larger system of 5 related apps and 10 devices in about 5 hours for 10 events.Source: §10.5 · p. 10

11 DISCUSSION

The discussion describes adapting IoTSan to IFTTT and reports a limited prototype evaluation. It also identifies scope and implementation constraints on the SmartThings prototype.

11 DISCUSSION

  • Most IoTSan modules can be reused for IFTTT, while the translator requires a comparatively larger change.The IFTTT translator extracts trigger and action services; modeled services include Amazon Alexa, Google Assistant, and Nest Thermostat.Source: §11 · pp. 10–11
  • 7 violations of 4 unsafe physical states were found in a limited prototype evaluation of 10 IFTTT rules.The prototype treats each rule as an app with one event handler and models services as sensor or actuator devices.Source: §11 · p. 11, Table 9 · p. 11
  • The prototype handles systems of about 30 apps and requires apps to subscribe explicitly to devices; dynamic device discovery is unsupported.The paper also notes limits in the translator's support for heterogeneous collections and dynamic language features.Source: §11 · p. 11

12 RELATED WORK

Prior IoT security work often targets individual devices, protocols, platforms, or apps, while IoTSan focuses on system-level physical safety, practical model checking, failures, and malicious-app attribution. Related work also includes runtime app/platform modifications and earlier IoT model-checking efforts.

12 RELATED WORK

  • IoT security research spans devices, protocols, platforms, privacy and information leakage, firmware vulnerabilities, and smart-app design flaws.Several efforts modify app source code or platforms to enforce good runtime behavior.Source: §12 · pp. 11–12
  • Unlike runtime enforcement that modifies apps or platforms, IoTSan statically identifies possible violations of specified physical and cyber safety properties without app modifications.The related work includes runtime proposals targeting good smart-app behavior.Source: §12 · p. 12
  • Earlier IoT model-checking work addressed system-level threats or basic correctness, whereas IoTSan targets practical physical-safety analysis, robustness, and malicious-app attribution.Its practical challenges include scale and making Groovy amenable to model checking.Source: §12 · p. 12

13 CONCLUSIONS

IoTSan uses model checking to identify causes of unsafe physical or cyber states and provide counterexamples. It addresses practical analysis challenges, and evaluations report unsafe configurations and 100% accuracy in flagging considered bad apps.

13 CONCLUSIONS

  • IoTSan uses model checking to identify causes of bad physical or cyber states and provides counterexamples illustrating those causes.The framework targets badly designed apps, undesirable interactions, and device or communication failures.Source: §13 · p. 12
  • IoTSan addresses model-checking state-space explosion and automatically translates app code into a model-checking-amenable form.Source: §13 · p. 12
  • IoTSan identifies unsafe configurations and flags considered bad apps with 100% accuracy in its evaluations.Source: §13 · p. 12
Loading 1810.09551v2…