Automatic abstraction is a powerful software verification technique. In this paper, we elaborate an abstract domain for C strings, that is, null-terminated arrays of characters. The domain we present (called M-String) is parametrized on an index (bound) domain and a character domain. Picking different constituent domains, i.e., both shape information on the array structure and value information on the contained characters, allows M-String to be tailored for specific verification tasks, balancing precision against complexity. We describe the concrete and the abstract semantics of basic string operations and prove their soundness formally. In addition to a selection of string functions from the standard C library, we provide semantics for character access and update, enabling automatic lifting of arbitrary string-manipulating code into the domain.
In addition to describing the domain theoretically, we also provide an executable implementation of the abstract operations. Using a tool which automatically lifts existing programs into the M-String domain along with an explicit-state model checker, we evaluate the accuracy of the proposed domain experimentally on real-case test programs.
Installation
DIVINE should work on any reasonably recent Linux distribution. It might also be possible to make it work on macOS, *BSD or even on Windows using Windows Subsystem for Linux, but this is not tested routinely.
Binary Distribution
The binary distribution is intended for Ubuntu 18.04. However, as a binary distribution, it might not work on other Linux distributions or even on Ubuntu due to updates.
To use it, it is sufficient to extract the archive. Then run ./divine help in the main archive directory. If this succeeds (gives you a list of commands), you should be good to go with the binary distribution, if not, you should build DIVINE from the sources as your system is not compatible with the archive.
Building from Source
To build from the source, you will need some prerequisites, namely a C++11 compiler such as reasonably recent GCC (>= 4.9) or Clang (>= 3.2), make, CMake (>= 3.2), libedit, perl, and about 12GB of disk space and 4GB or RAM. For the symbolic verification to work, you will also need the Z3 solver, including its libraries.
You should extract the archive and then run make divine in its main directory. This should build DIVINE into _build.release/tools subdirectory by default. For more details, please refer to the manual.
Usage
Binary distribution contains a main binary of divine. If you have built DIVINE from the source, the built binary resides in _build.release/tools/divine
To run divine verification with mstring abstraction on source.c use:
divine check --symbolic source.cTo create a symbolic string use functions from divine/dios/include/rst/domains.h. We provide following constructors:
__mstring_from_string( const char * buff )lifts string in the buffer,__mstring_from_segments( uint64_t chars, ... )creates mstring with specified characters in segments, i.e.__mstring_from_segments( 3, 'a', 'b', '\0' ),__mstring_from_random_segments( uint64_t segments )creates mstring with specified number of segments,__mstring_val( unsigned len )creates zeroinitialized mstring of lengthlen.
The implementation of M-String domain is located in attached sources:
divine/dios/include/rst/mstring.hppdivine/dios/rst/mstring.cpp
Benchmarks
Verisec: This set adopted from Ku K., Hart T.E., Chechik M., Lie D.: A buffer overflow benchmark for software model checkers. ASE 2007: 389-392. (source)