Finding broken Linux configuration specifications by statically analyzing the Kconfig language
Finding broken Linux configuration specifications by statically analyzing the Kconfig language
复制标题
通过静态分析 Kconfig 语言来查找损坏的 Linux 配置规范
DOI：
10.1145/3468264.3468578
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Gazzillo, Paul
中科院分区：
文献类型：
--
作者：
Oh, Jeho;Yıldıran, Necip Fazıl;Braha, Julian;Gazzillo, Paul
高度可配置的软件支撑着我们的大部分计算基础设施。它可以实现广泛的重用，但也为破坏配置规范打开了大门。配置规范语言 Kconfig 旨在防止构建 Linux 内核的无效配置。然而，Linux 配置空间的巨大规模使得通过手动或随机测试来查找规范错误变得困难。在本文中，我们介绍了一个用于构建 Kconfig 静态分析工具的软件模型检查框架。我们开发了 Kconfig 语言的形式语义，并在名为 kclause 的符号求值器中实现了该语义，该符号求值器将 Kconfig 行为建模为逻辑公式。然后，我们设计并实现了一个名为 kismet 的错误查找器，它采用 kclause 模型并利用自动定理证明来查找未满足的依赖项错误。 kismet 的评估是针对最新版本的 Linux 的精度、性能和对内核开发的影响，该版本在 28 个特定于架构的规范中拥有超过 140,000 行 Kconfig。我们的评估以 100% 的精度发现了 781 个错误（考虑在 Kconfig 规范之间共享时为 151 个），每个 Kconfig 规范花费了 37 到 90 分钟，尽管由于不够近似而遗漏了一些错误。与随机测试相比，kismet 在很短的时间内发现了更多真正的阳性错误。
Highly-configurable software underpins much of our computing infrastructure. It enables extensive reuse, but opens the door to broken configuration specifications. The configuration specification language, Kconfig, is designed to prevent invalid configurations of the Linux kernel from being built. However, the astronomical size of the configuration space for Linux makes finding specification bugs difficult by hand or with random testing. In this paper, we introduce a software model checking framework for building Kconfig static analysis tools. We develop a formal semantics of the Kconfig language and implement the semantics in a symbolic evaluator called kclause that models Kconfig behavior as logical formulas. We then design and implement a bug finder, called kismet, that takes kclause models and leverages automated theorem proving to find unmet dependency bugs. kismet is evaluated for its precision, performance, and impact on kernel development for a recent version of Linux, which has over 140,000 lines of Kconfig across 28 architecture-specific specifications. Our evaluation finds 781 bugs (151 when considering sharing among Kconfig specifications) with 100% precision, spending between 37 and 90 minutes for each Kconfig specification, although it misses some bugs due to underapproximation. Compared to random testing, kismet finds substantially more true positive bugs in a fraction of the time.
登录
查看更多内容
分析Kconfig语义及其分析工具
DOI：
--
发表时间：
2015
期刊：
International Conference on Generative Programming: Concepts and Experiences
影响因子：
--
作者：
Sascha El;Adam Krafczyk;Klaus Schmid
通讯作者：
Klaus Schmid
Tortoise：交互式系统配置修复
DOI：
10.1109/ase.2017.8115673
发表时间：
2017
期刊：
Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE
影响因子：
--
作者：
Weiss, Aaron;Guha, Arjun;Brun, Yuriy
通讯作者：
Brun, Yuriy
挖掘 Kbuild 以检测 Linux 中的变异异常
DOI：
--
发表时间：
2012
期刊：
European Conference on Software Maintenance and Reengineering
影响因子：
--
作者：
Sarah Nadi;R. Holt
通讯作者：
R. Holt
影响因子：
4.4
作者：
Von Rhein, Alexander;Liebig, Joerg;Apel, Sven
通讯作者：
Apel, Sven
DOI：
10.1145/2491411.2491437
发表时间：
2013-08
期刊：
--
影响因子：
--
作者：
Jörg Liebig;Alexander von Rhein;Christian Kästner;S. Apel;Jens Dörre;C. Lengauer
通讯作者：
Jörg Liebig;Alexander von Rhein;Christian Kästner;S. Apel;Jens Dörre;C. Lengauer