Errors getting started with s2e

[darkthor]

Hello,

I am new to S2E so I apologize if I am asking very basic installation questions. I have set up my own S2E environment, but I'm not completely sure I have everything just right, also based on the outputs I am getting after running S2E, I don't think I'm getting expected output.

I have a Ubuntu 12.04 x64 host on which I downloaded S2E off the git repository. I built everything and installed the dependencies. I then created a Ubuntu 12.04 32-bit qemu image, following the VM setup instructions on the website. I amusing the following config file:

s2e = {

  kleeArgs = {

     "--use-batching-search=true", "--batch-time=2.0"

  }

}

plugins = {

  "BaseInstructions",

  "RawMonitor",

  "ModuleExecutionDetector",

  "CodeSelector",

  "HostFiles",

  "ExecutionTracer"

}

pluginsConfig = {}

pluginsConfig.ModuleExecutionDetector = {}

pluginsConfig.CodeSelector = {}

pluginsConfig.ExecutionTracer = {}

pluginsConfig.HostFiles = {

   baseDirs = {"/home/user/stage/build/myfiles"}

}

I launch S2E with the following command:

qemu-release/i386-s2e-softmmu/qemu-system-i386 disk.qcow2 -s2e-config-file config.lua -s2e-verbose -loadvm 3

I then observe the following output in the host console:

S2E: output directory = "/home/user/stage/build/s2e-out-1"

WARNING: Linking two modules of different data layouts!

Creating plugin CorePlugin

Creating plugin BaseInstructions

Creating plugin RawMonitor

Creating plugin ModuleExecutionDetector

Creating plugin CodeSelector

Creating plugin HostFiles

Creating plugin ExecutionTracer

Can not get configuration value 'pluginsConfig['RawMonitor']':

    value of type nil can not be converted to lua_table with only string keys

Can not get configuration value 'pluginsConfig['RawMonitor'].kernelStart':

    [string "return pluginsConfig['RawMonitor'].kernelSt..."]:1: attempt to index field 'RawMonitor' (a nil value)

You should specify pluginsConfig['RawMonitor'].kernelStart

ModuleExecutionDetector: no configuration keys!

Can not get configuration value 'pluginsConfig['ModuleExecutionDetector'].trackAllModules':

    value of type nil can not be converted to boolean

Can not get configuration value 'pluginsConfig['ModuleExecutionDetector'].configureAllModules':

    value of type nil can not be converted to boolean

Can not get configuration value 'pluginsConfig['CodeSelector'].moduleIds':

    value of type nil can not be converted to lua_list with only string values

You should specify a list of modules in pluginsConfig['CodeSelector'].moduleIds

0 [State 0] Created initial state

Adding CPU (addr = 0x7fe23f7b7820, size = 0x4dc80)

Initing initial device state.

WARNING!!! All writes to disk will be lost after shutdown.

I am concerned about the WARNING in the above, but the VM seems to load. I have copied and built the guest directory on the VM. I then execute the following:

LD_PRELOAD=/home/s2e/guest/init_env/init_env.so /bin/echo --select-process-code --sym-args 0 2 4

Things then seem to run indefinitely. The host console spews info about switch from state to state, but the process never seems to complete. Ideally I want to run my own binaries and see s2e launch all the different paths of the program. Before I post about this issue, maybe I can get some clarification on whether I am running things properly, does the above output make sense? I would love to know what values s2e is using symbollically.

Thanks,

darkthor

[darkthor]

Clarification - the Ubuntu versions are 12.10

[Jonas Wagner]

Hi Darkthor,

good to see that you're interested in using S2E!

From the information that you provide, I think you're on a good track. For your next questions, do give us a bit more info please, e.g., by zipping and attaching the s2e-out folder.

What happens when you run

LD_PRELOAD=/home/s2e/guest/init_env/init_env.so /bin/echo --select-process-code --sym-args 0 2 4

inside S2E is the following: The echo program is started. Just before it is run, the init_env library intercepts the call to main(). It creates an argv[] array that contains between 0 and 2 symbolic arguments, each up to four characters long. Then, main() is called. Inside main, echo parses its arguments, and executes different code depending on whether they are "-h", "-e", ..., or just some text. Each time such a branch happens, S2E will fork a state. It will execute these states one after another, switching between them from time to time, until all the states are terminated.

What you need to tell S2E is that you'd like to terminate a state when echo has finished running. You'd do this by adding an S2E kill command after echo, as follows:

LD_PRELOAD=/home/s2e/guest/init_env/init_env.so /bin/echo --select-process-code --sym-args 0 2 4; /home/s2e/guest/s2ecmd/s2ecmd kill 0 "echo done"

You can also add the TestCaseGenerator plugin to your configuration. Then you will see the command line arguments that correspond to each S2E state. Finally, the following two options (added to kleeArgs in your config.lua) will make everything a bit faster:

    "--flush-tbs-on-state-switch=false",

    "--state-shared-memory=true",

Hope this helps,

Jonas

[Vitaly Chipounov]

On 17.01.2013 11:25, Jonas Wagner wrote:

What you need to tell S2E is that you'd like to terminate a state when echo has finished running. You'd do this by adding an S2E kill command after echo, as follows:

LD_PRELOAD=/home/s2e/guest/init_env/init_env.so /bin/echo --select-process-code --sym-args 0 2 4; /home/s2e/guest/s2ecmd/s2ecmd kill 0 "echo done"

Thanks for the s2ecmd tip, Jonas. I will add it to the documentation.

Vitaly

--
--
You received this message because you are a member of the S2E Developer Forum.
To post to this group, send email to s2e...@googlegroups.com
To unsubscribe from this group, send email to s2e-dev+u...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/s2e-dev
 
 
 

[darkthor]

Thank you. I reran the echo example with full LD_PRELOAD command line as suggested. I did not see the VM flickering back and forth between states, but the debug info does look like it was in fact doing so. The echo command though didn't seem to quit though, the VM seemed to hang indefinitely. I am attaching the output to help confirm my use of s2e.

Ideally what I would like to do is run a binary (no source) and find out how s2e handled the return value and outputs of library calls (e.g. connect, read, write, recv, etc.). My understanding is that S2E will generate a concrete output or return value for these calls in order to force the program down a particular path in code. I'd like to know what those values are during each trace. Does this make sense in terms of S2E?

Thank you

[darkthor]

OK I think I am finally beginning to understand how this works. So based on what I just read in my other post, it sounds like I can only learn the symbolic values from the library calls if I change the source to use the s2e api. Otherwise my only option for kicking off the forking/path exploration is based on symbolic inputs. Is that correct?

[Jonas Wagner]

Hi,

OK I think I am finally beginning to understand how this works. So based on what I just read in my other post, it sounds like I can only learn the symbolic values from the library calls if I change the source to use the s2e api. Otherwise my only option for kicking off the forking/path exploration is based on symbolic inputs. Is that correct?

I think this is correct. And actually, it's one of the biggest strengths of S2E, not a limitation. What I mean by this is that S2E allows you to test a software in a real environment. Functions such as accept() are not stubs, or models that return arbitrary, inconsistent values. This is very important because it means that all executions that S2E finds are real executions, that can happen in the software you test. You will not have false alarms (bug reports that only occur inside S2E, but not in reality).

That said, S2E allows you to insert symbolic data in a lot of places; you could for example intercept the accept() function call and override it's return value. There are plugins in S2E to do this. It involves a little bit of coding but is definitely feasible. You can find more about this in the paper [1] under "consistency models". I've not used that feature myself, but probably others on this list could help you.

[1]: S2E Paper: Chipounov, V., Kuznetsov, V., & Candea, G. (2011). S2E: A platform for in-vivo multi-path analysis of software systems. ASPLOS. http://dslab.epfl.ch/pubs/s2e.pdf

Have a lot of fun!

Jonas

[0xefbeefbe]

Michael,

You may find "The S2E Platform: Design, Implementation, and Applications paper of use as well http://dslab.epfl.ch/pubs/s2e-tocs.pdf. It helped kick start my understanding of S2E, especially the application of S2E.

Regards,

Shawn