Hi,
This looks like the expected behavior. S2E uses concolic
execution [1], which means that when the path terminates, there is
no need to call the solver, the initial values (c, 5) will be
used. S2E calls the solver on forks, which will create a new set
of concrete inputs to be used on the forked path. To get
alternative values, you need to enable forking. You can also save
the constraints, negate them offline, then use the new concrete
inputs in another run. S2E does not have support for this yet.
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
---
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/b5b9163c-5f96-4f7c-91b3-487ccac7caf2n%40googlegroups.com.
Hi,
Right, I forgot that by default, S2E forks and concretizes
symbolic pointers. You need to disable that [1].
Vitaly
[1]
https://github.com/S2E/s2e/blob/master/libs2ecore/src/S2EExecutor.cpp#L111
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/a22e2166-35ef-41e6-b64d-92d655639b5an%40googlegroups.com.
Hi,
Here is a slightly tweaked program that should behave properly (4
states).
- Made the array aligned
- Made it 256-byte long
- Checked that -Wall doesn't return any warnings. Your original
code had symbolic signed indexes, which could go negative during
symbolic execution.
The reason for this is because S2E's symbolic pointer handling
has various limitations:
- It cannot handle symbolically pointers that span multiple pages.
- It restricts symbolic pointers to chunks of 256 bytes. Anything
larger than that will cause many forks to handle all possible
cases of unaligned accesses.
#include <stdio.h>
#include <string.h>
#include <unistd.h>
#include <s2e/s2e.h>
__attribute__ ((aligned (0x1000))) unsigned char spec[256] = {0};
int main(void) {
// suppose the characters to be checked are "c5"
unsigned char input[32] = { 0 };
input[0] = 'c';
input[1] = '5';
s2e_make_symbolic(input, 32, "input");
// init the spec array
// 1 means the char is allowed (i.e. in spec)
spec['c'] = 1;
// 0 means the char is not allowed (i.e. not in spec)
spec['5'] = 0;
if(spec[input[0]]){
printf("input[0]: 'c' is in spec\n");
}else{
printf("input[0]: 'c' NOT in spec\n");
}
if(spec[input[1]]){
printf("input[1]: '5' is in spec\n");
}else{
printf("input[1]: '5' NOT in spec\n");
}
return 0;
}
Vitaly
Hi,
It's not clear to me why you would get the constraints you mention. Please find attached the query log and the project for the program I gave you. You will see queries of this form:
# Query 10 -- Type: InitialValues,
Instructions: 28685
array const_arr1[4096] : w32 -> w8 = [0x0 ... 0x0]
array v0_input_0[32] : w32 -> w8 = symbolic
(query [(Eq false
(Eq 0x0
(Read w8 (ZExt w32 (Read w8 0x1 v0_input_0))
U0:[0xfff=0x0, 0xffe=0x0, 0xffd=0x0,
0xffc=0x0, 0xffb=0x0, 0xffa=0x0, ... 0x3=0x0, 0x2=0x0, 0x1=0x0,
0x0=0x0] @ const_arr1)))
(Eq 0x0
(Read w8 (ZExt w32 (Read w8 0x0 v0_input_0))
U0))]
false []
[v0_input_0])
# OK -- Elapsed: 5.237028e-01
# Solvable: true
# v0_input_0 =
[100,99,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100,100]
You get an array of constants that contains the fixed spec array.
The symbolic expressions reads from that array.
Use the following settings in s2e-config.lua, don't modify the
settings in the source.
kleeArgs = {
"--fork-on-symbolic-address=false",
"--use-query-log=all:kquery",
}
Vitaly
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/f7fceee2-e3b2-43e9-aae3-362ce4457b03n%40googlegroups.com.
Hi,
Symbolic pointers in S2E are not ready for real-world programs yet, that's why they are disabled by default. Symbolic pointers make it much harder to solve constraints. Symbolic execution engines that have access to the source code, e.g., KLEE, can reason more precisely about them, by sending to the solver the minimum required (e.g., your spec array). S2E however, does not know anything about this, so it has to send entire memory pages instead. This unfortunately breaks the solver. Perhaps it's possible to rewrite the queries to make it easier on the solver, but I am no expert on this.
Something else you could do is rewrite your symbolic array
accesses in terms of it-then-else. You could have a function spec
that looks like this:
uint8 spec(uint8 index) {
if (index == 0) return 'a';
if (index == 1) return 'b';
...
if (index == 255) return ...;
}
You will end up with simpler constraints and DART-style concolic execution should have no problems extracting them and negating the desired ones to produce alternate concrete inputs.
Vitaly
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/a37f51ef-be52-420c-97bc-52a1357f5514n%40googlegroups.com.
Hi,
You should see two calls to forkAndConcretize in most cases [1]: one for the whole address and another one for the upper 20 bits. Those must always be concrete, as they are used as an index for the TLB and walking page tables. S2E only allows the lower 12 bits to be symbolic. That's why you see the right shift by 12 bits in the fork-on-symbolic-address=false case. You don't see it in the true case, because the address was fully concretized by the first call, so there is nothing symbolic left.
Regarding doConcretize, is should be set by plugins that hook the onSymbolicAddress event.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/d629d52d-1111-4f6f-8466-31e4426842een%40googlegroups.com.