umount-test-opts - README.md

 1# umount-test-opts
 2
 3This repository contains files to perform equivalence testing of the `-O` option implementation for `umount(8)` shipped with [BusyBox](https://busybox.net/) and [util-linux](https://git.kernel.org/cgit/utils/util-linux/util-linux.git).
 4
 5## Background
 6
 7The `-O` option provided by `umount(8)` unmounts file systems by mount options.
 8This is implemented by checking the mount options of a file system against a provided pattern.
 9The function which performs this comparison is called [`mnt_match_options()`](https://cdn.kernel.org/pub/linux/utils/util-linux/v2.37/libmount-docs/libmount-Options-string.html#mnt-match-options) in util-linux.
10Vanilla BusyBox does not provide this feature but I have written a patch which [adds this feature to Busybox](http://lists.busybox.net/pipermail/busybox/2022-June/089769.html).
11The corresponding function is called `fsopts_matches` in my patch.
12This is an attempt to check if my BusyBox implementation of this feature is "correct".
13This setup has found one [undefined behavior bug in util-linux](https://git.kernel.org/pub/scm/utils/util-linux/util-linux.git/commit/?id=06ee5267516761721ebfbdfa313980cef8e54c66) and two functional errors in [my BusyBox patch](http://lists.busybox.net/pipermail/busybox/2023-March/090193.html).
14
15## Setup
16
17The setup provided here uses [symbolic execution](https://en.wikipedia.org/wiki/Symbolic_execution) with [KLEE](https://klee.github.io) to ensure that both implementations always return the same value for the same input strings via `assert(3)`:
18
19    assert(mnt_match_options(options, pattern) == fsopts_matches(options, pattern));
20
21This is a well-known idea which is already mentioned in the [original KLEE paper](https://www.usenix.org/legacy/events/osdi08/tech/full_papers/cadar/cadar.pdf) (Section 5.5).
22For two 8 byte inputs KLEE finds 485846 execution paths for this assertion under the constraints mentioned below.
23On all of these execution paths the assertion holds.
24
25## Usage
26
27This repository uses the KLEE [Docker](https://www.docker.io/) image, to use this image run:
28
29    $ docker build -t klee-umount .
30    $ docker run -it klee-umount
31
32Within the container run the following commands:
33
34    $ cd umount
35    $ make sim
36
37This will execute the code with KLEE.
38
39## Limitations
40
41* The equivalence checked is only performed for fixed-size strings of length `N`.
42* Support for `key=value` mount options is not implemented in Busybox, hence the input is constrained to `[-,+A-Za-z0-9]`.