Losing track of symbolic tags

[jon]

Hi,

I am using S2E to trace dataflow by marking a buffer as symbolic then checking to see if the tag is propagated. 

For example, I may use S2EMakesymbolic(buf, len, 'unique_tag') to mark the 'buf' as symbolic, then subsequently evaluate data occurring later in the execution to see if it contains the tag (e.g., ReadLSB w32 0x0 v2_uniqe_tag_4).

This works well and I am able to find operations that are dependent upon this buffer ('buf'). However, I eventually lose track of the tag.  To illustrate the problem, take FuncA.

FuncA(buf) -> takes the 'buf' as an argument and I can confirm the tag is present. FuncA calls VirtualAlloc to create 'NewBuf'.  FuncA then computes upon 'buf' translating it and storing the result in 'NewBuf'.  During execution, I periodically check in to see if the tag is present, and it is, but I eventually lose it.  I would expect, since 'buf' is symbolic, that the resulting data stored in 'NewBuf' would retain the symbolic tag 'unique_tag'.  Is this not the case? If it isn't, do you have any advice on tracking data dependence of symbolic data?  

[Vitaly Chipounov]

Hi,

I suspect you ran into the under tainting problem. You may have
indirect dependency between the first and the second buffer. In the
following case, buf2 would contain only concrete data, although its
content depends on buf1. This dependency is encoded in path
constraints.

char *f(char *buf1) {
char *buf2 = malloc(...)
if (buf2[0]) {
buf2[0] = 1;
} else {
buf2[0] = 2;
}
return buf2;
}

You can have the opposite problem, where the output seems to be
derived from the input, when it is actually not. For example buf2[0] =
buf1[0] xor buf1[0]. Unless the symbolic execution engine is smart
enough to figure out that the result is always 0, it will build an
expression derived from the input.

These two issues are known as under and over tainting. Unfortunately,
I don't have an easy solution for that.

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/8ee51d05-0ee7-41d5-8fd2-112bce102914n%40googlegroups.com.

[jon]

Thanks for your response.