Hands On Experience

Aus /bin - basisgruppe informatik - wiki
Wechseln zu: Navigation, Suche

A cheat-sheet for the practical use of S²E


Creating Images

  • Start with an empty image and load a certain .ISO in the virtual CDROM-drive
qemu-img create -f raw s2e_disk.raw 2
qemu s2e_disk.raw -cdrom debian-6.0.0-i386-businesscard.iso
  • With ALT+CTRL+2 you can switch inside the QEMU-guest-machine to the QEMU-console. If you type 'quit' the VM is closed.
  • Convert the RAW-image to a QCOW2-Image to support copy-on-write and saving vmstates for S²E by typing 'savevm 1' (takes a few minutes on my quadcore... hm, what about copy on write?)
qemu-img convert -O qcow2 s2e_disk.raw s2e_disk.qcow2

QEMU: Networking between Guest and Host

(Source: http://hub.opensolaris.org/bin/view/Project+qemu/Qemu_Networking )

  • IP-Adress of Guest:
  • IP-Adress of Host (for Guest only):

If you install an SSH-server on the host, you can fetch files from the guest system:

scp user@

Workflow of symbolically execute a simple C-program

  • Start the guest system in vanilla-qemu and compile
gcc -m32 -O3 test.c -o test
-O3 activates level-3-optimization (f.ex. inlining)
-m32 This option generates code for a 32-bit environments (this is especially needed when you want to compile for a 32-bit-code in a 64-bit-environment).


  • I've found the following warning in messages.txt: KLEE: WARNING: calling external: cpu_x86_handle_mmu_fault(2922820, c60a1f80, 1, 0, 1). What does it mean?

Symbolically execute simple java-programs with S2E

  • I started from here

Use Java Native Interface

My files look like this: First, a Wrapper which mitigates the calls to the native S2E-methods in s2e.h


public class S2EWrapper {

	public static native int getVersion();
	public static native void printMessage(String message);
	public static native void printWarning(String warning);
	public static native void enableForking();
	public static native void disableForking();
	public static native void killState(int status, String message);
	// only done for integers for now
	public static native int getSymbolic(String name);
	public static native int getExampleValue(int symbvar);
	public static native int concretize(int var);
	public static native void assertThat(boolean condition, String failMessage);
	//Load the library
	  static {

Note for System.loadLibrary: In Unix-Environments, if you specify "S2EWrapper" as library, you need to have a "libS2EWrapper.so" file containing the native library. In Windows-environments, the filename has to be S2EWrapper.dll.

Next, a java-class which calls native libs:

public class jtest {

	 * @param args
	public static void main(String[] args) {
		int x = 2;
		int max = 30;
		if (args.length == 2) {
			try {
				x = Integer.parseInt(args[0]);
				max = Integer.parseInt(args[1]);
			} catch (Exception e ) {
				System.out.println("arguments are not integers - using default values.");
			int level = checkRadiation(x,max);
			System.out.println("Alarm Level: "+level);
		System.out.println("we need two integer arguments");

	public static int checkRadiation(int x, int max) {
		System.out.println("S2E-Version: "+S2EWrapper.getVersion());
		System.out.println("X: "+x+" MAX: "+max);
		  x = S2EWrapper.getSymbolic("s");
		  int ret = 0;
		  if (x <= (max/2)) {
			 S2EWrapper.printMessage("if branch. example: "+S2EWrapper.getExampleValue(x));
		     ret = x/1;
		  } else if (x <= max) {
			 S2EWrapper.printMessage("elseif branch. example: "+S2EWrapper.getExampleValue(x)); 
		     ret= x/2;
		  } else {
			  S2EWrapper.printMessage("else branch. example: "+S2EWrapper.getExampleValue(x));
			  ret= x/3;

		S2EWrapper.assertThat(ret >=0, "Alarm level is not positive.");
		S2EWrapper.killState(1, "State killed");
		return ret;

First, automatically create a header-file S2EWrapper.h to get signatures for the methods:

javah -jni S2EWrapper

Based on this, create a S2EWrapper.c and implement the methods:

#include <jni.h>
#include <s2e.h>
#include "S2EWrapper.h"

JNIEXPORT jint JNICALL Java_S2EWrapper_getSymbolic
  (JNIEnv *env, jclass class, jstring symbname) {
		jboolean iscopy;
		int x;
		const char *symbol = (*env)->GetStringUTFChars(
	                env, symbname, &iscopy);
	    s2e_make_symbolic(&x, sizeof(x), symbol);
	    return x;

JNIEXPORT jint JNICALL Java_S2EWrapper_getVersion
  (JNIEnv *env, jclass class) {
	return s2e_version();

JNIEXPORT void JNICALL Java_S2EWrapper_printMessage
  (JNIEnv *env, jclass class, jstring string) {

	jboolean iscopy;
	const char *message = (*env)->GetStringUTFChars(env, string, &iscopy);

JNIEXPORT void JNICALL Java_S2EWrapper_printWarning
  (JNIEnv *env, jclass class, jstring string) {

	jboolean iscopy;
	const char *message = (*env)->GetStringUTFChars(env, string, &iscopy);

JNIEXPORT void JNICALL Java_S2EWrapper_enableForking
  (JNIEnv *env, jclass class) {

JNIEXPORT void JNICALL Java_S2EWrapper_disableForking
  (JNIEnv *env, jclass class) {

JNIEXPORT void JNICALL Java_S2EWrapper_killState
  (JNIEnv *env, jclass class, jint status, jstring string) {
	jboolean iscopy;
	const char *message = (*env)->GetStringUTFChars(env, string, &iscopy);
	int i_status = status;
	s2e_kill_state(i_status, message);

JNIEXPORT jint JNICALL Java_S2EWrapper_getExampleValue
  (JNIEnv *env, jclass class, jint var) {
	s2e_get_example(&var, sizeof(var));
	return var;

JNIEXPORT jint JNICALL Java_S2EWrapper_concretize
  (JNIEnv *env, jclass class, jint var) {
		return var;

JNIEXPORT void JNICALL Java_S2EWrapper_assertThat
  (JNIEnv *env, jclass class, jboolean condition, jstring failmsg) {
		jboolean iscopy;
		const char *message = (*env)->GetStringUTFChars(env, failmsg, &iscopy);

To simplify, create a makefile to do all the necessary stuff:

all : libS2EWrapper.so

libS2EWrapper.so : S2EWrapper.o
	gcc -m32 -O3 -shared -o libS2EWrapper.so S2EWrapper.o

S2EWrapper.o : S2EWrapper.c S2EWrapper.h
	gcc -m32 -O3 -I "/usr/lib/jvm/java-6-openjdk/include/" -I "/home/aka/S2E/s2e/guest/include" -I "/home/aka/workspace/s2ejava/src" -c S2EWrapper.c -o S2EWrapper.o

S2EWrapper.h : S2EWrapper.class
	javah -jni S2EWrapper

S2EWrapper.class :
	javac S2EWrapper.java

clean :
	-rm S2EWrapper.h
	-rm S2EWrapper.o
	-rm S2EWrapper.class
	-rm libS2EWrapper.so

When calling make all it creates a header-file S2EWrapper.h, then an object file (given the necessary paths) and a shared library.

On the guest machine

  • use s2e-disabled-qemu for preparation (faster)
  • retrieve the directory from the host machine
scp -r user@ ./
  • install a jdk (apt-get install openjdk-6-jdk)
  • make clean all
  • <ALT>+<CTRL>+2 to get into QEMU-console / savevm 1 to save the state / quit
  • run the java program with the command below - use s2e-enabled-qemu with the stored state: ~/S2E/qemu-release/i386-s2e-softmmu/qemu ~/S2E/s2e_disk.qcow2 -loadvm 1 -s2e-config-file ~/S2E/config.lua -s2e-verbose
java -Djava.library.path=./ jtest 1 4

You may see the following native code-error with vanilla QEMU which disappears when you use a S2E-patched qemu (directories $S2E/qemu-release/i386-softmmu and i386-s2e-softmmu).

# A fatal error has been detected by the Java Runtime Environment:
#  SIGILL (0x4) at pc=0x00007fd509a475d5, pid=29583, tid=140553105749760
# JRE version: 6.0_20-b20
# Java VM: OpenJDK 64-Bit Server VM (19.0-b09 mixed mode linux-amd64 compressed oops)
# Derivative: IcedTea6 1.9.7
# Distribution: Ubuntu 10.10, package 6b20-1.9.7-0ubuntu1
# Problematic frame:
# C  [libS2EWrapper.so+0x5d5]
# An error report file with more information is saved as:
# /home/aka/workspace/s2ejava/src/hs_err_pid29583.log
# If you would like to submit a bug report, please include
# instructions how to reproduce the bug and visit:
#   https://bugs.launchpad.net/ubuntu/+source/openjdk-6/
# The crash happened outside the Java Virtual Machine in native code.
# See problematic frame for where to report the bug.

Look at Machine Code / Byte Code

Some useful links:

When using S²E it makes sense to view machinecode and bytecode to understand what is going on during symbolic execution:

  • You can store the bytecode of the file jtest.class to jtest.bytecode by typing:
javap -c jtest >jtest.bytecode
  • Moreover, path conditions in S²E are formulated in KLEE query language, for example:
(Eq 0 (And w32 (LShr w32 (LShr w32 (Extract w32 0 (SDiv w64 (Or w64 (Shl w64 (ZExt w64 (AShr w32 N0:(ReadLSB w32 0 s) 31)) 32) (ZExt w64 N0)) 1)) 24) 7) 1))

Get Machine code which is the result of JITing bytecode inside JVM

Getting the actual machine code which is created when the Java Virtual Machine compiles the bytecode into native machine code (i.e. X86 instructions) is not difficult but requires a bit work in the guest OS:

  • To use the Program Counter (PC)-information which is logged during the execution in S²E (written in messages.txt), we need to know the current assembly code as it is created and executed, because this is exactly the code which is then put into KLEE (in symbolic execution mode).
  • In Open-JDK you need to install a disassembler plugin (as described in this article). I chose to download the compiled binary for i386 on the guest machine.
  • Installation means copying the downloaded plugin (something like: libhsdis-i386.so) to the directories where the libjvm.so is located. Here in the guest debian system:
    • /usr/lib/jvm/java-6-openjdk/jre/lib/i386/client
    • /usr/lib/jvm/java-6-openjdk/jre/lib/i386/server
  • save the vmstate (savevm 1) and start this state with S²E-enabled QEMU. Then run the following command to execute the test program in S²E with the disassembler plugin enabled (get some tea, it takes longer than usual):
java -Djava.library.path=./ -XX:+UnlockDiagnosticVMOptions -XX:+PrintAssembly -Xcomp jtest 1 4 >jtest.fullyDisassembled.txt
  • It is also possible to restrict the output of disassembled statements to certain methods:
java -Djava.library.path=./ -XX:+UnlockDiagnosticVMOptions -XX:CompileCommand=print,jtest.checkRadiation -XX:CompileCommand=print,S2EWrapper.* -Xcomp jtest 1 4 >jtest.checkRadiationDisassembled.txt
  • Furthermore, you can print the list of compiled methods (but its easier to have the whole output to have the instructions of most of the possible pc's which could appear in message.txt):
java -Djava.library.path=./ -XX:+UnlockDiagnosticVMOptions -XX:+PrintCompilation -Xcomp jtest 1 4 >jtest.listOfCompiledMethods.txt
  • Unfortunately, all writes to harddisc are lost and since we piped the output in the file jtest.checkRadiationDisassembled.txt and the all states are killed, the file is lost after shutdown. But we can forward the file over scp after executing is done and before the initial state is killed:
java -Djava.library.path=./ -XX:+UnlockDiagnosticVMOptions -XX:+PrintAssembly -Xcomp jtest 1 4 >jtest.checkRadiationDisassembled.txt; scp jtest.checkRadiationDisassembled.txt <user>@; ./kill;
  • Since there is no password parameter for scp, you need to work with ssh-keys in order to send data without password query: Generate a keypair (private/public) and send it to the host machine (f.ex. see instructions here)
  • I had to comment out the killState()-statement in the target java program. This gives me the opportunity to send the generated file jtest.checkRadiationDisassembled.txt to the host. To force a shutdown of the guestmachine afterwards, I wrote and compiled a simple c program which only executes a s2e_killState(0,"autokill") in the main routine.