Equivalence checking of BusyBox and util-linux umount(8) -O option handling

git clone


2023-03-07 Reference v2 of my BusyBox patch Sören Tempel
2023-03-03 util-linux: Add license header Sören Tempel
2023-03-03 Reference util-linux bug Sören Tempel
2023-03-03 Update amount of execution paths for new code Sören Tempel
2023-03-02 Implement handling of the '+' prefix in BusyBox Sören Tempel

Clone the repository to access all 23 commits.


This repository contains files to perform equivalence testing of the -O option implementation for umount(8) shipped with BusyBox and util-linux.


The -O option provided by umount(8) unmounts file systems by mount options. This is implemented by checking the mount options of a file system against a provided pattern. The function which performs this comparison is called mnt_match_options() in util-linux. Vanilla BusyBox does not provide this feature but I have written a patch which adds this feature to Busybox. The corresponding function is called fsopts_matches in my patch. This is an attempt to check if my BusyBox implementation of this feature is “correct”. This setup has found one undefined behavior bug in util-linux and two functional errors in my BusyBox patch.


The setup provided here uses symbolic execution with KLEE to ensure that both implementations always return the same value for the same input strings via assert(3):

assert(mnt_match_options(options, pattern) == fsopts_matches(options, pattern));

This is a well-known idea which is already mentioned in the original KLEE paper (Section 5.5). For two 8 byte inputs KLEE finds 485846 execution paths for this assertion under the constraints mentioned below. On all of these execution paths the assertion holds.


This repository uses the KLEE Docker image, to use this image run:

$ docker build -t klee-umount .
$ docker run -it klee-umount

Within the container run the following commands:

$ cd umount
$ make sim

This will execute the code with KLEE.