Abstract
Developing secure Internet of Things (IoT) applications that are free of vulnerabilities and resilient against exploit is desirable for software developers and testers. In this paper, we present IoTVerif, an automated tool that can verify SSL/TLS (Secure Socket Layer/Transport Layer Security) X.509 certificate validation of IoT messaging protocols utilized by real-world IoT client applications. IoTVerif does not require any prior knowledge about the messaging protocol, but simply correlates the observed network trace of an application with its execution context. IoTVerif helps IoT client application developers identify the SSL/TLS vulnerabilities based on certificate validation. We specifically target MQTT, a broker-based protocol that has attracted increasing popularity in the IoT application market.
We used IoTVerif to analyze the server X.509 certificate validation in 15 well-known MQTT client applications. Our result revealed that 5 (33.3%) of the applications examined are vulnerable to man-in-the-middle (MITM) and/or TLS renegotiation attacks. Our result also shows that IoTVerif can generate a Finite State Machine (FSM) that depicts the interaction between the application and the IoT broker and automatically identifies various attacks. It has the potential to reverse-engineer the emerging IoT messaging protocols and identify the vulnerabilities in the IoT applications.