Set only few bytes of the input as symbolic

[andreafioraldi]

Hi,
I'm trying to set only few bytes in the input as symbolic.

My idea is to transform the makeExpr method in memory.h from

  inline void makeExpr(ADDRINT addr) {
    ExprRef e = g_expr_builder->createRead(off_++);
    setExprToMem(addr, e);
  }

to something like this:

  inline void makeExpr(ADDRINT addr) {
   ExprRef e = g_expr_builder->createRead(off_++);
    if(off_ not in symbolic_offsets) {
      e = e.evaluateImpl();
    }
    setExprToMem(addr, e);
  }

Can you give me an opinion about this? Do you think that is possible to use QSYM in this way?
I'm modifying the right part of the codebase?

Thanks :)

[andreafioraldi]

Another fundamental question: Is it worth doing this? Have you an idea of the overhead of setting only e.g 10 bytes vs 500 bytes as symbolic? In the paper I read that QSYM solves only relevant constraints so maybe this is useless in terms of performance if I specify the interesting branches that must be considered (maybe using the AFL bitmap).

[insuyun]

Hi, Andrea.
Yes. You are modifying right part.
I think you can just clear the symbol in makeExpr.

  inline void makeExpr(ADDRINT addr) {
   ExprRef e = g_expr_builder->createRead(off_++);
    if(off_ not in symbolic_offsets) {
        clearExprFromMem(addr);
    }
   else {
        setExprToMem(addr, e);
    }
  }

For fundamental question, yes, it is worth doing this.
If you limit your symbolic data, you can save resources to make the constraint.
As noted in the paper, making the constraint is also a big part of symbolic execution's overhead.
Thank you.

[andreafioraldi]

Ok ty, I didn't understand that the concrete memory is firstly copied and then marked as symbolic so just unmarking seems fine.

Another question: As I understood from #4 I must compile the tool using an old GCC. Have you tried to compile it on Ubuntu 16 and then execute the pintool on a recent distro? There are kernel issues or it is just an ABI issue (I remember that libstdc++ should be provided by PIN so should be a compiler issue not related to libs).

[insuyun]

Actually, Ubuntu 16.04 also has ABI issue and we used hack for resolving that issue as you can see here.

For latest kernel, it seems it has some compatibility issue in PIN.
I think we need to dig into PIN for finding the reason
but I don't want to reverse PIN and I cannot patch it because it's not open source.
I feel like it would be better to move to other DBI, but I couldn't find good one yet.

[andreafioraldi]

Ok seems that an old kernel is the only solution, ty for your time.
I suggest you to switch to QEMU maybe adding opaque types + C api wrappers to call the QSYM code (it seems not so much PIN dependent). QEMU is the hard way but the only way that works.

[insuyun]

Yes, I feel like qemu seems the best option.
Thank you for your suggestion.