Internet of Things (IoT) consists of a large number of devices connected
through a network, which exchange a high volume of data, thereby posing new
security, privacy, and trust issues. One way to address these issues is
ensuring data confidentiality using 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. Here we propose a new verification approach named
Encryption-BMC and Fuzzing (EBF), which combines Bounded Model Checking (BMC)
and Fuzzing techniques to check for security vulnerabilities that arise from
concurrent implementations of cyrptographic protocols, which include data race,
thread leak, arithmetic overflow, and memory safety. EBF models IoT protocols
as a client and server using POSIX threads, thereby simulating both entities’
communication. It also employs static and dynamic verification to cover the
system’s state-space exhaustively. We evaluate EBF against three benchmarks.
First, we use the concurrency benchmark from SV-COMP and show that it
outperforms other state-of-the-art tools such as ESBMC, AFL, Lazy-CSeq, and
TSAN with respect to bug finding. Second, we evaluate an open-source
implementation called WolfMQTT. It is an MQTT client implementation that uses
the WolfSSL library. We show that tool detects a data race bug, which other
approaches are unable to find. Third, to show the effectiveness of EBF, we
replicate some known vulnerabilities in OpenSSL and CyaSSL (lately WolfSSL)
libraries. EBF can detect the bugs in minimum time.

By admin