A model checking-based security analysis framework for IoT systems

Zheng Fang, Hao Fu, Tianbo Gu, Zhiyun Qian, Trent Jaeger, Pengfei Hu, Prasant Mohapatra

Research output: Contribution to journalArticlepeer-review

15 Scopus citations


IoT systems are revolutionizing our life by providing ubiquitous computing, inter-connectivity, and automated control. However, the increasing system complexity poses huge challenges for security as IoT devices are distributed, highly heterogeneous, and can directly interact with the physical environment. In IoT systems, bugs in device firmware, defects in network protocols, and design flaws in automation rules can lead to system breach or failure. The challenge gets even more escalated as the possible attacks may be chained together in a long sequence across multiple layers, rendering the existing vulnerability analysis frameworks inapplicable. In this paper, we present FORESEE, a model checking-based framework to comprehensively evaluate IoT system security. It builds a multi-layer IoT hypothesis graph by simultaneously modeling all of the essential components in IoT systems, including the physical environment, devices, communication protocols, and applications. The model checker can then analyze the generated hypothesis graph to validate system security properties or generate attack paths if there are any violations. An optimization algorithm is further introduced to reduce the computational complexity of our analysis. Our framework verifies hypothesis graphs with millions of nodes in less than 100 seconds. The illustrative case studies show that our framework can detect more potential threats than the existing approaches.

Original languageEnglish (US)
Article number100004
JournalHigh-Confidence Computing
Issue number1
StatePublished - Jun 2021

All Science Journal Classification (ASJC) codes

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications
  • Computer Science Applications
  • Computational Theory and Mathematics


Dive into the research topics of 'A model checking-based security analysis framework for IoT systems'. Together they form a unique fingerprint.

Cite this