Execution Consistency Models

[yvonn...@gmail.com]

Hello,everyone

        It mentions 6  execution consistency models in the s2e paper. I want to know when I create a new project with the default configuration in the s2e.yaml ,bootstrap.sh and launch-s2e.sh, which model will be used. where can I find this configuration and change it?

   wish to your reply, thanks

[Vitaly Chipounov]

Hi,

The paper describes execution consistency models at a conceptual level. In general, you can't change which model is used with a flip of a switch. Instead, each application implicitly implements one model that is most suitable for it and optionally provides extra levels when useful.

The models help you reason about the effects of making input symbolic at different levels. If you want to get coverage faster, you would typically start injecting symbolic values more aggressively, at the expense of false positives.

- If you inject symbolic values from outside the system, you will get strict consistency. For example, If you create a new project with a binary that takes as input a symbolic file, you will implicitly get strict consistency.

- If you inject symbolic values anywhere inside the system, you will get a form of relaxed consistency. For example, the device driver testing fault injection tutorial demonstrates local consistency by injecting symbolic faults inside the driver. There is an option to have a more relaxed injection by setting the appropriate switch [1].

I hope this clarifies it.

Vitaly

[1] https://github.com/S2E/s2e-env/blob/master/s2e_env/templates/bootstrap.windows_driver.sh#L16

--
--
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

---
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Qing mrivca]

Thanks，Vitaly！！