Analysis of EDHOC Implementations Using Protocol State Fuzzing

Abstract

The last decade an increasing number of devices have come to light that belong to the ecosystem of Internet of Things (IoT). These devices have the ability to connect to the internet and exchange data mainly using embedded sensors. The environment that those devices operate in are usually limited in resources and bandwidth, which is a fact that also restricts the security that they provide. In order to address this problem a lot of new network and security protocols have been proposed and standardized, targeting such devices operating in constrained environments. Among them is the EDHOC protocol, which is a lightweight key exchange protocol ideal for constrained environments. Not only the protocols should be well designed in theory, but also in practice. The implementations of the protocols ought to be precise, robust and should comply with their specifications. The main subject of this thesis is the analysis of the implementations of the EDHOC protocol. One of the many available ways to analyze such implementations is to first generate a close approximation of the implementations’ underlying state machine model and then inspect the resulting model or use it for model-based testing. This thesis presents EDHOC-Fuzzer, which is a tool capable of learning such state machine models using the technique of protocol state fuzzing. This technique has been already successfully applied to many other protocols. In this thesis several EDHOC implementations were put under learning and their learned models have been analyzed thoroughly. Their analysis provides insights in the way that the implementation behaves and can uncover some well-hidden logical flaws that can lead to minor bugs or even security vulnerabilities. This showcases not only the effectiveness of the techniques used to analyze these implementations, but also the impact that such tools can have, when they are added in the toolbox of people implementing such protocols.