Exploring the Potential of Frama-C in IoT Static Analysis
Exploring the Potential of Frama-C in IoT Static Analysis
复制标题
探索 Frama-C 在物联网静态分析中的潜力
DOI：
10.1145/3565287.3617617
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Siy, Harvey
中科院分区：
文献类型：
--
作者：
Tran, Minh Le;King, William;Siy, Harvey
在这项研究中，我们研究了使用Frama-C对物联网应用进行静态分析的可行性。我们研究了不同类型的可能的物联网漏洞，以及如何专门使用静态分析来识别它们。使用某些Frama-C插件（如伊娃），我们能够在不修改代码本身的情况下对大多数物联网代码运行静态分析，并捕获可能在现实世界的应用程序中被利用的错误，否则会被错过。此外，我们创建了一个简单的物联网设备，通过使用Raspberry Pi 4硬件和一组不同的SunFounder传感器，并通过Frama-C运行我们为它创建的代码来查找任何错误。所做的静态分析在我们的代码中发现了大量潜在的漏洞，主要由整数溢出组成。我们学习了如何使用静态分析工具，如Frama-C，作为一种强大的方法来发现潜在的漏洞，对代码进行最小的更改。
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.
对无错误 C 程序的不懈追求
影响因子：
22.7
作者：
P. Baudin;François Bobot;David Bühler;Loïc Correnson;F. Kirchner;N. Kosmatov;A. Maroneze;Valentin Perrelle;Virgile Prevosto;Julien Signoles;Nicky Williams
通讯作者：
Nicky Williams