kmax 4.8

Tools for working with symbolic constraints from Kbuild Makefile.

• The kmax tool suite
  • Installation
    • Dependencies
    • Installing the kmax tool suite
    • Quick test
  • Using krepair on patches
    • The paper example
  • Using kismet
    • Checking a single select construct
    • Checking all Kconfig files for an architecture
  • Using klocalizer --save-dimacs and klocalizer --save-smt
  • Additional documentation
  • Bugs found
  • Credits

The kmax tool suite

Installation

Dependencies

System dependencies

# kmax dependencies
sudo apt install -y pipx python3-dev gcc build-essential
# linux dependencies
sudo apt install -y flex bison bc libssl-dev libelf-dev git
# superc dependencies
sudo apt install -y wget libz3-java libjson-java sat4j unzip xz-utils lftp

User dependencies

# install superc and make.cross
wget -O - https://raw.githubusercontent.com/appleseedlab/superc/master/scripts/install.sh | bash

Environment

Add these environment variables to your shell, e.g., .bash_profile:

export COMPILER_INSTALL_PATH=$HOME/0day
export CLASSPATH=/usr/share/java/org.sat4j.core.jar:/usr/share/java/json-lib.jar:${HOME}/.local/share/superc/z3-4.8.12-x64-glibc-2.31/bin/com.microsoft.z3.jar:${HOME}/.local/share/superc/JavaBDD/javabdd-1.0b2.jar:${HOME}/.local/share/superc/xtc.jar:${HOME}/.local/share/superc/superc.jar:${CLASSPATH}
export PATH=${HOME}/.local/bin/:${PATH}

Installing the kmax tool suite

pipx install kmax

Quick test

Get Linux kernel source:

cd ~/
wget https://cdn.kernel.org/pub/linux/kernel/v6.x/linux-6.10.tar.xz
tar -xvf linux-6.10.tar.xz
cd ~/linux-6.10/

Test krepair by automatically repairing allnoconfig to include drivers/usb/storage/alauda.o, which would normally be omitted by allnoconfig.

# create allnoconfig
make ARCH=x86_64 allnoconfig
# run klocalizer --repair allnoconfig to build alauda.c
klocalizer --repair .config -o allnoconfig_repaired --include drivers/usb/storage/alauda.o
# clean and build the kernel with the repair config file
KCONFIG_CONFIG=allnoconfig_repaired make ARCH=x86_64 olddefconfig clean drivers/usb/storage/alauda.o

You should see CC drivers/usb/storage/alauda.o at the end of the build.

Using krepair on patches

klocalizer --repair will take a config file that fails to build lines of a patch and repairs it to build the whole patch. This uses SuperC to find #ifdef constraints.

Let's first get the Linux source code:

cd ~/
git clone git://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git

Now let's get an example patch from the Linux kernel's mainline repository:

cd ~/linux/
git checkout 6fc88c354f3af
git show > 6fc88c354f3af.diff

Next, let's repair allnoconfig, which does not build all lines from the patch.

# create allnoconfig
make.cross ARCH=x86_64 allnoconfig
# run klocalizer to repair allnoconfig to include the patch
klocalizer --repair .config -a x86_64 --include-mutex 6fc88c354f3af.diff
# clean and build the files modified by the patch (WERROR=0 for tools/lib/subcmd/subcmd-util.h which triggers a use-after-free on gcc 13)
KCONFIG_CONFIG=0-x86_64.config make.cross WERROR=0 ARCH=x86_64 olddefconfig clean kernel/bpf/cgroup.o net/ipv4/af_inet.o net/ipv4/udp.o net/ipv6/af_inet6.o net/ipv6/udp.o

We can use koverage to check how much of patch is covered by a given config file:

koverage -f --config 0-x86_64.config --arch x86_64 --check-patch 6fc88c354f3af.diff -o coverage_results.json
cat coverage_results.json

In contrast, we can see that allnoconfig omits coverage of the patch:

make.cross ARCH=x86_64 allnoconfig
koverage -f --config .config --arch x86_64 --check-patch 6fc88c354f3af.diff -o allnoconfig_coverage_results.json
cat allnoconfig_coverage_results.json

Notes:

• While repair usually covers all lines of a patch, some lines may still be omitted, for instance if they are dead code or in header files.
• If a patch modifies both arms of an #ifdef, multiple config files are needed to cover all lines. These are exported as NUM-ARCH.config.

The paper example

Here is another example from the krepair paper. This patch modifies code in both arms of an #ifdef, so a single .config file cannot cover all patched lines. klocalizer emits two .config files, which together cover all lines.

git checkout 8594c3b85171b
git show > 8594c3b85171b.diff
make.cross ARCH=arm allnoconfig
klocalizer --repair .config -a arm --include-mutex 8594c3b85171b.diff
koverage -f --config 0-arm.config --arch arm --check-patch 8594c3b85171b.diff -o 0-coverage_results.json
koverage -f --config 1-arm.config --arch arm --check-patch 8594c3b85171b.diff -o 1-coverage_results.json
cat 0-coverage_results.json
cat 1-coverage_results.json
diff -y 0-coverage_results.json 1-coverage_results.json | less

Using kismet

This tool will check for unmet dependency bugs in Kconfig specifications due to reverse dependencies overriding direct dependencies.

Checking a single select construct

Found by Intel's kernel test robot running kismet

git checkout 5a7f27a624d9e33262767b328aa7a4baf7846c14
kismet --linux-ksrc=./ --selectees CONFIG_SND_SOC_MAX98357A --selectors CONFIG_SND_SOC_INTEL_SOF_CS42L42_MACH -a=x86_64

The alarm can be found in kismet_summary_x86_64.csv and .config files that exercise the bug can be found in kismet-test-cases/.

Checking all Kconfig files for an architecture

Run kismet on the root of the Linux source tree.

cd ~/
wget https://cdn.kernel.org/pub/linux/kernel/v5.x/linux-5.16.tar.xz
tar -xvf linux-5.16.tar.xz
cd ~/linux-5.16/
kismet --linux-ksrc="${HOME}/linux-5.16/" -a=x86_64

Once finished (it can take about an hour on a commodity desktop), kismet will produce three outputs:

1. A summary of the results in kismet_summary_x86_64.txt
2. A list of results for each select construct in kismet_summary_x86_64.csv (UNMET_ALARM denotes the buggy ones)
3. A list of .config files meant to exercise each bug in kismet-test-cases/

Technical details can be found in in the kismet documentation and the publication on kclause and kismet. The experiment replication script can be used to run kismet on all architectures' Kconfig specifications.

Using klocalizer --save-dimacs and klocalizer --save-smt

This tool extracts a DIMACS or a SMT formula. Therefore, execute the following commands in the root directory of your Linux kernel:

klocalizer -a x86_64 --save-dimacs <Path>
klocalizer -a x86_64 --save-smt <Path>

Note that <Path> should be replaced by the absolute path to the file, the formulae should be written to. If you intend to use a Docker container, feel free to use the Dockerfile provided in Advanced Usage.

Additional documentation

Advanced Usage

Bugs found

Bugs Found by our tools

Credits

The main developers of this project have been Paul Gazzillo (kextract, kclause, kmax, klocalizer), Necip Yildiran (kismet, krepair, koverage), Jeho Oh (kclause), and Julian Braha (koverage). Julia Lawall has posed new applications and provided invaluable advice, feedback, and support. Thanks to all the users who have contributed code and issues. Special thanks to the Intel 0-day team for working to include kismet into the kernel test robot and for their valuable feedback. This work is funded in part by the National Science Foundation under awards CCF-1840934 and CCF-1941816.