Exploring the Potential of Frama-C in IoT Static Analysis

Exploring the Potential of Frama-C in IoT Static Analysis

연구 분야: Strategies

학회: MobiHoc '23: Proceedings of the Twenty-fourth International Symposium on Theory, Algorithmic Foundations, and Protocol Design for Mobile Networks and Mobile Computing

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.