commits

Clone the repository to access all 34 commits.

• .gitignore
• Makefile
• README.md
• busybox.h
• channels.scm
• main.c
• manifest.scm
• util-linux.h

umount-test-opts

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

Background

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 that performs this comparison is called mnt_match_options() in util-linux. Vanilla BusyBox does not provide this feature, but I have written a patch that 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.

Setup

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 an assertion in the test harness:

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

This is a well-known idea that is already mentioned in the original KLEE paper (Section 5.5). For two 7 byte inputs, KLEE finds 70119 execution paths for this assertion under the constraints mentioned below. On all of these execution paths, the assertion holds. On an AMD Ryzen 5700, this takes around 4 minutes.

Usage

Ideally, use this repository with Guix:

$ guix time-machine -C channels.scm -- shell

Within the Guix shell run the following commands:

$ make sim

Alternatively, you can also try to use KLEE’s Docker image:

$ docker run --rm -it klee/klee -v "$(pwd):/code"

Within the container run:

$ cd /code
$ make sim

Limitations

• The equivalence checked is only performed for fixed-size strings of length N.
• Support for key=value mount options is not implemented in BusyBox, hence the input is constrained to [-,+A-Za-z].
• The inputs always have a length of INPUT_SIZE since the aforementioned constraint does not include null terminators.