Analysis of crypto module in RIOT OS using Frama-C

With the growing advances in Internet of Things (IoT) technology, it has become an indispensable part of many areas like home automation, industries, medical equipment, etc. Thus, the security of the IoT hardware and software is of utmost importance. The availability of secure IoT software components allows for better confidence in the use of IoT devices for consumers. IoT operating systems are core software components of the IoT ecosystem. There are a lot of IoT operating systems (OSes) available, but Real-time Operating System for IoT (RIOT) is one of the most commonly used open-source OS used by universities and businesses. As the RIOT source code is written in C, it inherently has some security vulnerabilities. With IoT devices having the characteristic of limited battery and computational capability, it is very challenging to detect cyber-attacks online. This would necessitate more rigorous security checks being performed on the device prior to deployment. For the security of the RIOT OS, the analysis techniques used in highly critical domains can also be applied to IoT software. Thus, the purpose of this work is to apply techniques such as formal verification to the crypto module of RIOT using a software analysis platform for C code, namely Frama-C in order to analyze the security aspects of the module.