Open Source Summit + Embedded Linux Conference + OSPOCon 2021

Linux developers specify legal uses of configuration options in the Kconfig language. With over 140,000 lines of Kconfig specifications in the Linux kernel, its complex behavior makes maintenance challenging. A common pitfall, highlighted in Kconfig’s manual, is the unmet dependency bug, which happens when an option’s reverse dependencies override its direct dependencies. Unmet dependencies allow an invalid kernel configuration to slip by Kconfig and potentially break the build. This talk introduces a static analysis tool, called kismet, that uses automated logical reasoning checks to check for unmet dependencies in a Kconfig specification database. The talk covers the technical details of the analyzer as well an evaluation showing that kismet finds 781 unmet dependencies (151 when considering sharing among each architecture's Kconfig specifications) for one recent version of the Linux source code, although it misses some due to limitations in handling string and number configuration options. All found unmet dependency bugs have been validated by automatically creating a .config file that triggers it. kismet takes between 37 and 90 minutes for each architecture's Kconfig specification, for a total of about 20 hours for all 28 architecture's Kconfig specifications.