Linux 内核模块和设备驱动程序的静态分析工具答案

【问题标题】：Static Analysis tool for Linux kernel modules and device driversLinux 内核模块和设备驱动程序的静态分析工具
【发布时间】：2012-12-07 16:42:10
【问题描述】：

我需要一个静态分析工具，用于我为基于 ARM 的开发板编写的 Linux 设备驱动程序。我正在考虑以下几种工具：

Sparse 是一种计算机软件工具，已在 Linux 上可用，旨在发现 Linux 内核中可能存在的编码错误。
Linux Verification Center 有两个活跃的项目旨在提高可加载内核模块的质量。
- Linux Driver Verification (LDV) - 用于对 Linux 设备驱动程序进行静态源代码验证的综合工具集。
- KEDR Framework - 用于动态分析和验证内核模块的可扩展框架。
- 另一个正在进行的项目是Linux File System Verification，旨在开发一个专用工具集来验证 Linux 文件系统实现。
在GCC 上启用-Werror、-Wextra 和-Wall，并使用Valgrind 运行。

上次我玩 Sparse 时，我发现输出令人困惑，并且没有找到好的文档来解释输出。有没有人有关于稀疏工具的好文档？我可以使用哪些其他免费静态分析工具来验证我的 Linux 驱动程序？我知道 LINT 工具，但它已获得许可。

【问题讨论】：

试试夹板。这是免费的。另一个建议是使用 -Wall 和 -Wextra 进行编译。
夹板用于普通 C 代码。我需要一个可以检查 linux 内核代码的工具。一个常见的例子是在原子上下文中使用可能休眠（或者通常可能导致重新调度）的函数，即在中断处理程序中，在由自旋锁等保护的关键部分中。
听起来你在这里混合了很多不同的概念。 Linux 内核是用 C 编写的，因此 splint 是一个有效的静态分析工具。
是的，LDV 是一个非常强大的静态分析系统，到目前为止，它已经发现了内核中的许多 bug。他们还有一个验证器 (linuxtesting.org/ldv/online) 的 Web 界面，您可以使用它来上传和检查您的驱动程序。不确定他们现在如何处理 ARM 细节，但无论如何 - 值得一试。
Linux验证中心另外两个项目中构建的工具，都是动态分析系统，而不是你需要的静态分析工具。 KEDR 框架目前仅适用于 x86。作为 KEDR 的主要开发人员之一，很遗憾，到目前为止，我还没有时间将其移植到 ARM。明年，我希望能够做到这一点。 Linux File System Verification 项目中开发的 Spruce 系统在一定程度上也依赖于 KEDR。

【解决方案1】：

Smatch 是用于内核的 C 静态分析工具。它产生了数百个补丁。不少与安全相关或对稳定内核来说足够重要。

【讨论】：

【解决方案2】：

如果你想编写自己的规则，Coccinelle 可能是合适的。如果您想使用其他人编写的规则，您可以使用集成到内核中的各种工具。查看第 4.2 节：文档/开发流程/4.Coding 的代码检查工具以获取一些建议。

【讨论】：