MPInspector: A Systematic and Automatic Approach for Evaluating the Security of IoT Messaging Protocols


Qinying Wang, Zhejiang University; Shouling Ji, Zhejiang University; Binjiang Institute of Zhejiang University; Yuan Tian, University of Virginia; Xuhong Zhang, Zhejiang University; Binjiang Institute of Zhejiang University; Binbin Zhao, Georgia Institute of Technology; Yuhong Kan and Zhaowei Lin, Zhejiang University; Changting Lin and Shuiguang Deng, Zhejiang University; Binjiang Institute of Zhejiang University; Alex X. Liu, Ant Group; Raheem Beyah, Georgia Institute of Technology


Facilitated by messaging protocols (MP), many home devices are connected to the Internet, bringing convenience and accessibility to customers. However, most deployed MPs on IoT platforms are fragmented, which are not implemented carefully to support secure communication. To the best of our knowledge, there is no systematic solution to perform automatic security checks on MP implementations yet.

To bridge the gap, we present MPInspector, the first automatic and systematic solution for vetting the security of MP implementations. MPInspector combines model learning with formal analysis and operates in three stages: (a) using parameter semantics extraction and interaction logic extraction to automatically infer the state machine of an MP implementation, (b) generating security properties based on meta properties and the state machine, and (c) applying automatic property based formal verification to identify property violations. We evaluate MPInspector on three popular MPs, including MQTT, CoAP and AMQP, implemented on nine leading IoT platforms. It identifies 252 property violations, leveraging which we further identify eleven types of attacks under two realistic attack scenarios. In addition, we demonstrate that MPInspector is lightweight (the average overhead of end-to-end analysis is ~4.5 hours) and effective with a precision of 100% in identifying property violations.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

@inproceedings {274709,
author = {Qinying Wang and Shouling Ji and Yuan Tian and Xuhong Zhang and Binbin Zhao and Yuhong Kan and Zhaowei Lin and Changting Lin and Shuiguang Deng and Alex X. Liu and Raheem Beyah},
title = {{MPInspector}: A Systematic and Automatic Approach for Evaluating the Security of {IoT} Messaging Protocols},
booktitle = {30th USENIX Security Symposium (USENIX Security 21)},
year = {2021},
isbn = {978-1-939133-24-3},
pages = {4205--4222},
url = {},
publisher = {USENIX Association},
month = aug,

Presentation Video