Question about state fork in s2e

35 views
Skip to first unread message

forwo...@gmail.com

unread,
Nov 21, 2020, 11:10:06 AM11/21/20
to S2E Developer Forum
Hello, I am using s2e to test a CTF problem, and I found that s2e did not fork a new state as expected in a certain branch. As shown in the figure, I created a symbol variable v1 in pickTigerType (b) and then stored it on the heap in makeTiger(a). When the program is executed at the IF branch of pwnMe (d), there is no new state being forked. It is reasonable to say that the data taken from the heap should be the symbol variable v1 just passed in.

Specifically, when makeTiger copied data to the memory, I tested that their source operands EAX and EDX are both symbolic data (c), but when executed to the CMP instruction of pwnMe, I tested that EAX is not a symbolic value.

I want to know why this happens? Maybe you can provide me with an idea to solve it. 

Expecting your reply.
865001605973616_.pic_hd.jpg

Vitaly Chipounov

unread,
Nov 21, 2020, 12:03:29 PM11/21/20
to s2e...@googlegroups.com, forwo...@gmail.com

Hi,

Could you please run s2e export_project and attach the resulting archive? It will be easier for us to see what's wrong.

Vitaly

865001605973616_.pic_hd.jpg --
--
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/93f71f38-4fde-43a6-a707-a9eaa7e6117bn%40googlegroups.com.

forwo...@gmail.com

unread,
Nov 22, 2020, 4:08:32 AM11/22/20
to S2E Developer Forum
Thank you for your reply. I have figured it out. Since I read the data in that heap memory, the value at that location has been concreted.

KLEE: WARNING: silently concretizing (reason: memory access from concrete code) to value 0x1

Vitaly Chipounov

unread,
Nov 22, 2020, 7:27:39 AM11/22/20
to s2e...@googlegroups.com, forwo...@gmail.com

Hi,

S2E does not concretize data in the heap. Symbolic data can be stored anywhere in RAM. Concretizations occur when writing symbolic data to devices (e.g., printing symbolic data on the screen) or to control registers of the CPU.

Vitaly

forwo...@gmail.com

unread,
Nov 22, 2020, 10:17:00 AM11/22/20
to S2E Developer Forum
I found this function in S2EExecutionStateMemory.cpp and it seems to write this value to object_offset + i after concrete. Did I understand it wrong?
```
void S2EExecutionStateMemory::transferRamInternal(const klee::ObjectStateConstPtr &os_, uint64_t object_offset,
uint8_t *buf, uint64_t size, bool write, bool exitOnSymbolicRead) {
klee::ObjectStateConstPtr os = os_;

if (os->isSharedConcrete()) {
assert(!exitOnSymbolicRead);

/* This can happen in case of access to device memory */
uint8_t *concreteStore = (uint8_t *) os->getAddress();
if (write) {
memcpy(concreteStore + object_offset, buf, size);
} else {
memcpy(buf, concreteStore + object_offset, size);
}
return;
}

if (write) {
auto wos = m_addressSpace->getWriteable(os);
bool oldAllConcrete = wos->isAllConcrete();

for (uint64_t i = 0; i < size; ++i) {
wos->write8(object_offset + i, buf[i]);
}

bool newAllConcrete = wos->isAllConcrete();
if ((oldAllConcrete != newAllConcrete) && (wos->notifyOnConcretenessChange())) {
m_notification->addressSpaceSymbolicStatusChange(wos, newAllConcrete);
}

} else {
ObjectStatePtr wos = nullptr;
for (uint64_t i = 0; i < size; ++i) {
if (!os->readConcrete8(object_offset + i, buf + i)) {
if (exitOnSymbolicRead) {
// m_startSymbexAtPC = getPc();
// XXX: what about regs_to_env ?
pabort("Check cpu_restore_state");
// fast_longjmp(env->jmp_env, 1);
}

if (!wos) {
os = wos = m_addressSpace->getWriteable(os);
}

buf[i] = m_concretizer->concretize(wos->read8(object_offset + i), "memory access from concrete code");
wos->write8(object_offset + i, buf[i]);
}
}
}
}
```

Vitaly Chipounov

unread,
Nov 22, 2020, 10:44:50 AM11/22/20
to s2e...@googlegroups.com, forwo...@gmail.com

Yes, this function concretizes any symbolic data it reads.

forwo...@gmail.com

unread,
Nov 22, 2020, 11:17:31 AM11/22/20
to S2E Developer Forum
So as long as I read the memory, the location of that memory will be written permanently, and it is no longer a symbolic value?

I tried to remove write8() but found that some of the constraints I originally added could not be added successfully. I have seen the function transferRamInternalSymbolic, but it doesn't seem to be called.

So I want to ask if there is a good way to read the value of the memory without affecting the symbol data, just like register reading ( Call regs()->read ), if it is a symbol value, it returns false.

Thank you for answering my question.

Vitaly Chipounov

unread,
Nov 22, 2020, 12:12:51 PM11/22/20
to s2e...@googlegroups.com, forwo...@gmail.com

I don't understand what you are trying to solve. If the problem is the unwanted concretization you mentioned earlier, we first need to understand why it happens. Please attach the project file as instructed earlier, so that we can help with debugging.

Vitaly

Reply all
Reply to author
Forward
0 new messages