|2023-03-07||README.md: 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.
-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(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.
- The equivalence checked is only performed for fixed-size strings of length
- Support for
key=valuemount options is not implemented in Busybox, hence the input is constrained to