一句话：为 Kconfig 建立形式语义与符号求值器 kclause，并以此构建静态缺陷查找器 kismet，发现 Linux 内核配置规范中的依赖错误。
Linux 内核等高度可配置软件依赖 Kconfig 规范来避免构建出非法配置，但其配置空间浩瀚，人工与随机测试难以发现规格缺陷。本文提出用于构建 Kconfig 静态分析工具的软件模型检测框架：给出 Kconfig 语言的形式语义，并在符号求值器 kclause 中实现，将 Kconfig 行为建模为逻辑公式；再实现缺陷查找器 kismet，借助自动定理证明找出未满足依赖的缺陷。在近期 Linux 版本（28 份架构相关规范、逾 14 万行 Kconfig）上的评估显示：共发现 781 个缺陷（去重后 151 个），精度 100%，每份规范耗时 37–90 分钟；虽因欠近似漏报部分缺陷，但比随机测试用更少时间找到更多真阳性。
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.
DOI 原文 ·
@inproceedings{paperbot6395,
title = {Finding broken Linux configuration specifications by statically analyzing the Kconfig language},
author = {Jeho Oh and Necip Fazıl Yıldıran and Julian Braha and Paul Gazzillo},
booktitle = {FSE},
year = {2021},
doi = {10.1145/3468264.3468578}
}