In this paper, we describe a novel approach for adapting an existing software model checker to perform precise runtime verification, by allowing the software under test to communicate with the wider environment (including file system and network access). The modifications to the model checker are small and self-contained, making this a viable strategy for re-using existing model checking tools in a new context.
Additionally, from the data that is gathered during a single execution in the runtime verification mode, we automatically re-construct a description of the execution environment which can then be used in the standard, full-blown model checker. This additional verification step can further improve coverage, especially in the case of parallel programs, without introducing substantial overhead into the process of runtime verification.
- full text (pdf, revision 1, 2017-05-12)
Source Code
The prototype implementation can be obtained as a source tarball, comprising a modified distribution of DIVINE 4: divine-4.0.5+passthrough.tar.gz.
TBD
Using the Prototype
The programs reproduced below, as well as a number of test cases bundled in the source tarball, can be tested with our prototype implementation. Assuming that you have downloaded, built and installed the modified version of DIVINE 4 (see above), you can execute following commands to verify a given program:
$ divine run -o configuration:passthrough -o nofail:malloc program.cThis does two things: it executes the program in passthrough mode (under the assumption that malloc does not fail) and stores a syscall trace of the execution in a file named passthrough.out. In turn, it is possible to re-use this trace in a replay mode by issuing the command:
$ divine run -o configuration:replay -o nofail:malloc program.cThis simply re-runs the program, which is not very interesting in itself. However, while passthrough can only be used with divine run, the replay mode can be used with all the tools DIVINE offers, including sim and verify:
$ divine verify -o configuration:replay -o nofail:malloc program.cIt is also possible to visualise the state space generated in the replay mode, illustrating that for parallel programs, there are many new interleavings (the execution in run is always a non-branching sequence of states; this can be seen with, for example, the rw-par.c program below):
$ divine draw -o configuration:replay -o nofail:malloc rw-par.cEvaluation Programs
The evaluation section of the paper refers to four C programs that were used to validate our approach. The programs are reproduced here. First is rw.c which simply demonstrates the ability to read and write files in the real operating system.
#include <unistd.h>
#include <assert.h>
#include <string.h>
#include <fcntl.h>
int main() {
char buf[8] = {};
int fd = open( "file47", O_WRONLY | O_CREAT, 0644 );
assert( fd >= 0 );
assert( write( fd, "tralala", 7 ) == 7 );
assert( close( fd ) == 0 );
fd = open( "file47", O_RDONLY );
assert( fd >= 0 );
int res = read( fd, buf, 7 );
assert( res == 7 );
assert( strcmp( "tralala", buf) == 0 );
assert( close( fd ) == 0 );
return 0;
}[download]
The second program, then, demonstrates input/output (going through the host operating system) in a parallel application. Due to limitations of the prototype implementation (as outlined in Section 6.5 of the paper), the example uses non-blocking IO.
#include <pthread.h>
#include <unistd.h>
#include <assert.h>
#include <string.h>
#include <fcntl.h>
#include <sys/stat.h>
const char *message = "1234567";
void *worker( void *_ ) {
(void)_;
int fd = open( "pipe", O_WRONLY );
assert( fd >= 0 );
assert( write( fd, message, 7 ) == 7 );
assert( write( fd, "-", 1 ) == 1 );
assert( close( fd ) == 0 );
}
int main() {
char buf[ 8 ] = {};
assert( mkfifo( "pipe", 0644 ) == 0 );
int fd = open( "pipe", O_RDONLY | O_NONBLOCK );
pthread_t thread;
pthread_create( &thread, NULL, worker, NULL );
assert( fd >= 0 );
char incoming;
int total = 0;
while ( 1 )
{
int cnt = read( fd, &incoming, 1 );
if ( !cnt )
continue;
assert( cnt == 1 );
if ( incoming == '-' )
break;
buf[ total ] = incoming;
total += cnt;
}
pthread_join( thread, NULL );
assert( strcmp( buf, message ) == 0 );
return 0;
}[download]
The next program is a very simple HTTP client. Due to missing resolver in DIVINE’s libc, it has an IP address hard-coded in the source. Other than that, it uses the standard socket APIs to open a TCP/IP connection, send a request and read the response.
#include <stdio.h>
#include <sys/socket.h>
#include <stdlib.h>
#include <string.h>
#include <unistd.h>
#include <stdint.h>
int construct_socket();
char *get_query(char *host, char *page);
#define HOST "divine.fi.muni.cz"
#define PAGE "/"
#define PORT 0x5000u
#define USERAGENT "HTMLGET 1.0"
// the address of divine.fi.muni.cz
#define ADDR 0xa133fb93
/* declare a few things currently missing from DIVINE's libc */
struct in_addr
{
uint32_t s_addr;
};
struct sockaddr_in
{
short sin_family; // e.g. AF_INET
unsigned short sin_port; // e.g. htons(3490)
struct in_addr sin_addr; // see struct in_addr, below
char sin_zero[8]; // zero this if you want to
};
int main(int argc, char **argv)
{
struct sockaddr_in *remote;
int socket;
int actionResult;
char *query;
char buffer[ BUFSIZ + 1 ];
socket = construct_socket();
remote = (struct sockaddr_in *)malloc( sizeof( struct sockaddr_in ) );
if ( !remote )
return 1;
remote->sin_family = AF_INET;
remote->sin_addr.s_addr = ADDR;
memset( remote->sin_zero, 0, 8 );
remote->sin_port = PORT;
if ( connect( socket, ( struct sockaddr * )remote, sizeof( struct sockaddr ) ) < 0 ) {
perror( "Error: Could not connect" );
exit( 1 );
}
query = get_query( HOST, PAGE );
fprintf( stderr, "Query is:\n<<START>>\n%s<<END>>\n", query );
int sent = 0;
while ( sent < strlen( query ) ) {
actionResult = send( socket, query+sent, strlen( query ) - sent, 0 );
if ( actionResult == -1 ) {
perror( "Error: Can't send query" );
exit( 1 );
}
sent += actionResult;
}
memset( buffer, 0, sizeof( buffer ) );
int htmlStart = 0;
char *htmlContent = NULL;
while( ( actionResult = recv( socket, buffer, BUFSIZ, 0 ) ) > 0 ) {
if ( htmlStart == 0 ) {
htmlContent = strstr( buffer, "\r\n\r\n" );
if ( htmlContent != NULL ) {
htmlStart = 1;
htmlContent += 4;
}
} else
htmlContent = buffer;
if( htmlStart )
fprintf( stdout, "%s", htmlContent );
memset( buffer, 0, actionResult );
}
if ( actionResult < 0 )
perror( "Error: Not receiving data" );
// clean up
free( query );
free( remote );
close( socket );
return 0;
}
int construct_socket()
{
int _socket;
if ( ( _socket = socket( AF_INET, SOCK_STREAM, 6 ) ) < 0 ) {
perror( "Error: Unable to create TCP socket" );
exit( 1 );
}
return _socket;
}
char *get_query(char *host, char *page)
{
char *query;
char *getpage = page;
char *tpl = "GET /%s HTTP/1.0\r\nHost: %s\r\nUser-Agent: %s\r\n\r\n";
if ( getpage[0] == '/' ) {
getpage = getpage + 1;
fprintf( stderr,"Removing leading \"/\", converting %s to %s\n", page, getpage );
}
query = (char *)malloc( strlen( host ) + strlen( getpage )
+ strlen( USERAGENT ) + strlen( tpl ) - 5 );
sprintf( query, tpl, getpage, host, USERAGENT );
return query;
}[download]
Finally, rw-par.c is a program which creates a pair of threads and runs filesystem IO operations in both (using, effectively, the filesystem to communicate with each other).
#include <pthread.h>
#include <unistd.h>
#include <assert.h>
#include <string.h>
#include <fcntl.h>
#include <sys/stat.h>
#include <pthread.h>
const char *message = "1234567";
void *worker( void *_ )
{
char buf[ 8 ] = {};
int fd = open( "exampleFile", O_RDONLY );
assert( fd >= 0 );
char incoming;
int red = 0;
while (1) {
while ( read( fd, &incoming, 1 ) == 0 ) {}
if ( incoming == '-' )
break;
buf[ red ] = incoming;
++red;
}
assert( strcmp( buf, message ) == 0 );
assert( close( fd ) == 0 );
return _;
}
int main()
{
int fd = open( "exampleFile", O_WRONLY | O_CREAT, 0644 );
assert( fd >= 0 );
pthread_t thread;
pthread_create( &thread, NULL, worker, NULL );
assert( write( fd, message, 7 ) == 7 );
assert( write( fd, "-", 1 ) == 1 );
assert( close( fd ) == 0 );
pthread_join( thread, NULL );
return 0;
}[download]