论文标题
在物联网加密协议中验证软件漏洞
Verifying Software Vulnerabilities in IoT Cryptographic Protocols
论文作者
论文摘要
物联网（IoT）是一个由通过网络连接的大量智能设备组成的系统。这些设备的数量正在迅速增加，这创建了一个庞大而复杂的网络，并在该网络上传达了大量数据。在运输中保护这些数据的一种方法，即实现数据机密性，是为物联网协议使用轻巧的加密算法。但是，此类协议的设计和实现是容易出错的任务。实施中的缺陷可能导致毁灭性的安全漏洞。这些漏洞可以由攻击者利用并影响用户的隐私。存在各种技术来验证软件并检测漏洞。有限的模型检查（BMC）和模糊性是检查软件系统有关其规格的正确性的有用技术。在这里，我们描述了一个使用BMC和模糊技术的框架，称为“加密-BMC”和“ fuzzing（EBF）”（EBF）。我们评估了EBF验证框架在案例研究（即S-MQTT协议）上的应用，以检查IoT加密协议中的安全漏洞。
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.
