In this paper, we describe a novel approach to verification of programs which rely on POSIX APIs for their functioning. We leverage DiVM, an existing verification framework, which provides low-level (machine-like) interfaces. In our approach, we do not extend the verifier with special support for high-level features: instead, we have implemented a small operating system with support for POSIX-compatible threads, processes and filesystem. This operating system then becomes part of the run-time environment of the user program (and from the point of view of the verifier, is part of the system under test).
Additionally, we show that a small set of modular components can be combined to obtain various levels of POSIX API support. This means that DiOS can be configured to only provide features relevant to a particular program, yielding minimal overhead, without losing flexibility and while providing comprehensive API coverage.
- full text (pdf, revision 1, 2018-03-10)
Source code
The source code of DiOS, current as of writing of this paper, is available for download as dios-2018.03.12.tar.gz and is mainly useful for inspection. Building is better accomplished by obtaining a source distribution of DIVINE and evaluation is further simplified by obtaining pre-compiled binaries of DIVINE. For further instructions, see below.
Installation
The evaluation was done with an as-of-yet unreleased version of DIVINE. All relevant changes will be part of version 4.1.2. The version we have used for evaluation can also be downloaded from here: divine-4.1.1+dios.tar.gz. We have also built static binaries for 64-bit Linux (amd64/x86-64) of both divine and divcc. You can simply drop the static binaries on your path and proceed to the next section. If you would prefer to build DIVINE from source, you can follow the instructions in the manual.
Building gzip
To reproduce the build and execution of gzip, you need both divcc and divine. See previous section on how to obtain them.
We have used the upstream source tarball, gzip-1.8.tar.gz. The changes required to build gnulib on DiOS are available here: gzip-1.8-divine.diff. You simply need to unpack the source tarball, apply the patch and use divcc from DIVINE to build the package:
$ wget http://ftp.gnu.org/gnu/gzip/gzip-1.8.tar.gz
$ wget https://divine.fi.muni.cz/2018/dios/gzip-1.8-divine.diff
$ tar xzf gzip-1.8.tar.gz
$ cd gzip-1.8
$ patch -p1 < ../gzip-1.8-divine.diff
$ ./configure CC=divcc
$ make
$ echo hello world | ./gzip - > hello.gz
$ divine check --stdin hello.gz ./gzip -f -d -To see the output from an execution, you can run (in this case, the program flow is deterministic, so there is little difference between execution and model checking):
$ divine exec --virtual -o nofail:malloc --stdin hello.gz ./gzip -f -d -