Scalable Analysis of Interaction Threats in IoT Systems

Team: Mohannad Alhanahnah, Clay Stevens, Bocheng Chen, Qiben Yan, Hamid Bagheri

University of Wisconsin-Madison, University of Nebraska-Lincoln, Michigan State University

Introduction

IoTCOM combines static analysis with lightweight formal methods to automatically infer relevant specifications of IoT apps in an analyzable formal specification language and check them as a whole for interaction threats. IoTCOM has proven to be highly effective at detecting a broad spectrum of interaction threats triggered through cyber and physical channels, many of which were previously unknown. The contributions of this work are:

Classification of interaction threats between IoT apps. We identify and rigorously define seven classes of multi-app interaction threats between IoT apps over physical and cyber channels both within and among apps.
Formal model of IoT systems. We develop a formal specification of IoT systems, respecting cyber and physical channels and representing the behavior of IoT apps apropos the detection of safety and security vulnerabilities. We construct this specification as a reusable Alloy~\cite{AlloyBook} module to which all extracted app models conform.
Automated analysis. We show how to exploit the power of our formal abstractions by building a modular model extractor that uses static analysis techniques to automatically extract the precise behavior of IoT apps into a trimmed Behavioral Rule Graph, respecting the logical conditions that impact the behavior of the app rules, which is then captured in a format amenable to formal analysis.
Experiments. We evaluate the performance of IoTCOM against real-world apps developed for multiple IoT platforms (SmartThings and IFTTT), corroborating IoTCOM's ability in effective compositional analysis of IoT apps interaction vulnerabilities in the order of minutes. We make research artifacts, including the entire Alloy specifications, and the experimental data available to the research and education community.

Motivating Example

The below example points to one of the most demanding issues in the smart home IoT ecosystem, i.e., detection of multi-app coordination threats. What is required is a system-wide reasoning---that determines how those individual rules could impact one another when the corresponding apps are installed together---not comfortably attainable through conventional analysis methods such as static analysis or testing, which are more suited for identifying issues in individual parts of the system.

Interaction Threats

In this work, we provide formal definitions of 7 classes of interaction threats. These threats can occur through physical and/or virtual interactions. Following is the definition of the 7 interaction threats:

Action-trigger (T1)

Action-condition match (T2)

Action-condition not match (T3)

(T4) Self coordination

(T7) Exclusive event

(T5) conflic Action-action

(T6) repeat Action-action

Following is the definition of the 7 interaction threats:

Approach

IoTCOM comprises two components: Behavior Rule Extractor and Formal Analyzer. The Behavior Rule Extractor performs static analysis and applies novel graph abstraction for extracting the behavior of IoT apps. The Formal Analyzer utilizes bounded model checking for identifying potential safety and security violations.

IoTCOM Overview

Evaluation Results

RQ1: Accuracy

To evaluate the accuracy of IoTCOM and compare it against other state-of-the-art techniques, we used the IoTMAL suite of benchmarks. We also developed 3 bundles (Bundle4 - Bundle6) contain violations involve physical channels. IoTCOM effectively detects all of the violations (100% precision) with fewer false positives (92.8% recall). The following table represents the accuracy of IoTCOM in comparison with IoTSAN and SOTERIA.

RQ2: Effectiveness

We evaluated the capability of IoTCOM to identify violations in real-world IoT apps. We conducted our analysis on numerous bundles of IoT apps from both SmartThings and IFTTT. The following diagrams represent two samples of violations that have been detected by IoTCOM. Fig.1 illustrates a chain of 3 Groovy apps, performing unintended behavior. This violation shows an infinite actuation loop. For detecting this violation, interactions over the luminance physical and scheduling APIs (i.e. runIn) should be recognized. Figure 2 presents another violation that involves an IFTTT Applet and Groovy Apps. A precise control flow analysis is required for identifying this violation.

Fig.1: Example violation of T4: Lights continually turn off and on. Dashed line represents coordination via the physical channel

Fig.2 Example violation of T1: Cyber coordination between apps may leave the door unlocked when no one is home. The first rule is guarded by a condition that the home owner not be present

Fig.3 Example violation of T5: Both "on'' and "off'" commands sent to the same light due to the same event. Dashed line represents coordination via the luminance physical channel.

Alloy Counterexamples for the case studies in Figures 1-3

Fig.4 Counterexample generated by Alloy for the violation presented in Fig 1 (Fig. 6 in the paper)

Fig.5 Counterexample generated by Alloy for the violation presented in Fig 2 (Fig. 7 in the paper)

Fig.6 Counterexample generated by Alloy for the violation presented in Fig 3 (Fig. 8 in the paper)

RQ3: Verification Time Comparison

In this part, we evaluates the verification time required by IoTCOM and IoTSAN. Where IoTSAN manually specifies the initial configuration for each app in the bundle as part of the model. But IoTCOM does not require specification of a single initial configuration, instead exhaustively checking all configurations that fall within the scope of the app model. To perform a fair comparison between the two approaches, we generated initial configurations for 11 bundles of apps and converted them into~a~format supported by IoTSAN. We then ran the two techniques considering all valid initial configurations to avoid missing~any~violation.

Overall, the timing results show that IoTCOM reduces the violation detection time by 92.1% on average and by as much as 99.5%, and is able to effectively perform safety/security violation detection of bundles of real-world apps in just a few minutes (on an ordinary laptop), confirming that the presented technology is indeed feasible in practice for real-world~usage.

Verification time by IoTCOM and IoTSAN to perform the same safety violation detection in a logarithmic scale

Safety Properties

Research Artifacts and Source Code

Static analysis implementation
Benchmark apps: contains all benchmark apps that have been used for evaluating IoTCOM. All individual Apps and Bundle1-Bundle3 are obtained from IoTMAL, while Bundle4 - Bundle6 have been developed to show violations that involve interactions over physical channels.
Policies: Alloy definitions for the Safety and Security Properties
IoTAppModel and IoTChannelMapping : Alloy Specifications for modeling IoT apps and mapping IoT channels
Real-world Apps: list of bundles used in RQ2 and RQ3 and Alloy models for 3732 apps used for constructing the 622 bundles.
MotivatingExample: includes Ally models for the apps in the motivating example and the property for generating the counterexample. To do so, download the Zip file, unzip it, then open main.als in the Alloy Analyzer (we used alloy4.2.jar)
Case studies demonstrated in RQ2: contains Alloy models of each bundle and the definitions of the violated property. README file shows the instructions for regenerate RQ2 results each model to generate the violations.
Additional IFTTT Apps: includes 2000+ IFTTT json applets used for constructing app bundles
Alloy Model Files Generated from Additional IFTTT Apps: contains 937 Alloy model files.

Page updated

Google Sites

Report abuse