commits

Clone the repository to access all 23 commits.

• .gitignore
• Dockerfile
• Makefile
• README.md
• busybox.h
• main.c
• 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 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.

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 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.

Usage

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.

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-z0-9].