Verifying Software Vulnerabilities in IoT Cryptographic Protocols
This work addresses security risks in IoT networks, which is critical for protecting user privacy, but it is incremental as it builds on existing verification techniques.
The authors tackled the problem of detecting security vulnerabilities in IoT cryptographic protocols by developing the EBF framework, which combines bounded model checking and fuzzing, and applied it to the S-MQTT protocol to identify flaws.
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.