Verifying Software Vulnerabilities in IoT Cryptographic Protocols

TL;DR

This paper introduces the Encryption-BMC and Fuzzing (EBF) framework, combining Bounded Model Checking and Fuzzing to verify security vulnerabilities in IoT cryptographic protocols, demonstrated through a case study on S-MQTT.

Contribution

The paper presents a novel combined verification framework, EBF, for detecting vulnerabilities in IoT cryptographic protocols using BMC and Fuzzing techniques.

Findings

EBF effectively identified vulnerabilities in the S-MQTT protocol.

Combined BMC and Fuzzing improves verification coverage.

Framework demonstrates practical applicability in IoT security analysis.

Abstract

Internet of Things (IoT) is a system that consists of a large number of smart devices connected through a network. The number of these devices is increasing rapidly, which creates a massive and complex network with a vast amount of data communicated over that network. One way to protect this data in transit, i.e., to achieve data confidentiality, is to use lightweight encryption algorithms for IoT protocols. However, the design and implementation of such protocols is an error-prone task; flaws in the implementation can lead to devastating security vulnerabilities. These vulnerabilities can be exploited by an attacker and affect users' privacy. There exist various techniques to verify software and detect vulnerabilities. Bounded Model Checking (BMC) and Fuzzing are useful techniques to check the correctness of a software system concerning its specifications. Here we describe a framework called Encryption-BMC and Fuzzing (EBF) using combined BMC and fuzzing techniques. We evaluate the application of EBF verification framework on a case study, i.e., the S-MQTT protocol, to check security vulnerabilities in cryptographic protocols for IoT.