Finding Unmet Dependencies in Kconfig with the Kismet Static Analyzer

This course explains how Kismet analyzes Linux Kconfig for unmet dependency bugs. It models Kconfig in symbol logic, checks select statements, and evaluates the analyzer’s precision, recall, and performance.

Syllabus

linux works on lots of devices
the kernel is ultra-configurable
configurability makes maintenance harder
there's about 15,000 configuration options
written in about 150,000 lines of Kconfig
what does the build system do?
our goal: automatically analyze the build system
today's focus: Kconfig's unmet dependency bugs
kconfig language example
the unmet dependency bug
an unmet dependency bug in the wild
we first model Kconfig in symbol logic
we check every select for an unmet dependency
experimental setup
precision (true positives)
recall (false negatives)
performance
impact
student members of project team
conclusion