In this paper, we describe DiOS, a lightweight model operating system which can be used to execute programs that make use of POSIX APIs. Such executions are fully reproducible: running the same program with the same inputs twice will result in two exactly identical instruction traces, even if the program uses threads for parallelism.
DiOS is implemented almost entirely in portable C and C++: although its primary platform is DiVM, a verification-oriented virtual machine, it can be configured to also run in KLEE, a symbolic executor. Finally, it can be compiled into machine code to serve as a user-mode kernel.
Additionally, DiOS is modular and extensible. Its various components can be combined to match both the capabilities of the underlying platform and to provide services required by a particular program. New components can be added to cover additional system calls or APIs.
The experimental evaluation has two parts. DiOS is first evaluated as a component of a program verification platform based on DiVM. In the second part, we consider its portability and modularity by combining it with the symbolic executor KLEE.
Source Code
The tagged and annotated test programs mentioned in Section 7 of the paper are available here: test.tar.gz. For execution in KLEE, we compiled the test programs approximately this way (the exact executable instructions are part of test.tar.gz, in file test/lib/verify):
divine cc -o klee-pre.bc "$name" /dios/lib/config/seq.bc \
-C,-ldios,-lc++abi,-lc,-ldios_klee
lart klee-pre.bc klee.bc functionmeta fuse-ctors
klee -disable-verify -entry-point=klee_boot -exit-on-error -output-dir=_klee_out \
-check-overshift=false klee.bcThe process for native execution is more complex:
divine cc -c $std $ccopt $1
threads="interrupt-mem:__dios_reschedule interrupt-cfl:__dios_suspend"
lart *.bc native-pre.bc fuse-ctors lowering recurse-annotations $threads 2> /dev/null
divine cc -o native.bc native-pre.bc /dios/lib/config/native.bc \
-C,-ldios,-lrst,-lc++abi,-lc,-ldios_native
lart native.bc native-post.bc functionmeta 2> /dev/null
shift
RTDIR="$BINDIR/../toolchain/"
UNWDIR=$RTDIR/dios/libunwind/src
CXXDIR=$RTDIR/lib
LDFLAGS="-L$UNWDIR -Wl,-rpath,$UNWDIR -L$CXXDIR -Wl,-rpath,$CXXDIR"
clang -fPIC -o libnative-rt.o -c -x c - <<EOF
#include <sys/mman.h>
#include <string.h>
#include <stdlib.h>
#include <unistd.h>
void __dios_native_exit( int x )
{
_exit( x );
}
int __dios_native_rand()
{
return rand();
}
void *__dios_native_mmap( void *addr, size_t len, int prot, int flags, int fd, off_t off )
{
return mmap( addr, len, prot, flags, fd, off );
}
void __dios_native_puts( const char *x )
{
write( 1, x, strlen( x ) );
write( 1, "\n", 1 );
}
EOF
ld -static -r -s -o libnative-rt-partial.o libnative-rt.o /usr/lib/x86_64-linux-musl/libc.a
cat <<EOF > native.script
{
global:
__dios_native_exit;
__dios_native_puts;
__dios_native_mmap;
__dios_native_rand;
local:
EOF
nm libnative-rt-partial.o | grep -v __dios_native | cut -d' ' -f3 | \
grep '[a-z]' | sed -e 's,$,;,' >> native.script
echo '};' >> native.script
clang -shared -o libnative-rt.so -Wl,--version-script=native.script,-z,muldefs \
libnative-rt-partial.o
clang -Wl,-e,__dios_native_boot,-rpath,. native-post.bc libnative-rt.so \
$LDFLAGS -lc++abi -lunwind
./a.outThe source code of DiOS itself can be found in dios.tar.gz. Please note that neither of the tarballs are standalone, and are mainly useful for inspection. To execute the automated build and testcases, we suggest that you download divine-4.4.2+dios.tar.gz and run make. To be able to run the testcases with KLEE, you will need to build a patched version of KLEE: (klee-2.0+dios.tar.gz) and put the resulting klee binary on your path.
To run the testsuite, you can issue make functional (alternatively, make functional F=klee will only run testcases using klee).