2020/01/27 by Fatimah Aljaafari, Aljaafari, Fatimah, Lucas C. Cordeiro +4
Computer Science · #Advanced Malware Detection Techniques #Cryptographic Implementations and Security #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Security and Verification in Computing #Software Engineering (cs.SE) #cs.CR #cs.SE
paper · pdf · doi:10.48550/arxiv.2001.09837
arxiv created 2020/01/27 · openalex publication_date 2020/01/27 · arxiv updated 2020/01/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.