Tools for working with symbolic constraints from Kbuild Makefile.
Project description
The kmax tool suite
Getting started
Installing the kmax tool suite
Install using pipx.
sudo apt install -y pipx
pipx install kmax
Instructions to install from source can be found in the advanced documentation.
Installing SuperC (recommended)
SuperC allows klocalizer
to find #ifdef
constraints.
# install superc
sudo apt-get install -y libz3-java libjson-java sat4j unzip flex bison bc libssl-dev libelf-dev xz-utils lftp
wget -O - https://raw.githubusercontent.com/appleseedlab/superc/master/scripts/install.sh | bash
# setup environment
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}
Add the environment variables to your .bash_profile
to make them permanent.
Kicking the tires
Install Linux kernel compilation dependencies:
sudo apt install -y flex bison bc libssl-dev libelf-dev
Get the Linux kernel source:
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/
Test klocalizer
by automatically repair allnoconfig
to build drivers/usb/storage/alauda.o
, which would normally be omitted by allnoconfig
.
# create allnoconfig
make ARCH=x86_64 allnoconfig
# run klocalizer to 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 klocalizer --repair
on patches
klocalizer
will take config file that fails to build lines of a patch and repairs it to build the whole patch. This requires installing SuperC as described above.
Let's first get an example patch from the Linux kernel's mainline repository:
cd ~/
git clone git://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
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 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 (optionally build the whole kernel)
KCONFIG_CONFIG=0-x86_64.config make 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 --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 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 asNUM-ARCH.config
.
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.
Using koverage
koverage
checks whether a Linux configuration file includes a set of source file:line pairs for compilation. This following checks whether lines 256 and 261 of kernel/fork.c
are included for compilation by Linux v5.16 allyesconfig.
cd ~/linux-5.16/
make.cross ARCH=x86_64 allyesconfig
koverage --config .config --arch x86_64 --check kernel/fork.c:[259,261] -o coverage_results.json
make allnoconfig; klocalizer -v --repair .config --include kernel/fork.c:[259]; rm -rf koverage_files/; koverage -v -a x86_64 --config .config --check kernel/fork.c:[259] -o coverage.out
The coverage results are in coverage_results.json
, which indicate that line 259 is included while 261 is excluded by allyesconfig, because the lines are under mutually-exclusive #ifdef
branches.
Use --check-patch file.patch
to check coverage of all source lines affected by a given patch.
Using kismet
This tool will check for unmet dependency bugs in Kconfig specifications due to reverse dependencies overriding direct dependencies.
Run kismet
on the root of the Linux source tree.
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:
- A summary of the results in
kismet_summary_x86_64.txt
- A list of results for each
select
construct inkismet_summary_x86_64.csv
(UNMET_ALARM
denotes the buggy ones) - A list of
.config
files meant to exercise each bug inkismet-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.
Additional documentation
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.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.