Exploring the Potential of Frama-C in IoT Static Analysis
Minh Le Kim Tran, William King, Harvey P. Siy · 2023
In this research, we investigated the feasibility of using static analysis for IoT applications with Frama-C. We looked at different kinds of possible IoT vulnerabilities and how static analysis specifically could be used to identify them. With certain Frama-C plugins such as Eva, we were able to run static analysis on most IoT code without modifying the code itself and catch errors that could potentially be exploited in real-world applications that would have otherwise been missed. Additionally, we created a simple IoT device, by utilizing Raspberry Pi 4 hardware with a set of different SunFounder sensors, and ran our created code for it through Frama-C to find any errors. The static analysis done gave a significant amount of potential vulnerabilities in our code, mostly consisting of integer overflows. We learned how we could use static analysis tools, like Frama-C, as a powerful way to find potential vulnerabilities with minimal changes to code.