Abstract
Although extensive research has been conducted on securing the Internet of Things (IoT) communication protocols, various vulnerabilities and exploits are continuously discovered and reported. Since vulnerabilities are introduced from either insecure communication protocols or defectiveness of applications, it is difficult to identify them during the software development or testing phase. In this paper, we present IoTVerif, a system that automatically verifies the Secure Socket Layer/Transport Layer Security (SSL/TLS) certificate for IoT applications that utilize broker-based messaging protocols. IoTVerif constructs the specification of an IoT protocol and verifies its security properties, without relying on prior knowledge about communication protocols. Once the specification is constructed, a general-purpose model checker automatically verifies those properties, as well as generates counter-examples if any property does not hold. We analyze the effectiveness of IoTVerif with real-world IoT-related applications. Our evaluation results show that IoTVerif can successfully identify vulnerabilities from IoT applications, which are exploitable by the man-in-the-middle (MITM) and TLS renegotiation attacks. IoTVerif holds a great promise for reverse-engineering emerging IoT messaging protocols and identifies the vulnerabilities from IoT-related applications.