Finding Unmet Dependencies in Kconfig with the Kismet Static Analyzer
summary
Static analyzer kismet converts Kconfig into boolean formulas via k-clause, feeds them to SAT solvers, and emits test .config files that reproduce failures in the build system. On 28 architectures it flags 151 confirmed unmet-dependency bugs with 100% precision, misses 8 positives compared to ~11 million randconfig trials, and runs per-architecture in ~37–90 minutes (full run under a day, parallelizable). 38 reports were filed and 15 patches merged; ~30% of these bugs trigger build errors.
AI-written summary · about
chapters (20)
- 0:00linux works on lots of devices
- 0:18the kernel is ultra-configurable
- 0:56configurability makes maintenance harder
- 2:33there's about 15,000 configuration options
- 3:35written in about 150,000 lines of Kconfig
- 4:35what does the build system do?
- 5:45our goal: automatically analyze the build system
- 6:13today's focus: Kconfig's unmet dependency bugs
- 7:13kconfig language example
- 8:50the unmet dependency bug
- 9:28an unmet dependency bug in the wild
- 11:33we first model Kconfig in symbol logic
- 13:06we check every select for an unmet dependency
- 15:19experimental setup
- 15:47precision (true positives)
- 16:38recall (false negatives)
- 17:22performance
- 18:13impact
- 23:41student members of project team
- 23:52conclusion
related talks
15mStatic Detection of Silent Misconfigurations with Deep Interaction Analysis
42mBringing Together Configuration Research: Towards a Common Ground
52mBringing Existing Open-Source Code into MISRA Compliance
24mSymbiotic: finding bugs in C programs
23mDeprecating Stuff
23mPrecise and Accurate Patch Presence Test for Binaries
27mCatch Me If You Can: Hunting Misconfigurations Before They...
49mBuild Systems: a Simple Solution to a Complicated Problem